Module dev.civl.sarl

Package dev.civl.sarl.IF

Interface SymbolicUniverse

All Superinterfaces:

CoreUniverse

public interface SymbolicUniverse
extends CoreUniverse

A symbolic universe is used for the creation and manipulation of SymbolicObjects. The symbolic objects created by this universe are said to belong to this universe. Every symbolic object belongs to one universe, though a reference to the universe is not necessarily stored in the object.

s are one kind of symbolic object. Other symbolic objects include

invalid reference

SymbolicCollection

s (such as sequences, sets, and maps), SymbolicTypes, and various concrete SymbolicObjects.

SymbolicObjects implement the Immutable Pattern: all symbolic objects are immutable, i.e., they cannot be modified after they are created.

Nested Class Summary

Nested classes/interfaces inherited from interface dev.civl.sarl.IF.CoreUniverse

CoreUniverse.ForallStructure

Method Summary

Modifier and Type	Method	Description
Number	extractNumber(BooleanExpression assumption, NumericExpression expression)	Attempts to extract a concrete numeric value from the given expression, using the assumption if necessary to simplify the expression.
Reasoner	reasoner(BooleanExpression context)	Returns a Reasoner for the given context.
Reasoner	reasoner(List<BooleanExpression> contextStack)
void	setLogicFunctions(ProverFunctionInterpretation[] logicFunctions)	Set a list of logic functions with their definitions to the universe so that Reasoners created by this universe can take use of the definitions of the given logic functions.
SymbolicExpression	valueSetElimWidening(BooleanExpression context, SymbolicExpression vst, SymbolicExpression elimExpr, SymbolicExpression lower, SymbolicExpression upper)
SymbolicExpression	valueSetProtectiveWidening(BooleanExpression context, SymbolicExpression vstM, SymbolicExpression vstP)
SymbolicExpression	valueSetWidening(BooleanExpression context, SymbolicExpression vst)	Apply a default widening operator to the value set references in the given value set template.

Methods inherited from interface dev.civl.sarl.IF.CoreUniverse

add, add, and, and, append, apply, array, array, arrayDimensionAndBaseType, arrayElementReference, arrayLambda, arrayRead, arrayType, arrayType, arrayWrite, assign, bitand, bitnot, bitor, bitshiftLeft, bitshiftRight, bitvector2Integer, bitVectorType, bitxor, bool, bool, booleanObject, booleanType, boundedIntegerType, canonicalRenamer, canonicalRenamer, cardinality, cast, ceil, character, characterType, comparator, compatible, concreteValueOfUninterpretedType, cond, constantArray, constantSubstituter, denseArrayWrite, dereference, derivative, differentiable, divide, divides, emptyArray, emptyMap, entrySet, entryType, equals, equiv, exists, existsInt, expand, extractBoolean, extractCharacter, extractNumber, falseExpression, floor, forall, forallInt, fullySubstitute, functionType, functionType, get, getErrFile, getForallStructure, getFreeSymbolicConstants, getIntegerLengthBound, getOutputStream, getProbabilisticBound, getShowProverQueries, getShowQueries, getSummands, getUseBackwardSubstitution, herbrandIntegerType, herbrandRealType, identityReference, implies, insertElementAt, integer, integer, integer, integer2Bitvector, integerType, intObject, isPermutCall, isSigmaCall, isSubsetOf, keySet, lambda, length, lessThan, lessThanEquals, make, mapSize, mapSubstituter, mapSubstituter, mapType, minus, modulo, multiply, multiply, nameSubstituter, neq, not, nullExpression, nullReference, number, number, numberFactory, numberObject, numObjects, numProverValidCalls, numValidCalls, objectWithId, offsetReference, oneInt, oneReal, or, or, permut, power, power, power, printCompressed, printCompressedTree, printExprTree, pureType, put, quickEquals, rational, rational, rational, rational, rational, rational, rational, rational, realType, reduction, referencedType, referenceType, removeElementAt, removeEntryWithKey, removeQuantifiers, roundToZero, setAdd, setDifference, setErrFile, setIntegerLengthBound, setIntersection, setOutputStream, setProbabilisticBound, setRemove, setShowProverQueries, setShowQueries, setType, setUnion, setUseBackwardSubstitution, sigma, simpleSubstituter, stringExpression, stringObject, subtract, symbolicConstant, symbolicUninterpretedType, trueExpression, tuple, tuple, tupleComponentReference, tupleRead, tupleType, tupleWrite, unionExtract, unionInject, unionMemberReference, unionTest, unionType, valueSetAssigns, valueSetContains, valueSetDiff, valueSetHavoc, valueSetNoIntersect, valueSetReferences, valueSetReferenceType, valueSetTemplate, valueSetTemplateType, valueSetUnion, valueType, vsArrayElementReference, vsArraySectionReference, vsArraySectionReference, vsIdentityReference, vsOffsetReference, vsTupleComponentReference, vsUnionMemberReference, zeroInt, zeroReal

Method Details

reasoner

Reasoner reasoner(BooleanExpression context)

Returns a Reasoner for the given context. A Reasoner provides simplification and reasoning services. The context is the boolean expression assumed to hold by the reasoner. The Reasoner can be used to determine if a boolean predicate is valid; it may use an external theorem prover to assist in this task.

Parameters:

context - the boolean expression assumed to hold by the Reasoner

Returns:

a Reasoner with the given context

reasoner

Reasoner reasoner(List<BooleanExpression> contextStack)

extractNumber

Number extractNumber(BooleanExpression assumption,
 NumericExpression expression)

Attempts to extract a concrete numeric value from the given expression, using the assumption if necessary to simplify the expression. For example, if the assumption is "N=5" and the expression is "N", this method will probably return the number 5. If it cannot obtain a concrete value for whatever reason, it will return null.

Parameters:

assumption - a boolean expression that is assumed to hold

expression - a symbolic expression of numeric type

Returns:

a concrete Number or null

valueSetWidening

SymbolicExpression valueSetWidening(BooleanExpression context,
 SymbolicExpression vst)

Apply a default widening operator to the value set references in the given value set template.

Parameters:

context - the context (path condition) in which this widen is being applied

vst - a value set template

Returns:

the value set template after being applied the default widening operator

valueSetProtectiveWidening

SymbolicExpression valueSetProtectiveWidening(BooleanExpression context,
 SymbolicExpression vstM,
 SymbolicExpression vstP)

valueSetElimWidening

SymbolicExpression valueSetElimWidening(BooleanExpression context,
 SymbolicExpression vst,
 SymbolicExpression elimExpr,
 SymbolicExpression lower,
 SymbolicExpression upper)

setLogicFunctions

void setLogicFunctions(ProverFunctionInterpretation[] logicFunctions)

Set a list of logic functions with their definitions to the universe so that Reasoners created by this universe can take use of the definitions of the given logic functions.

Logic functions are instances of ProverFunctionInterpretations

Parameters:

logicFunctions - an array of ProverFunctionInterpretations