Module dev.civl.sarl
Package dev.civl.sarl.IF

Interface CoreUniverse

All Known Subinterfaces:
PreUniverse, SymbolicUniverse
public interface CoreUniverse
A CoreUniverse provides most of the functionality of a SymbolicUniverse, including the mechanisms to create and manipulate SymbolicExpressions and other SymbolicObjects. The part that is missing deals with "reasoning", i.e., the ability to determine the validity of formulas and to simplify expressions within a "context".

  • Method Details

    • getUseBackwardSubstitution

      boolean getUseBackwardSubstitution()
      Shall the Reasoners generated by this universe use backwards substitution when simplifying, in order to solve for certain numeric expressions in terms of others?
      Returns:
      the value of the "useBackwardSubstitution" flag

    • setUseBackwardSubstitution

      void setUseBackwardSubstitution(boolean value)
      Sets the value of the "useBackwardSubstitution" flag. If true, the Reasoners generated by this universe will use backwards substitution when simplifying, in order to solve for certain numeric expressions in terms of others.
      Parameters:
      value - the new value for the "useBackwardSubstitution" flag

    • getShowQueries

      boolean getShowQueries()
      Gets the showQueries flag: if true, SARL theorem prover queries will be printed to the output stream.
      Returns:
      current value of the showQueries flag
      See Also:

    • setShowQueries

      void setShowQueries(boolean value)
      Sets the showQueries flag. If this is set to true, SARL theorem prover queries will be printed to the output stream.
      Parameters:
      value - new value for the showQueries flag.
      See Also:

    • getShowProverQueries

      boolean getShowProverQueries()
      Gets the showProverQueries flag: if true, the theorem prover queries processed by the underlying theorem prover(s) will be printed to the output stream.
      Returns:
      current value of the showProverQueries flag
      See Also:

    • setShowProverQueries

      void setShowProverQueries(boolean value)
      Sets the showProverQueries flag. If set to true , the theorem prover queries processed by the underlying theorem prover(s) will be printed to the output stream.
      Parameters:
      value - new value for the showProverQueries flag
      See Also:

    • getOutputStream

      PrintStream getOutputStream()
      Returns the output stream to which information (such as queries) will be printed. By default, standard out.
      Returns:
      current output stream
      See Also:

    • setOutputStream

      void setOutputStream(PrintStream out)
      Sets the output stream, the stream to which information (such as queries) will be printed. By default, standard out.
      Parameters:
      out - new value for output stream
      See Also:

    • comparator

      Comparator<SymbolicObject> comparator()
      Returns a comparator on the set of all symbolic objects. This defines a total order on all symbolic objects.
      Returns:
      a comparator on all symbolic objects

    • numObjects

      int numObjects()
      Returns the number of canonic symbolic objects controlled by this universe.
      Returns:
      the number of canonic symbolic objects

    • objectWithId

      SymbolicObject objectWithId(int id)

      Gets the canonic SymbolicObject belonging to this universe with the given ID number.

      Each canonic symbolic object is assigned a unique ID number. The numbers start from 0 and there are no gaps, i.e., they are in the range 0..numExpressions-1.

      Parameters:
      id - the ID number of a SymbolicObject belonging to this universe
      Returns:
      the canonic symbolic object with the given ID number.

    • getProbabilisticBound

      RationalNumber getProbabilisticBound()
      The upper bound on the probability of error when deciding whether a polynomial is 0. Must be a rational number in [0,1). If 0, probabilistic techniques are not used. In general, this should be a very small positive number.
      Returns:
      the current upper bound on probability of error

    • setProbabilisticBound

      void setProbabilisticBound(RationalNumber epsilon)
      Sets the upper bound on the probability of error when deciding whether a polynomial is 0. Must be a rational number in [0,1). If 0, probabilistic techniques are not used. In general, this should be a very small positive number.
      Parameters:
      epsilon - the new upper bound on probability of error that should be used from this point forward, a rational number in [0,1)

    • compatible

      BooleanExpression compatible(SymbolicType type0, SymbolicType type1)
      Returns a boolean expression which holds iff the two types are compatible. Two types are compatible if it is possible for them to have a value in common. For the most part, this is the same as saying they are the same type. The exception is that an incomplete SymbolicArrayType and a SymbolicCompleteArrayType with compatible element types are compatible.
      Parameters:
      type0 - a non-null symbolic type
      type1 - a non-null symbolic type
      Returns:
      a boolean expression which holds iff the two types are compatible
      See Also:

    • pureType

      SymbolicType pureType(SymbolicType type)
      Returns the "pure" version of the type, i.e., the compatible SymbolicType that contains no SymbolicExpressions. It is obtained by making every array type incomplete, i.e., by removing the length expressions from complete array types. This is applied recursively down all components of the type tree.
      See Also:

    • booleanType

      SymbolicType booleanType()
      The boolean type.
      Returns:
      the boolean type

    • integerType

      SymbolicIntegerType integerType()
      The "ideal" integer type, representing the set of mathematical integers.
      Returns:
      the integer type
      See Also:

    • herbrandIntegerType

      SymbolicIntegerType herbrandIntegerType()

      Returns the Herbrand integer type. All operations in which at least one argument has Herbrand integer type will be treated as uninterpreted functions: no simplifications or other transformations will be performed.

      Note: to create a concrete number of Herbrand integer type, create an ideal concrete integer then cast it to the Herbrand type.

      Returns:
      the Herbrand integer type
      See Also:

    • boundedIntegerType

      SymbolicIntegerType boundedIntegerType(NumericExpression min, NumericExpression max, boolean cyclic)

      Returns the bounded integer types with specified upper and lower bounds. Either of the bounds may be null, indicating there is no bound (i.e., the bound is + or - infinity). If cyclic is true, then all operations treat the domain cyclically (i.e., max+1 = min).

      NOTE: THIS IS NOT YET IMPLEMENTED.

      Parameters:
      min - smallest integer value in the domain or null
      max - largest integer value in the domain or null
      cyclic - should operations treat the domain cyclically?
      Returns:
      the bounded integer type as specified
      See Also:

    • realType

      SymbolicRealType realType()
      The "ideal" real type, representing the set of mathematical real numbers.
      Returns:
      the real type
      See Also:

    • herbrandRealType

      SymbolicRealType herbrandRealType()

      Returns the Herbrand real type. All operations in which at least one argument has Herbrand real type will be treated as uninterpreted functions: no simplifications or other transformations will be performed. Operations may involve mixed real and Herbrand real types, but the result will always be a Herbrand expression as long as at least one argument is Herbrand.

      A Herbrand value and non-Herbrand value are always considered to be not equal, even if they are concrete expressions.

      Note: to create a concrete number of herbrand real type, create an ideal concrete real then cast it to the herbrand type.

      Returns:
      the Herbrand real type
      See Also:

    • characterType

      SymbolicType characterType()
      Returns the character type.
      Returns:
      the character type

    • arrayType

      SymbolicCompleteArrayType arrayType(SymbolicType elementType, NumericExpression extent)
      Returns the complete array type with the given element type and extent (array length). Neither argument can be null.
      Parameters:
      elementType - the type of the elements of the array
      extent - length of the array
      Returns:
      the complete array type as specified
      See Also:

    • arrayType

      SymbolicArrayType arrayType(SymbolicType elementType)
      Returns the incomplete array type with the given element type. The element type cannot be null.
      Returns:
      the incomplete array type
      See Also:

    • arrayDimensionAndBaseType

      dev.civl.sarl.util.Pair<Integer,SymbolicType> arrayDimensionAndBaseType(SymbolicArrayType type)

      Returns the dimension and base type of an array type.

      The dimension and base type of an array type T[] are defined as follows: if T is an array type, the dimension of T[] is one plus the dimension of T, and the base type of T[] is the base type of T . Otherwise, the dimension of T[] is 1 and the base type is T.

      Parameters:
      type - a non-null array type
      Returns:
      A Pair consisting of dimension (left) and base type (right).

    • tupleType

      SymbolicTupleType tupleType(StringObject name, Iterable<? extends SymbolicType> fieldTypes)
      Returns the tuple type defined by the given sequence of component types. The tuple type consists of all tuples of values (x0, ..., xn-1), where xi has type fieldsTypesi. A tuple type also has a name, and two tuple types are not equal if they have unequal names.
      Parameters:
      name - the name of the tuple type
      fieldTypes - an iterable object specifying the sequence of component types for the tuple type
      Returns:
      the tuple type specified by the given name and field types

    • functionType

      SymbolicFunctionType functionType(Iterable<? extends SymbolicType> inputTypes, SymbolicType outputType)
      Returns the specified function type. A function type is specified by a sequence of input types, and an output type.
      Parameters:
      inputTypes - sequence of input types
      outputType - the output type of the function
      Returns:
      the function type

    • functionType

      SymbolicFunctionType functionType(Iterable<? extends SymbolicType> inputTypes, SymbolicType outputType, SymbolicFunctionType.SpecialRelationKind relKind)
      Returns the specified function type. A function type is specified by a sequence of input types, and an output type.
      Parameters:
      inputTypes - sequence of input types
      outputType - the output type of the function
      relKind - the special relation kind if this function represents such a relation
      Returns:
      the function type

    • unionType

      SymbolicUnionType unionType(StringObject name, Iterable<? extends SymbolicType> memberTypes)

      Returns the type which is the union of the given member types.

      Say the member types are t0,...,tn-1 and call the union type u. For 0 ≤ i < n, there are functions injecti: ti → u, extracti: u → ti, and testi: u → {true,false}. The domain of u consists of all expressions of the form injecti(xi).

      We have extracti(injecti(x))=x and extracti is undefined on any element of u that is not in the image of injecti. testi(x) is true iff x=injecti(xi) for some xi in ti.

      Parameters:
      name - the name of the union type
      memberTypes - the sequence of member types
      Returns:
      the specified union type

    • setType

      SymbolicSetType setType(SymbolicType elementType)
      Returns the type for "set of T"; not yet implemented.
      Parameters:
      elementType - type of elements of the set
      Returns:
      the type "set of elementType"

    • mapType

      SymbolicMapType mapType(SymbolicType keyType, SymbolicType valueType)
      Under construction.
      Parameters:
      keyType -
      valueType -
      Returns:

    • entryType

      SymbolicTupleType entryType(SymbolicMapType mapType)
      Returns a tuple type which has two components: component 0 is the key type of the map type; component 1 is the value type of the map type. This is the type of an "entry" in the map. This type is used by the method entrySet(SymbolicExpression), which returns the set of entries of a map.
      Parameters:
      mapType - a map type
      Returns:
      the type of an entry in the map

    • symbolicUninterpretedType

      SymbolicUninterpretedType symbolicUninterpretedType(String name)
      Returns an uninterpreted type which is an instance of SymbolicUninterpretedType.
      Parameters:
      name - the name of the returning uninterpreted type
      Returns:
      an instance of SymbolicUninterpretedType whose name is the given String.

    • mapSubstituter

      UnaryOperator<SymbolicExpression> mapSubstituter(Map<SymbolicExpression,SymbolicExpression> map)
      Returns a substituter for which the base substitutions are specified by an explicit Java Map. The map specifies a set of key-value pairs. The substituter will replace any key with its corresponding value; all other substitutions are determined from those "base" cases by recursive application of substitution.
      Parameters:
      map - a map which specifies that a key should be replaced by the corresponding value
      Returns:
      a substituter based on the given map

    • mapSubstituter

      UnaryOperator<SymbolicExpression> mapSubstituter(UnaryOperator<SymbolicExpression> operator)

    • constantSubstituter

      UnaryOperator<SymbolicExpression> constantSubstituter(Map<SymbolicConstant,SymbolicExpression> map)
      Returns a substituter for which the base substitutions are specified by an explicit Java Map. The map specifies a set of key-value pairs. The substituter will replace any key with its corresponding value; all other substitutions are determined from those "base" cases by recursive application of substitution.
      Parameters:
      map - a map which specifies that a key should be replaced by the corresponding value
      Returns:
      a substituter based on the given map

    • nameSubstituter

      UnaryOperator<SymbolicExpression> nameSubstituter(Map<StringObject,StringObject> nameMap)
      Returns a substituter specified by a mapping of old names to new names for symbolic constants. Any symbolic constant appearing as a key in the map will be replaced by a similar one with name the corresponding value. This includes bound symbolic constants.
      Parameters:
      nameMap - mapping of old to new names for symbolic constants
      Returns:
      a substituter which replaces symbolic constants as specified by nameMap

    • simpleSubstituter

      UnaryOperator<SymbolicExpression> simpleSubstituter(SymbolicConstant var, SymbolicExpression value)
      Returns a substituter that replaces a specific symbolic constant with some specific value. The value must have a type that is compatible with that of the symbolic constant.
      Parameters:
      var - the symbolic constant
      value - the value that will replace the symbolic constant
      Returns:
      a substituter that will replace any occurrence of var with value

    • canonicalRenamer

      CanonicalRenamer canonicalRenamer(String root, Predicate<SymbolicConstant> ignore)

      Returns an operator on SymbolicExpressions that replaces all symbolic constants (including bound ones) with symbolic constants with unique canonical names. The names are formed by appending the integers 0, 1, ..., to root. The renamer has state, so it can be used repeatedly (applied to multiple symbolic expressions) and will continue to generate new names for the new symbolic constants it encounters if they have not been encountered before. Every fresh binding of a bound variable is considered to be new, so is given a unique new name.

      The parameter ignore also provides a way to specify that certain symbolic constants should be ignored, i.e., they should not be renamed.

      Parameters:
      root - the string that forms the root of the names of the new symbolic constants
      ignore - a predicate providing a method that takes a SymbolicConstant and returns true or false; if it returns true, then that symbolic constant should not be renamed
      Returns:
      a unary operator which take a symbolic expression and returns a symbolic expression in which the symbolic constants have been assigned canonical names

    • canonicalRenamer

      CanonicalRenamer canonicalRenamer(String root)

      Returns an operator on SymbolicExpressions that replaces all symbolic constants (including bound ones) with symbolic constants with unique canonical names. The names are formed by appending the integers 0, 1, ..., to root. The renamer has state, so it can be used repeatedly (applied to multiple symbolic expressions) and will continue to generate new names for the new symbolic constants it encounters if they have not been encountered before. Every fresh binding of a bound variable is considered to be new, so is given a unique new name.

      Equivalent to invoking canonicalRenamer(String, Predicate) with ignore the constant predicate false.

      Parameters:
      root - the string that forms the root of the names of the new symbolic constants
      Returns:
      a unary operator which take a symbolic expression and returns a symbolic expression in which the symbolic constants have been assigned canonical names

    • make

      SymbolicExpression make(SymbolicExpression.SymbolicOperator operator, SymbolicType type, SymbolicObject[] arguments)
      Applies the given operator to the arguments and returns the resulting expression in the form used by this universe. The arguments should have the form required by the operator; see the documentation in the SymbolicExpression interface, especially for the SymbolicExpression.SymbolicOperators. The result returned should be identical to what would be returned by calling the specific methods (e.g., add(Iterable)).
      Parameters:
      operator - a symbolic operator
      type - the type which the resulting expression should have (since it may not be unambiguous)
      arguments - arguments which should be appropriate for the specified operator

    • numValidCalls

      int numValidCalls()
      Returns the total number of calls made to methods Reasoner.valid(BooleanExpression) and Reasoner.validOrModel(BooleanExpression).
      Returns:
      the total number of validity calls

    • numProverValidCalls

      int numProverValidCalls()
      Returns the total number of calls made to the validity method in the underlying automated theorem prover. This is in general smaller than that returned by numValidCalls(), as not every valid call requires a call to the prover.
      Returns:
      the total number of theorem prover validity calls

    • booleanObject

      BooleanObject booleanObject(boolean value)
      Returns the BooleanObject wrapping the given boolean value. A BooleanObject is a SymbolicObject, so can be used as an argument of a SymbolicExpression.
      Parameters:
      value - true or false, the boolean value to wrap
      Returns:
      the corresponding BooleanObject

    • intObject

      IntObject intObject(int value)
      Returns the IntObject wrapping the given Java int value. An IntObject is a SymbolicObject so can be used as an argument of a SymbolicExpression. It is used in cases where a "small" concrete integer is needed. For concrete integers of arbitrary size, use IntegerNumber instead and create a NumberObject .
      Parameters:
      value - any Java int
      Returns:
      an IntObject wrapping value

    • numberObject

      NumberObject numberObject(Number value)
      Returns the NumberObject wrapping the given Number value. These are SARL Numbers, not Numbers. They are used to represent infinite precision, unbounded integers and rational numbers.
      Parameters:
      value - a finite concrete SARL Number
      Returns:
      the NumberObject wrapping value

    • stringObject

      StringObject stringObject(String string)
      Returns the StringObject wrapping the given String value. A StringObject is a SymbolicObject so can be used as an argument to a SymbolicExpression.
      Parameters:
      string - any Java String
      Returns:
      the StringObject wrapping string

    • nullExpression

      SymbolicExpression nullExpression()
      Returns the "NULL" expression. This is a non-null (in the Java sense of "null") SymbolicExpression for which the method SymbolicExpression.isNull() returns true. Its type is null, and it has 0 arguments.
      Returns:
      the NULL expression

    • symbolicConstant

      SymbolicConstant symbolicConstant(StringObject name, SymbolicType type)

      Returns the SymbolicConstant with the given name and type. Two SymbolicConstants are equal iff they have the same name and type. This method may use a Flyweight Pattern to return the same object if called twice with the same arguments. Or it may create a new object each time. These details are unimportant because symbolic constants are immutable.

      This method will return the right kind of SymbolicConstant based on the type. For example, if the type is numeric ( SymbolicIntegerType or SymbolicRealType), an instance of NumericSymbolicConstant will be returned. If the type is boolean, a BooleanSymbolicConstant will be returned.

      Parameters:
      name - the name to give to this symbolic constant; it will be used to identify the object and for printing
      type - the type of the symbolic constant

    • zeroInt

      NumericExpression zeroInt()
      The symbolic expression representing the 0 integer value.
      Returns:
      the integer 0 as a numeric symbolic expression

    • oneInt

      NumericExpression oneInt()
      The symbolic expression representing the integer 1.
      Returns:
      the integer 1 as a numeric symbolic expression

    • integer

      NumericExpression integer(int value)
      Returns the integer symbolic expression with the given int value.
      Parameters:
      value - a Java int
      Returns:
      the symbolic expression of integer type representing that concrete value

    • integer

      NumericExpression integer(long value)
      Returns the numeric symbolic expression with the given long value.
      Parameters:
      value - any Java long
      Returns:
      the symbolic expression of integer type with that value

    • integer

      NumericExpression integer(BigInteger value)
      Returns the numeric symbolic expression with the given BigInteger value. The BigInteger class is a standard Java class for representing integers of any size.
      Parameters:
      value - any BigInteger
      Returns:
      the symbolic expression of integer type with that value

    • zeroReal

      NumericExpression zeroReal()
      Returns the symbolic expression representing the real number 0. Note that this is NOT equal to the integer number 0, since they have different types.
      Returns:
      the real number 0 as a symbolic expression

    • oneReal

      NumericExpression oneReal()
      Returns the symbolic expression representing the real number 1.
      Returns:
      the real number 1 as a symbolic expression

    • rational

      NumericExpression rational(int value)
      Returns the symbolic expression of real type (SymbolicRealType) representing the given int value. This is sometimes referred to as a "rational integer".
      Parameters:
      value - an Java int
      Returns:
      a concrete rational representation of this integer value; essentially, the rational number (value/1)

    • rational

      NumericExpression rational(long value)
      Returns the symbolic expression of real type (SymbolicRealType) representing the given long value. This is sometimes referred to as a "rational integer".
      Parameters:
      value - a Java long
      Returns:
      a concrete rational representation of this long value; essentially the rational number (value/1)

    • rational

      NumericExpression rational(BigInteger value)
      Returns the symbolic expression of real type (SymbolicRealType) representing the given BigInteger value. This is sometimes referred to as a "rational integer"
      Parameters:
      value - a Java BigInteger
      Returns:
      a concrete rational representation of this BigInteger value; essentially, the rational number (value/1)

    • rational

      NumericExpression rational(float value)
      Returns the symbolic expression of real type (SymbolicRealType) representing the given float value.
      Parameters:
      value - a Java float
      Returns:
      a concrete rational representation of this float value

    • rational

      NumericExpression rational(double value)
      Returns the symbolic expression of real type (SymbolicRealType) representing the given double value.
      Parameters:
      value - a Java double
      Returns:
      a concrete symbolic expression of real type representing the value

    • rational

      NumericExpression rational(int numerator, int denominator)
      Returns the rational number obtained by dividing two integers, numerator and denominator. The result is a symbolic expression of SymbolicRealType. Note that this universe is free to transform the expression into an equivalent form, for example, by canceling any common factors.
      Parameters:
      numerator - a Java int
      denominator - a non-0 Java int
      Returns:
      the real number formed by dividing numerator by denominator, as a symbolic expression of real type

    • rational

      NumericExpression rational(long numerator, long denominator)
      Returns the rational number obtained by dividing two long integers. The result will have SymbolicRealType.
      Parameters:
      numerator - a Java long
      denominator - a non-0 Java long
      Returns:
      the real number formed by dividing numerator by denominator, as a NumericExpression

    • rational

      NumericExpression rational(BigInteger numerator, BigInteger denominator)
      Returns the rational number obtained by dividing two BigIntegers. The result will have SymbolicRealType.
      Parameters:
      numerator - an integer, the numerator
      denominator - a non-0 integer, the denominator
      Returns:
      the rational number formed by dividing numerator by denominator, as a symbolic expression

    • numberFactory

      NumberFactory numberFactory()
      Returns the number factory used by this universe.
      Returns:
      the number factory used by this universe

    • number

      NumericExpression number(Number number)
      Returns the concrete symbolic expression wrapping the given number. The type of the expression will be the "ideal" SymbolicIntegerType if number is an IntegerNumber, or the "ideal" SymbolicRealType if number is a RationalNumber.
      Parameters:
      number - any non-null finite SARL Number
      Returns:
      the concrete symbolic expression wrapping that number
      See Also:

    • number

      NumericExpression number(NumberObject numberObject)
      Returns the concrete symbolic expression wrapping the given number object. The type of the expression will be the "ideal" SymbolicIntegerType if numberObject.getNumber() is an IntegerNumber, or the "ideal" SymbolicRealType if it is a RationalNumber.
      Parameters:
      numberObject - any non-null NumberObject
      See Also:

    • extractNumber

      Number extractNumber(NumericExpression expression)
      Returns the Number value if the given symbolic expression has a concrete numerical value, else returns null.
      Parameters:
      expression - any non-null numeric expression
      Returns:
      the Number value or null

    • character

      SymbolicExpression character(char theChar)
      Returns a concrete symbolic expression of character type which wraps the given Java char.
      Parameters:
      theChar - the Java char
      Returns:
      symbolic expression wrapping theChar
      See Also:

    • extractCharacter

      Character extractCharacter(SymbolicExpression expression)
      If the given expression is a concrete character expression, this returns the character value, else it returns null.
      Parameters:
      expression - a symbolic expression
      Returns:
      the character it wraps or null
      See Also:

    • stringExpression

      SymbolicExpression stringExpression(String theString)
      Returns a symbolic expression of type array-of-char which is a literal array consisting of the sequence of characters in the given string.
      Parameters:
      theString - a Java string
      Returns:
      theString represented as a symbolic expression of type array-of-char
      See Also:

    • add

      NumericExpression add(NumericExpression arg0, NumericExpression arg1)
      Returns a symbolic expression which is the result of adding the two given symbolic expressions. The two given expressions must have the same (numeric) type: either both integers, or both real.
      Parameters:
      arg0 - a symbolic expression of a numeric type
      arg1 - a symbolic expression of the same numeric type
      Returns:
      the sum arg0+arg1
      See Also:

    • add

      NumericExpression add(Iterable<? extends NumericExpression> args)
      Returns a symbolic expression representing the sum of the given argument sequence.
      Parameters:
      args - a sequence of symbolic expressions of numeric type. They must all have the same type.
      Returns:
      expression representing the sum
      See Also:

    • subtract

      NumericExpression subtract(NumericExpression arg0, NumericExpression arg1)
      Returns a symbolic expression which is the result of subtracting arg1 from arg0. The two given expressions must have the same (numeric) type: either both integers, or both real.
      Parameters:
      arg0 - a symbolic expression of a numeric type
      arg1 - a symbolic expression of the same numeric type
      Returns:
      the difference, arg0-arg1
      See Also:

    • sigma

      NumericExpression sigma(NumericExpression low, NumericExpression high, SymbolicExpression function)
      A fold sum expression. Takes three arguments: low, high and a function f: int-to-T. The expression means f(low) + f(low + 1) + ... + f(high - 1)
      Parameters:
      low - The lower bound of the integer set (inclusive)
      high - The higher bound of the integer set (exclusive)
      function - An expression representing the set of addends of the summation expression. It must have a function type t. t must have an integer input type. The output type is the type of the summation expression.
      Returns:

    • reduction

      SymbolicExpression reduction(SymbolicExpression[] operands, NumericExpression count, SymbolicExpression op, List<BooleanExpression> compatibleConditionsOutput)

      a $reduction function that takes a list of operands, the number of elements per operand and an operator, returns the element-wise reduction result of the operator over the operands.

      Parameters:
      operands - a list of operands
      count - the number of elements in each operand
      op - an integer value representing the reduction operator
      compatibleConditionsOutput - output argument, containing compatible conditions, if any of the given compatible conditions fails, the returned result is invalid
      Returns:
      the element-wise reduction result of given operator over the operands, if the output compatibale conditions are all valid.

    • isSigmaCall

      boolean isSigmaCall(SymbolicExpression expr)

    • permut

      BooleanExpression permut(SymbolicExpression array_a, SymbolicExpression array_b, NumericExpression low, NumericExpression high)
      A permutation predicate, which asserts the slice from lower index low to higher index high in array array_a is a permutation of the slice from lower index low to higher index high in array array_b.
      Parameters:
      array_a -
      array_b -
      low -
      high -
      Returns:
      an instance of the permutation predicate

    • isPermutCall

      boolean isPermutCall(SymbolicExpression expr)

    • multiply

      NumericExpression multiply(NumericExpression arg0, NumericExpression arg1)
      Returns a symbolic expression which is the result of multiplying the two given symbolic expressions. The two given expressions must have the same (numeric) type: either both integers, or both real.
      Parameters:
      arg0 - a symbolic expression of a numeric type
      arg1 - a symbolic expression of the same numeric type
      Returns:
      arg0 * arg1, the product of arg0 and arg1.
      See Also:

    • multiply

      NumericExpression multiply(Iterable<? extends NumericExpression> args)
      Returns symbolic expression representing the product of the given sequence of expressions.
      Parameters:
      args - symbolic expression sequence; all elements have the same numeric type
      Returns:
      a symbolic expression representing the product
      See Also:

    • divide

      NumericExpression divide(NumericExpression arg0, NumericExpression arg1) throws ArithmeticException

      Returns a symbolic expression which is the result of dividing arg0 by arg1. The two given expressions must have the same (numeric) type: either both integers, or both real. In the integer case, division is interpreted as "integer division", which rounds towards 0.

      For reference, here's what C11 (Sec. 6.5.5) says about integer division: 

       The result of the / operator is the quotient from the
 division of the first operand by the second; the result
 of the % operator is the remainder. In both operations,
 if the value of the second operand is zero, the behavior
 is undefined.

 When integers are divided, the result of the / operator
 is the algebraic quotient with any fractional part discarded.
 [This is often called "truncation toward zero".]
 If the quotient a/b is representable, the expression
 (a/b)*b + a%b shall equal a; otherwise, the behavior
 of both a/b and a%b is undefined.

      Hence in C, a%b=a-(a/b)*b. Examples:

      • a=4, b=3: a/b=1, a%b=4-3=1
      • a=4, b=-3: a/b=-1, a%b=4-(-1)(-3)=1
      • a=-4, b=3: a/b=-1, a%b=-4-(-1)3=-1
      • a=-4, b=-3: a/b=1, a%b=-4-1(-3)=-1

      Note that the sign of a/b is the same for integer or real division, i .e., sign(a/b)=sign(a)*sign(b). The sign of a%b is sign(a).

      Parameters:
      arg0 - a symbolic expression of a numeric type
      arg1 - a symbolic expression of the same numeric type
      Returns:
      the quotient, arg0 / arg1
      Throws:
      ArithmeticException - If there is a division by zero.
      See Also:

    • modulo

      NumericExpression modulo(NumericExpression arg0, NumericExpression arg1) throws ArithmeticException
      Returns a symbolic expression which represents arg0 modulo arg1. The two given expressions must have the integer type.
      Parameters:
      arg0 - a symbolic expression of integer type
      arg1 - a symbolic expression of integer type
      Returns:
      the modulus, arg0 % arg1
      Throws:
      ArithmeticException - If there is a division by zero.
      See Also:

    • minus

      NumericExpression minus(NumericExpression arg)
      Returns a symbolic expression which is the negative of the given numerical expression. The given expression must be non-null and have either integer or real type.
      Parameters:
      arg - a symbolic expression of integer or real type
      Returns:
      negation: − arg
      See Also:

    • power

      NumericExpression power(NumericExpression base, IntegerNumber exponent)
      Concrete power operator: eb, where b is a concrete non-negative IntegerNumber. This method might actually multiply out the expression, i.e., it does not necessarily return an expression with operator SymbolicExpression.SymbolicOperator.POWER.
      Parameters:
      base - the base expression in the power expression
      exponent - a finite non-negative concrete integer exponent

    • power

      NumericExpression power(NumericExpression base, int exponent)
      Equivalent to power(base, intObject(exponent)).
      Parameters:
      base - the base expression in the power expression
      exponent - a non-negative concrete integer exponent
      Returns:
      power(base, intObject(exponent))

    • power

      NumericExpression power(NumericExpression base, NumericExpression exponent)
      General power operator: eb. Both e and b are numeric expressions.
      Parameters:
      base - the base expression in the power expression
      exponent - the exponent in the power expression

    • extractBoolean

      Boolean extractBoolean(BooleanExpression expression)
      If the given expression has a concrete Boolean value, this returns it, else it returns null.
      Parameters:
      expression - any BooleanExpression
      Returns:
      one of the two concrete Boolean values if expression is concrete, else null

    • trueExpression

      BooleanExpression trueExpression()
      Returns the boolean literal true.
      Returns:
      the symbolic expression true

    • falseExpression

      BooleanExpression falseExpression()
      Returns the boolean literal false.
      Returns:
      the symbolic expression false

    • bool

      BooleanExpression bool(BooleanObject object)
      The symbolic expression wrapping the given boolean object (true or false).

    • bool

      BooleanExpression bool(boolean value)
      Short cut for symbolic(booleanObject(value)).
      Parameters:
      value -
      Returns:
      symbolic expression wrapping boolean value

    • and

      BooleanExpression and(BooleanExpression arg0, BooleanExpression arg1)
      Returns a symbolic expression representing the conjunction of the two given arguments. Each argument must be non-null and have boolean type.
      Parameters:
      arg0 - a symbolic expression of boolean type
      arg1 - a symbolic expression of boolean type
      Returns:
      conjunction of arg0 and arg1

    • and

      BooleanExpression and(Iterable<? extends BooleanExpression> args)
      Returns a symbolic expression which represents the conjunction of the expressions in the given array args. Each expression in args must have boolean type. args must be non-null, and may have any length, including 0. If the length of args is 0, the resulting expression is equivalent to "true".
      Parameters:
      args - a sequence of expressions of boolean type
      Returns:
      the conjunction of the expressions in args

    • or

      BooleanExpression or(BooleanExpression arg0, BooleanExpression arg1)
      Returns a symbolic expression representing the disjunction of the two given arguments. Each argument must be non-null and have boolean type.
      Parameters:
      arg0 - a symbolic expression of boolean type
      arg1 - a symbolic expression of boolean type
      Returns:
      disjunction of arg0 and arg1

    • or

      BooleanExpression or(Iterable<? extends BooleanExpression> args)
      Returns a symbolic expression which represents the disjunction of the expressions in the given array args. Each expression in args must have boolean type. args must be non-null, and may have any length, including 0. If the length of args is 0, the resulting expression is equivalent to "false".
      Parameters:
      args - a sequence of expressions of boolean type
      Returns:
      the disjunction of the expressions in args

    • not

      BooleanExpression not(BooleanExpression arg)
      Returns a symbolic expression representing the logical negation of the given expression arg. arg must be non-null and have boolean type.
      Parameters:
      arg - a symbolic expression of boolean type
      Returns:
      negation of arg

    • implies

      BooleanExpression implies(BooleanExpression arg0, BooleanExpression arg1)
      Returns a symbolic expression representing "p implies q", i.e., p=>q.
      Parameters:
      arg0 - a symbolic expression of boolean type (p)
      arg1 - a symbolic expression of boolean type (q)
      Returns:
      p=>q

    • equiv

      BooleanExpression equiv(BooleanExpression arg0, BooleanExpression arg1)
      Returns a symbolic expression representing "p is equivalent to q", i.e., pinvalid input: '<'=>q.
      Parameters:
      arg0 - a symbolic expression of boolean type (p)
      arg1 - a symbolic expression of boolean type (q)
      Returns:
      pinvalid input: '<'=>q

    • lessThan

      BooleanExpression lessThan(NumericExpression arg0, NumericExpression arg1)
      Returns expression equivalent to arg0 invalid input: '<' arg1. The arguments must be numeric of the same type (i.e., both are of integer type or both are of real type).
      Parameters:
      arg0 - symbolic expression of numeric type
      arg1 - symbolic expression of same numeric type
      Returns:
      symbolic expression of boolean type arg0 invalid input: '<' arg1

    • lessThanEquals

      BooleanExpression lessThanEquals(NumericExpression arg0, NumericExpression arg1)
      Returns expression equivalent to arg0 invalid input: '<'= arg1 ("less than or equal to"). The arguments must be numeric of the same type (i.e., both are of integer type or both are of real type).
      Parameters:
      arg0 - symbolic expression of numeric type
      arg1 - symbolic expression of same numeric type
      Returns:
      symbolic expression of boolean type arg0 invalid input: '<'= arg1

    • equals

      BooleanExpression equals(SymbolicExpression arg0, SymbolicExpression arg1)
      Returns expression equivalent to arg0 = arg1 ("equals"). This is a general equals operator (not just for numeric expressions). To be equal, the arguments must have equal types. The notion of equals then depends on the particular type.
      Parameters:
      arg0 - a symbolic expression
      arg1 - a symbolic expression
      Returns:
      symbolic expression of boolean type arg0 = arg1

    • quickEquals

      BooleanExpression quickEquals(SymbolicExpression arg0, SymbolicExpression arg1)

    • neq

      BooleanExpression neq(SymbolicExpression arg0, SymbolicExpression arg1)
      Returns expression equivalent to arg0 != arg1 ("not equals").
      Parameters:
      arg0 - a symbolic expression
      arg1 - a symbolic expression
      Returns:
      symbolic expression of boolean type arg0 != arg1

    • removeQuantifiers

      BooleanExpression removeQuantifiers(BooleanExpression arg)
      Returns arg with all clauses containing quantifers removed.
      Parameters:
      arg - a symbolic expression
      Returns:
      the conjunction of all quantifer-free clauses of arg.

    • forall

      BooleanExpression forall(SymbolicConstant boundVariable, BooleanExpression predicate)
      Returns the universally quantified expression forall(x).e.
      Parameters:
      boundVariable - the bound variable x
      predicate - the expression e (of boolean type)
      Returns:
      the expression forall(x).e

    • forallInt

      BooleanExpression forallInt(NumericSymbolicConstant index, NumericExpression low, NumericExpression high, BooleanExpression predicate)
      A special case of "forall" that is very common: forall integers i such that lowinvalid input: '<'=iinvalid input: '<'high, p(i).
      Parameters:
      index - i, a symbolic constant of integer type
      low - a symbolic expression of integer type, lower bound of i (inclusive)
      high - a symbolic expression of integer type, upper bound of i (exclusive)
      predicate - some boolean symbolic expression, usually involving i
      Returns:
      an expression equivalent to "forall int i. lowinvalid input: '<'=iinvalid input: '<'high -> p(i)".

    • exists

      BooleanExpression exists(SymbolicConstant boundVariable, BooleanExpression predicate)
      Returns the existentially quantified expression exists(x).e.
      Parameters:
      boundVariable - the bound variable x
      predicate - the expression e (of boolean type)
      Returns:
      the expression exists(x).e

    • existsInt

      BooleanExpression existsInt(NumericSymbolicConstant index, NumericExpression low, NumericExpression high, BooleanExpression predicate)
      A special case of "exists" that is very common: exists integer i such that lowinvalid input: '<'=iinvalid input: '<'high and p(i).
      Parameters:
      index - i, a symbolic constant of integer type
      low - a symbolic expression of integer type, lower bound of i (inclusive)
      high - a symbolic expression of integer type, upper bound of i (exclusive)
      predicate - some boolean symbolic expression, usually involving i
      Returns:
      an expression equivalent to "exists int i. lowinvalid input: '<'=iinvalid input: '<'high invalid input: '&'invalid input: '&' p(i)".

    • divides

      BooleanExpression divides(NumericExpression a, NumericExpression b)
      Does the integer a divide the integer b evenly? I.e, does there exist an integer n such that b=a*n?
      Parameters:
      a - a symbolic expression of integer type
      b - a symbolic expression of integer type
      Returns:
      a symbolic expression of boolean type holding iff a divides b

    • lambda

      SymbolicExpression lambda(SymbolicConstant boundVariable, SymbolicExpression expression)
      Returns the lambda expression lambda(x).e, i.e., the expression representing the function which given x returns e, where e might possibly involve the variable x. Note that x is a symbolic constant.
      Parameters:
      boundVariable - the bound variable x
      expression - the expression e
      Returns:
      lambda(x).e

    • apply

      SymbolicExpression apply(SymbolicExpression function, Iterable<? extends SymbolicExpression> argumentSequence)
      The result of applying an uninterpreted function to a sequence of arguments. The number and types of arguments must match the function's input signature.

    • unionInject

      SymbolicExpression unionInject(SymbolicUnionType unionType, IntObject memberIndex, SymbolicExpression object)
      Casts an object belonging to one of the members of a union type to the union type.
      Parameters:
      unionType - the union type
      memberIndex - the index of the member type of the object in the list of member types of the union type
      object - an expression whose type is the member type with the given index
      Returns:
      an expression whose type is the union type representing the same object as the given object

    • unionTest

      BooleanExpression unionTest(IntObject memberIndex, SymbolicExpression object)
      Tests whether an object of a union type is in the image of injection from the member type of the given index.
      Parameters:
      memberIndex - an integer in range [0,n-1], where n is the number of member types of the union type
      object - an expression of the union type
      Returns:
      a boolean expression telling whether the object belongs to the specified member type

    • unionExtract

      SymbolicExpression unionExtract(IntObject memberIndex, SymbolicExpression object)
      Casts an object whose type is a union type to a representation whose type is the appropriate member type of the union type. The behavior is undefined if the object does not belong to the specified member type.
      Parameters:
      memberIndex - an integer in range [0,n-1], where n is the number of member types of the union types
      object - an object whose type is the union type and for which unionTest(unionType, memberIndex, object) holds.
      Returns:
      a representation of the object with type the member type

    • array

      SymbolicExpression array(SymbolicType elementType, SymbolicExpression[] elements)

      Creates a concrete array expression backed by the given Java array. Any changes to the Java array will also change the returned expression, so the Java array should never be modified after this method is called.

      Precondition: every element of elements must have type elementType. This is not necessarily checked. If this condition is not met, behavior is undefined.

      Parameters:
      elementType - the type of each element of elements
      elements - array of symbolic expressions, each of type elementType
      Returns:
      symbolic expression of type SymbolicCompleteArrayType with element type elementType and length elements.length wrapping elements

    • array

      SymbolicExpression array(SymbolicType elementType, Iterable<? extends SymbolicObject> elements)
      Returns the concrete array consisting of given sequence of elements. The type of the array will be the complete array type determined by the element type and the number of elements.
      Parameters:
      elementType - the type of each element of the array
      elements - sequence of symbolic expressions
      Returns:
      array consisting of those elements

    • emptyArray

      SymbolicExpression emptyArray(SymbolicType elementType)
      Returns array of length 0.
      Parameters:
      elementType - the type of the non-existent elements of this array
      Returns:
      array of length 0 of given type

    • constantArray

      SymbolicExpression constantArray(SymbolicType elementType, NumericExpression length, SymbolicExpression value)
      Returns an array in which every element has the same value.
      Parameters:
      elementType - the element type of the array
      length - the length of the array
      value - the value of each element
      Returns:
      an array of specified length in which every element is value

    • append

      SymbolicExpression append(SymbolicExpression concreteArray, SymbolicExpression element)
      Appends an element to the end of a concrete symbolic array. Returns a new array expression which is same as old with new element appended to end. TODO: extend to arbitrary arrays, not just concrete
      Parameters:
      concreteArray - a concrete array
      element - a symbolic expression whose type is compatible with element type of the array
      Returns:
      an array obtained by appending element to given array

    • removeElementAt

      SymbolicExpression removeElementAt(SymbolicExpression concreteArray, int index)
      Removes an element in a specified position in a concrete symbolic array. Returns a new array which is same as old except the element has been removed and the remaining elements have been shifted down to remove the gap. The resulting array has length 1 less than the original one. TODO: extend to arbitrary arrays, not just concrete
      Parameters:
      concreteArray - a concrete array
      index - an int index
      Returns:
      array obtained by removing element at specified index
      Throws:
      SARLException - if index is negative or greater than or equal to the length of the given concrete array

    • insertElementAt

      SymbolicExpression insertElementAt(SymbolicExpression concreteArray, int index, SymbolicExpression value)
      Inserts value an position index in array, shifting subsequence elements "up".
      Parameters:
      concreteArray - a concrete array
      index - an int index in the range [0,length], where length is the length of the original array. If index=length, this is the same as append.
      value - expression to insert
      Returns:
      array obtained by inserting the element at specified index

    • length

      NumericExpression length(SymbolicExpression array)
      Returns the length of any symbolic expression of array type. This is a symbolic expression of integer type.
      Parameters:
      array - a symbolic expression of array type
      Returns:
      a symbolic expression of integer type representing the length of the array

    • arrayRead

      SymbolicExpression arrayRead(SymbolicExpression array, NumericExpression index)
      Returns an expression representing the value of the element of the array at position index. Arrays are indexed from 0. The expression returned has type the element type of the array.
      Parameters:
      array - the given array
      index - symbolic expression of integer type
      Returns:
      expression representing value of index-th element of the array

    • arrayWrite

      SymbolicExpression arrayWrite(SymbolicExpression array, NumericExpression index, SymbolicExpression value)
      Returns an expression representing the result of modifying an array by changing the value at position index. Arrays are indexed from 0. The expression returned has the same (array) type as the original array.
      Parameters:
      array - the given array
      index - symbolic expression of integer type
      value - the new value for the element at position index
      Returns:
      expression representing the result of changing the index-th element to value

    • denseArrayWrite

      SymbolicExpression denseArrayWrite(SymbolicExpression array, Iterable<? extends SymbolicExpression> values)
      Returns an array obtained by performing a sequence of writes, given in a "dense" format, to an array. The sequence of values are used to write to the indexes 0, 1, .... A null element in the sequence is simply ignored.
      Parameters:
      array - a symbolic expression of array type
      values - a sequence of symbolic expressions, each of which is either null or a symbolic expression of the appropriate type
      Returns:
      the array resulting from writing to the given array in position 0,...,n-1, where n is the length of the sequence.

    • arrayLambda

      SymbolicExpression arrayLambda(SymbolicCompleteArrayType arrayType, SymbolicExpression function)
      Returns an expression representing an array with element type T defined by a function f from int to T.

    • tuple

      SymbolicExpression tuple(SymbolicTupleType type, SymbolicExpression[] components)
      Returns the concrete tuple with the given members. This does NOT check that members have types compatible with the fields types of the tuple type. If they don't, the behavior is undefined.
      Parameters:
      type - the tuple type
      components - the component expressions
      Returns:
      the tuple formed from the components

    • tuple

      SymbolicExpression tuple(SymbolicTupleType type, Iterable<? extends SymbolicObject> components)
      Returns the concrete tuple expression with the given tuple components.
      Parameters:
      type - the tuple type
      components - the component expressions
      Returns:
      the tuple formed from the components

    • tupleRead

      SymbolicExpression tupleRead(SymbolicExpression tuple, IntObject index)
      Returns an expression that represents the result of reading a component in a tuple value. The index should be an integer-valued expression. The components are numbered starting from 0.
      Parameters:
      tuple - the tuple value being read
      index - index of the component to read
      Returns:
      a symbolic expression representing the component at that index

    • tupleWrite

      SymbolicExpression tupleWrite(SymbolicExpression tuple, IntObject index, SymbolicExpression value)
      Returns an expression representing the result of modifying a tuple by changing the value of one component. The component is specified by its index. The components are indexed starting from 0. In this method, the index is specified by a concrete Java int.
      Parameters:
      tuple - the original tuple
      index - the index of the component to modify
      value - the new value for the component
      Returns:
      an expression representing the new tuple

    • isSubsetOf

      BooleanExpression isSubsetOf(SymbolicExpression set1, SymbolicExpression set2)

    • setAdd

      SymbolicExpression setAdd(SymbolicExpression set, SymbolicExpression value)

    • setRemove

      SymbolicExpression setRemove(SymbolicExpression set, SymbolicExpression value)

    • setUnion

      SymbolicExpression setUnion(SymbolicExpression set1, SymbolicExpression set2)

    • setIntersection

      SymbolicExpression setIntersection(SymbolicExpression set1, SymbolicExpression set2)

    • setDifference

      SymbolicExpression setDifference(SymbolicExpression set1, SymbolicExpression set2)

    • cardinality

      NumericExpression cardinality(SymbolicExpression set)

    • emptyMap

      SymbolicExpression emptyMap(SymbolicMapType mapType)

    • put

      SymbolicExpression put(SymbolicExpression map, SymbolicExpression key, SymbolicExpression value)

    • get

      SymbolicExpression get(SymbolicExpression map, SymbolicExpression key)

    • removeEntryWithKey

      SymbolicExpression removeEntryWithKey(SymbolicExpression map, SymbolicExpression key)

    • keySet

      SymbolicExpression keySet(SymbolicExpression map)

    • mapSize

      NumericExpression mapSize(SymbolicExpression map)

    • entrySet

      SymbolicExpression entrySet(SymbolicExpression map)
      Returns the entry set of the map. This is the set consisting of all ordered pairs (key,value) for each entry in the map. Each entry is a symbolic expression which has a tuple type. The tuple type has two components: component 0 is the key type, component 1 the value type.
      Parameters:
      map -
      Returns:

    • cast

      SymbolicExpression cast(SymbolicType newType, SymbolicExpression expression)
      Casts expression to new type.
      Parameters:
      newType - a symbolic type
      expression - a symbolic expression
      Returns:
      symbolic expression cast to new type

    • cond

      SymbolicExpression cond(BooleanExpression predicate, SymbolicExpression trueCase, SymbolicExpression falseCase)
      "If-then-else" expression. Note that trueCase and falseCase must have the same type, which becomes the type of this expression.
      Parameters:
      predicate - the test condition p
      trueCase - the value if condition is true
      falseCase - the value if condition is false
      Returns:
      symbolic expression whose values is trueCase if predicate holds, falseCase if predicate is false

    • referenceType

      SymbolicType referenceType()

      Returns the type of all reference expressions. A reference expression is a kind of symbolic expression used to represent a reference to a subexpression of other expressions. It may be thought of as a sequence of directions for navigating to a particular node in a tree, starting from the root. For example, a reference expression r might encode "the 3rd element of the 2nd component". Given an expression e of tuple type in which the 2nd component has array type, that r specifies a particular element of a particular component of e.

      A reference may also be thought of as a function which takes a symbolic expression (of a compatible type) and returns a sub-expression of that expression.

      Returns:
      the type of all reference expressions

    • nullReference

      ReferenceExpression nullReference()
      Returns the "null reference", a symbolic expression of reference type which is not equal to a reference value returned by any of the other methods, and which cannot be dereferenced.
      Returns:
      the null reference

    • dereference

      SymbolicExpression dereference(SymbolicExpression value, ReferenceExpression reference)
      Given a reference and a value, returns the sub-expression of value specified by the reference. Throws exception if the reference is not of the correct form for the type of value.
      Parameters:
      value - a non-null symbolic expression
      reference - a non-null reference into a sub-expression of value
      Returns:
      the sub-expression of value specified by the reference

    • referencedType

      SymbolicType referencedType(SymbolicType type, ReferenceExpression reference)
      Returns the type referenced by a reference into an expression of the given type. Example: if type is array-of-integer and reference is an array element reference, this method returns integer.
      Parameters:
      type - a non-null symbolic type
      reference - a reference that is compatible with type, i.e., can reference into an expression of that type
      Returns:
      the component of the given type which is referenced by the given reference

    • identityReference

      ReferenceExpression identityReference()
      Returns the identity (or "trivial") reference I. This is the reference characterized by the property that dereference(I,v) returns v for any symbolic expression v.
      Returns:
      the identity reference

    • arrayElementReference

      ArrayElementReference arrayElementReference(ReferenceExpression arrayReference, NumericExpression index)
      Given a reference to an array and an index (integer), returns a reference to the element of the array at that index. Think of this as tacking on one more instruction to the sequence of directions specified by a reference. For example, if arrayReference encodes "2nd component of element 3" and index is X+Y, the result returned specifies "element X+Y of the 2nd component of element 3".
      Parameters:
      arrayReference - a non-null reference for which the referenced sub-expression has array type
      index - a non-null expression of integer type
      Returns:
      a reference to the index-th element of the referenced array

    • tupleComponentReference

      TupleComponentReference tupleComponentReference(ReferenceExpression tupleReference, IntObject fieldIndex)
      Given a reference to a tuple, and a field index, returns a reference to that component of the tuple. Think of this as tacking on one more instruction to the sequence of directions specified by a reference. For example, if tupleReference encodes "2nd component of element 3" and fieldIndex is 15, the result returned specifies "the 15-th component of the 2nd component of element 3".
      Parameters:
      tupleReference - a non-null reference for which the referenced sub-expression has tuple type
      fieldIndex - a non-null concrete integer object specifying the component of the tuple (indexed from 0)
      Returns:
      a reference to the fieldIndex-th element of the referenced tuple

    • unionMemberReference

      UnionMemberReference unionMemberReference(ReferenceExpression unionReference, IntObject memberIndex)
      Given a reference to a union (expression of union type) and an index of a member type of that union, returns a reference to the underlying element.

    • offsetReference

      OffsetReference offsetReference(ReferenceExpression reference, NumericExpression offset)

    • assign

      SymbolicExpression assign(SymbolicExpression value, ReferenceExpression reference, SymbolicExpression subValue)
      Given a symbolic expression value, a reference to a point within that value, and a subValue, returns the symbolic expression obtained by replacing the referenced part of value with subValue.
      Parameters:
      value - a non-null symbolic expression
      reference - a non-null reference to a subexpression of value
      subValue - a non-null expression with type compatible with that of the referenced sub-expression of value
      Returns:
      the expression that results from taking value and replacing the referenced sub-expression with subValue

    • getFreeSymbolicConstants

      Set<SymbolicConstant> getFreeSymbolicConstants(SymbolicExpression expr)
      Returns the set of unbound symbolic constants occurring in an expression. Each symbolic constant will occur at most once in the collection returned. This includes symbolic constants that occur in types (for example, array lengths).
      Parameters:
      expr - a non-null symbolic expression
      Returns:
      set of unbound symbolic constants occurring in expr

    • bitand

      NumericExpression bitand(NumericExpression left, NumericExpression right)
      Returns the result of bit-and operation for two given unsigned integers, those two unsigned integers are in the form of NumericExpression.
      Parameters:
      left - a non-null NumericExpression representing an unsigned integer. The length of the unsigned integer should be defined as a concrete integer.
      right - a non-null NumericExpression representing an unsigned integer. The length of the unsigned integer should be defined as a concrete integer, whose value is same to the left.
      Returns:
      a NumericExpression representing the result.

    • bitor

      NumericExpression bitor(NumericExpression left, NumericExpression right)
      Returns the result of bit-or operation for two given unsigned integers, those two unsigned integers are in the form of NumericExpression.
      Parameters:
      left - a non-null NumericExpression representing an unsigned integer. The length of the unsigned integer should be defined as a concrete integer.
      right - a non-null NumericExpression representing an unsigned integer. The length of the unsigned integer should be defined as a concrete integer, whose value is same to the left.
      Returns:
      a NumericExpression representing the result.

    • bitxor

      NumericExpression bitxor(NumericExpression left, NumericExpression right)
      Returns the result of bit-xor operation for two given unsigned integers, those two unsigned integers are in the form of NumericExpression.
      Parameters:
      left - a non-null NumericExpression representing an unsigned integer. The length of the unsigned integer should be defined as a concrete integer.
      right - a non-null NumericExpression representing an unsigned integer. The length of the unsigned integer should be defined as a concrete integer, whose value is same to the left.
      Returns:
      a NumericExpression representing the result.

    • bitnot

      NumericExpression bitnot(NumericExpression expression)
      Returns the result of bit-not operation for the given unsigned integer, the given unsigned integer is in the form of NumericExpression. TODO: Not independent with Length, and for shifts
      Parameters:
      expression - a non-null NumericExpression representing an unsigned integer. The length of the unsigned integer should be defined as a concrete integer.
      Returns:
      a NumericExpression representing the result.

    • bitshiftLeft

      NumericExpression bitshiftLeft(NumericExpression left, NumericExpression right)
      Returns the result of bit-left-shift operation for the given unsigned integer, the given unsigned integer is in the form of NumericExpression.
      Note that: all blank bits caused by shifting are filled with 0.
      Parameters:
      left - The integer will be applied with bit-shift
      right - The integer represents the number of shifited bits.
      Returns:

    • bitshiftRight

      NumericExpression bitshiftRight(NumericExpression left, NumericExpression right)
      Returns the result of bit-right-shift operation for the given unsigned integer, the given unsigned integer is in the form of NumericExpression.
      Note that: all blank bits caused by shifting are filled with 0.
      Parameters:
      left - The integer will be applied with bit-shift
      right - The integer represents the number of shifited bits.
      Returns:

    • bitVectorType

      SymbolicCompleteArrayType bitVectorType(int length)
      Returns the SymbolicCompleteArrayType representing a bitVectorType, which is an array of booleans with concrete length.
      Parameters:
      length - an integer representing the length of the bits of the integer type.
      Returns:
      a SymbolicCompleteArrayType with the base-type of boolean and the given length.

    • integer2Bitvector

      SymbolicExpression integer2Bitvector(NumericExpression integer, SymbolicCompleteArrayType bitVectorType)
      Returns the conversion of a bit vector from an integer.
      Parameters:
      integer - a non-null SymbolicExpression representing an integer.
      bitVectorType - a non-null SymbolicCompleteArrayType representing the type of bit vector with a type of boolean and a concrete length.
      Returns:
      a non-null SymbolicExpression representing a bit vector.

    • bitvector2Integer

      NumericExpression bitvector2Integer(SymbolicExpression bitvector)
      Converts a bit vector to an integer. Pre-conditions: The type of bitvector should be a SymbolicCompleteArrayType whose element type is Boolean with a concrete length.
      Parameters:
      bitvector - a non-null SymbolicExpression representing a bit vector.
      Returns:
      a non-null SymbolicExpression representing an integer.

    • setErrFile

      void setErrFile(String errFile)

      Summary:Set name (path) for prover unexpected error file.

      Details: A prover unexpected error file saves all unexpected error messages coming from external provers (e.g. z3, cvc3 etc). Unexpected errors are caused by bugs either in the provers or in SARL . By setting filename including path to the file through such an interface, other components (like CIVL) can direct the file the any favorite places.

      Parameters:
      errFile - The desired prover error file name.

    • getErrFile

      String getErrFile()

      Summary:Get the name (path) of the prover unexpected error file. For details of the error file see setErrFile(String)

      Returns:
      The String type filename (including path)

    • printCompressed

      void printCompressed(SymbolicExpression expr, PrintStream out)
      Prints the expression by preceding with a sequence of definitions of sub-expressions which are used more than once. Good for printing large expressions with many repeated sub-expressions.
      Parameters:
      expr - the symbolic expression to print
      out - the stream to which the output will be sent

    • printCompressedTree

      void printCompressedTree(String prefix, SymbolicExpression expr, PrintStream out)

      Use this method to print large symbolic expression hierarchically.

      Parameters:
      prefix - any string the callers of this method want to put at the beginning of each line.
      expr - the input symbolic expression
      out - the output stream

    • printExprTree

      void printExprTree(SymbolicExpression expr, PrintStream out)

      print symbolic expression as tree structure

      Parameters:
      expr - the input symbolic expression
      out - the output stream

    • fullySubstitute

      SymbolicExpression fullySubstitute(Map<SymbolicExpression,SymbolicExpression> substituteMap, SymbolicExpression expression)
      Substitute the given SymbolicExpression expression by repeatedly applying the method
      invalid reference 
      #apply(SymbolicExpression)
      until no more substitution can happen.
      Parameters:
      substituteMap -
      expression -
      Returns:
      The new predicate which is done the fully substitution.

    • getIntegerLengthBound

      int getIntegerLengthBound()
      Get the current upper bound of the integer length.
      Returns:
      the maximum bit-length of the integer type

    • setIntegerLengthBound

      boolean setIntegerLengthBound(int bound)
      Set the upper bound of the length of the integer type.
      Parameters:
      bound -
      Returns:
      true

    • derivative

      SymbolicExpression derivative(SymbolicExpression function, IntObject index, IntObject degree)
      Returns the function which is the degree-th derivative of function with respect to the index-th parameter.
      Parameters:
      function - a function of n real variables, for some n at least 1
      index - the parameter index, an integer greater than or equal to 0 and less than n
      degree - a non-negative integer, the number of times to differentiate
      Returns:
      the function which is the derivative; it has the same signature as the given function

    • differentiable

      BooleanExpression differentiable(SymbolicExpression function, IntObject degree, Iterable<? extends NumericExpression> lowerBounds, Iterable<? extends NumericExpression> upperBounds)
      Returns an expression of boolean type which encodes the claim that a function is differentiable on a closed interval in R^n.
      Parameters:
      function - the function from R^n to R, for some n at least 1
      degree - the maximal degree of the derivatives which exist and are continuous, a nonnegative integer
      lowerBounds - lower bounds of the domain intervals; a sequence of real-valued expressions of length n
      upperBounds - upper bounds of the domain intervals; a sequence of real-valued expressions of length n
      Returns:
      a boolean expression encoding the differentiability claim
      See Also:

    • concreteValueOfUninterpretedType

      SymbolicExpression concreteValueOfUninterpretedType(SymbolicUninterpretedType type, IntObject key)
      Returns a symbolic expression of a SymbolicUninterpretedType.
      Parameters:
      type - an instance of SymbolicUninterpretedType
      key - an concrete integral key of the returning symbolic expression.
      Returns:
      a symbolic expression of a SymbolicUninterpretedType.

    • getForallStructure

      CoreUniverse.ForallStructure getForallStructure(BooleanExpression forallExpr)
      Attempts to find a boolean expression equivalent to forallExpr but with the structure 
       forall int i . a≤i≤b -> e
      where a and b are integer expressions that do not involve i, and e is some boolean expression. If the attempt succeeds, the result is returned as a structure with the bound variable i, the lower bound a, the upper bound b, and the body e. Note that the formula above is equivalent to 
       forall int i . !(a≤i) || !(i≤b) || e
      i.e., 
       forall int i . i≤a-1 || b+1≤i || e
      Parameters:
      forallExpr - an expression with operator SymbolicExpression.SymbolicOperator.FORALL
      Returns:
      a structure specifying the components above if the forall expression has the special form, else null

    • getSummands

      NumericExpression[] getSummands(NumericExpression expr)
      Decomposes an expression as a sum of terms, returning those terms as an array.
      Parameters:
      expr - a numeric symbolic expression
      Returns:
      an array of numeric expressions such that the sum of the elements of that array equals the given expression

    • expand

      NumericExpression[] expand(NumericExpression expr)
      Attempts to expand an expression as a sum of simpler expressions.
      Parameters:
      expr - a numeric expression, non-null
      Returns:
      an array of expressions whose sum is equivalent to expr

    • floor

      NumericExpression floor(NumericExpression expr)
      Given an expression x of real type, returns an expression of integer type representing the greatest integer less than or equal to x.
      Parameters:
      expr - an expression of real type
      Returns:
      the floor of expr, the greatest integer less than or equal to expr

    • ceil

      NumericExpression ceil(NumericExpression expr)
      Given an expression x of real type, returns an expression of integer type representing the least integer greater than or equal to x.
      Parameters:
      expr - an expression of real type
      Returns:
      the ceil of expr, the least integer greater than or equal to expr

    • roundToZero

      NumericExpression roundToZero(NumericExpression expr)
      Given an expression x of real type, returns an expression of integer type representing the resulting of rounding x towards 0. This is equivalent to x >= 0 ? floor(x) : ceil(x).
      Parameters:
      expr - an expression of real type
      Returns:
      the result of rounding expr towards 0

    • valueSetTemplate

      SymbolicExpression valueSetTemplate(SymbolicType valueType, ValueSetReference[] vsRefs)

      Given a symbolic type of a symbolic value and a list of ValueSetReferences, returns symbolic expression representing a value set template.

      A value set template consists of a type t of some value and a set of ValueSetReferences. Applying a value set template to a symbolic value v of the type t results in a subset of the value v.

      Parameters:
      vsRefs - references to subsets of some value v
      type - symbolic type of some value v
      Returns:
      a symbolic expression which is a value set template

    • valueSetReferences

      Iterable<ValueSetReference> valueSetReferences(SymbolicExpression valueSetTemplate)
      Returns the set of ValueSetReferences in the given value set template.
      Parameters:
      valueSetTemplate - a symbolic expression of valueSetTemplateType()
      Returns:
      an Iterable collection of ValueSetReferences in the given value set template

    • valueType

      SymbolicType valueType(SymbolicExpression valueSetTemplate)
      Returns the SymbolicType of values, to which the given value set template refers.
      Parameters:
      valueSetTemplate - a symbolic expression of valueSetTemplateType()
      Returns:
      the type of the values, to which the given value set template refers

    • valueSetTemplateType

      SymbolicType valueSetTemplateType()
      Returns the type of a value set template. A value set template is a symbolic expression that can be applied to a value, which is a instance of SymbolicExpression, in order to obtain a subset of the value.
      Returns:
      The symbolic type of a value set template.

    • valueSetContains

      BooleanExpression valueSetContains(SymbolicExpression vst0, SymbolicExpression vst1)

      Test if a value set template vst0 contains another value set template vst1.

      A value set template vst0 contains another value set template vst1 iff 1) both of them are associated with the same symbolic type; 2) all the value set references in vst1 are contained by value set references in vst0.

      Parameters:
      vst0 - a value set template
      vst1 - a value set template
      Returns:
      a boolean expression representing the result of the test

    • valueSetNoIntersect

      BooleanExpression valueSetNoIntersect(SymbolicExpression vst0, SymbolicExpression vst1)

      Test if two value set templates have no intersection, i.e., if applying the two templates to the same object, their referred parts have no overlap.

      Parameters:
      vst0 - a value set template
      vst1 - a value set template
      Returns:
      the condition that is true iff the two value set templates have no intersection

    • valueSetDiff

      SymbolicExpression valueSetDiff(SymbolicExpression vst0, SymbolicExpression vst1)

      Given two value set templates, returns their set difference.

    • valueSetUnion

      SymbolicExpression valueSetUnion(SymbolicExpression vst0, SymbolicExpression vst1)

      Given two value set templates, returns the union of the two.

      The given two value set templates must be associated with the same symbolic type. The returned value set template contains value set references that are the precise union of the value set references in the given two templates.

      Parameters:
      vst0 - a value set template
      vst1 - a value set template
      Returns:
      the union of two value set templates

    • valueSetHavoc

      dev.civl.sarl.util.Pair<SymbolicExpression,Integer> valueSetHavoc(SymbolicExpression value, SymbolicExpression valueSetTemplate, String prefix, int startCount)

    • valueSetAssigns

      SymbolicExpression valueSetAssigns(SymbolicExpression oldValue, SymbolicExpression valueSetTemplate, SymbolicExpression newValue)

      Copies a subset of a value v to another value v' with a given value set template. Returns the value after the copy operation.

      Parameters:
      oldValue - a symbolic expression whose type is same as the one that is associated with the given value set template
      valueSetTemplate - a value set template
      newValue - a symbolic expression whose type is same as the one that is associated with the given value set template
      Returns:
      a symbolic expression where the subset referred by the given value set template are come from the "newValue" and the other subset are still same as the ones in "oldValue"

    • valueSetReferenceType

      SymbolicType valueSetReferenceType()
      Returns:
      the symbolic type of ValueSetReference

    • vsIdentityReference

      VSIdentityReference vsIdentityReference()
      Returns the identity (or "trivial") value set reference I. This is the reference characterized by the property that dereference(I,v) returns v for any symbolic expression v.

    • vsArrayElementReference

      VSArrayElementReference vsArrayElementReference(ValueSetReference parent, NumericExpression index)
      Given a value set reference to a (set-of) array(s) and an index (integer), returns a reference to the (set-of) elements of the (set-of) array(s) at that index

    • vsArraySectionReference

      VSArraySectionReference vsArraySectionReference(ValueSetReference parent, NumericExpression lower, NumericExpression upper)
      Given a reference to a (set-of) array(s) and an inclusive lower index bound, an exclusive upper index bound and a DEFAULT step, which is one, of the range of the section, returns a reference to the (set-of) section(s) of the array(s) with the given bounds.

    • vsArraySectionReference

      VSArraySectionReference vsArraySectionReference(ValueSetReference parent, NumericExpression lower, NumericExpression upper, NumericExpression step)
      Given a reference to a (set-of) array(s) and an inclusive lower index bound, an exclusive upper index bound and a step of the range of the section, returns a reference to the (set-of) section(s) of the array(s) with the given bounds.

    • vsTupleComponentReference

      VSTupleComponentReference vsTupleComponentReference(ValueSetReference parent, IntObject fieldIndex)
      Given a reference to a (set-of) tuple(s), and a field index, returns a reference to that (set-of) component(s) of the tuple(s).

    • vsUnionMemberReference

      VSUnionMemberReference vsUnionMemberReference(ValueSetReference parent, IntObject memberIndex)
      Given a reference to a (set-of) union(s) (expression of union type) and an index of a member type of that union, returns a reference to the (set-of) underlying element(s).

    • vsOffsetReference

      VSOffsetReference vsOffsetReference(ValueSetReference parent, NumericExpression offset)
      Given a reference to a (set-of) value(s) and a integral offset, returns a reference to a (set-of) value(s), which is obtained by applying the (set-of) offset(s) to the given (set-of) value(s).