Module dev.civl.sarl

Package dev.civl.sarl.preuniverse.IF

Interface PreUniverse

All Superinterfaces:

CoreUniverse

public interface PreUniverse
extends CoreUniverse

A PreUniverse provides most of the services of a SymbolicUniverse, but not those that require reasoning, specifically theorem proving and simplification. The functionality of a symbolic universe is partitioned in this way to provide a hierarchical design to SARL. The simplification/proving modules require the basic symbolic algebra services provided by a PreUniverse . A full SymbolicUniverse requires the simplification and proving modules. A hierarchy in the USES relation is achieved.

Nested Class Summary

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

CoreUniverse.ForallStructure

Method Summary

Modifier and Type	Method	Description
CharObject	charObject(char value)	Returns the charObject wrapping the given char value.
SymbolicExpression	cleanBoundVariables(SymbolicExpression expr)	Changes the names of the bound variables in the expression so that every bound variable has a unique name.
UnaryOperator<SymbolicExpression>	cloneBoundCleaner(UnaryOperator<SymbolicExpression> boundCleaner)
void	incrementProverValidCount()
void	incrementValidCount()
UnaryOperator<SymbolicExpression>	newMinimalBoundCleaner()	Produces a new object for renaming bound variables in a minimal way.
ObjectFactory	objectFactory()	Returns the ObjectFactory used by this universe.
SymbolicTypeFactory	typeFactory()	Returns the SymbolicTypeFactory used by this universe.
SymbolicTypeSequence	typeSequence(Iterable<? extends SymbolicType> types)	Given an iterable collection of SymbolicTypes, returns a SymbolicTypeSequence conatining those SymbolicTypes

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

charObject

CharObject charObject(char value)

Returns the charObject wrapping the given char value. These are SARL char, not Java char.

Parameters:

value - a SARL char

Returns:

the CharObject wrapping that char

incrementValidCount

void incrementValidCount()

incrementProverValidCount

void incrementProverValidCount()

typeSequence

SymbolicTypeSequence typeSequence(Iterable<? extends SymbolicType> types)

Given an iterable collection of SymbolicTypes, returns a SymbolicTypeSequence conatining those SymbolicTypes

Parameters:

SymbolicType - - types

Returns:

SymbolicTypeSequence of SymbolicType - types

objectFactory

ObjectFactory objectFactory()

Returns the ObjectFactory used by this universe. This is the factory used for producing SymbolicObjects and performing basic manipulations of them.

Returns:

the object factory used by this universe

typeFactory

SymbolicTypeFactory typeFactory()

Returns the SymbolicTypeFactory used by this universe. This is the factory used for producing SymbolicTypes and performing basic manipulations on them.

Returns:

the type factory used by this universe

cleanBoundVariables

SymbolicExpression cleanBoundVariables(SymbolicExpression expr)

Changes the names of the bound variables in the expression so that every bound variable has a unique name. The names will be unique among ALL bound variables ever encountered by this method in this preuniverse.

Parameters:

expr - a symbolic expressions

Returns:

a symbolic expression equivalent to expr but with the names of the bound variables possibly changed to be unique

newMinimalBoundCleaner

UnaryOperator<SymbolicExpression> newMinimalBoundCleaner()

Produces a new object for renaming bound variables in a minimal way. Bound variables will only be renamed if it is necessary to prevent conflict with a free variable.

Returns:

new bound cleaner with empty state

cloneBoundCleaner

UnaryOperator<SymbolicExpression> cloneBoundCleaner(UnaryOperator<SymbolicExpression> boundCleaner)