CoreUniverse.java
package dev.civl.sarl.IF;
import java.io.PrintStream;
import java.math.BigInteger;
import java.util.Comparator;
import java.util.List;
import java.util.Map;
import java.util.Set;
import dev.civl.sarl.IF.expr.ArrayElementReference;
import dev.civl.sarl.IF.expr.BooleanExpression;
import dev.civl.sarl.IF.expr.BooleanSymbolicConstant;
import dev.civl.sarl.IF.expr.NumericExpression;
import dev.civl.sarl.IF.expr.NumericSymbolicConstant;
import dev.civl.sarl.IF.expr.OffsetReference;
import dev.civl.sarl.IF.expr.ReferenceExpression;
import dev.civl.sarl.IF.expr.SymbolicConstant;
import dev.civl.sarl.IF.expr.SymbolicExpression;
import dev.civl.sarl.IF.expr.SymbolicExpression.SymbolicOperator;
import dev.civl.sarl.IF.expr.TupleComponentReference;
import dev.civl.sarl.IF.expr.UnionMemberReference;
import dev.civl.sarl.IF.expr.valueSetReference.VSArrayElementReference;
import dev.civl.sarl.IF.expr.valueSetReference.VSArraySectionReference;
import dev.civl.sarl.IF.expr.valueSetReference.VSIdentityReference;
import dev.civl.sarl.IF.expr.valueSetReference.VSOffsetReference;
import dev.civl.sarl.IF.expr.valueSetReference.VSTupleComponentReference;
import dev.civl.sarl.IF.expr.valueSetReference.VSUnionMemberReference;
import dev.civl.sarl.IF.expr.valueSetReference.ValueSetReference;
import dev.civl.sarl.IF.number.IntegerNumber;
import dev.civl.sarl.IF.number.Number;
import dev.civl.sarl.IF.number.NumberFactory;
import dev.civl.sarl.IF.number.RationalNumber;
import dev.civl.sarl.IF.object.BooleanObject;
import dev.civl.sarl.IF.object.IntObject;
import dev.civl.sarl.IF.object.NumberObject;
import dev.civl.sarl.IF.object.StringObject;
import dev.civl.sarl.IF.object.SymbolicObject;
import dev.civl.sarl.IF.type.SymbolicArrayType;
import dev.civl.sarl.IF.type.SymbolicCompleteArrayType;
import dev.civl.sarl.IF.type.SymbolicFunctionType;
import dev.civl.sarl.IF.type.SymbolicFunctionType.SpecialRelationKind;
import dev.civl.sarl.IF.type.SymbolicIntegerType;
import dev.civl.sarl.IF.type.SymbolicMapType;
import dev.civl.sarl.IF.type.SymbolicRealType;
import dev.civl.sarl.IF.type.SymbolicSetType;
import dev.civl.sarl.IF.type.SymbolicTupleType;
import dev.civl.sarl.IF.type.SymbolicType;
import dev.civl.sarl.IF.type.SymbolicUninterpretedType;
import dev.civl.sarl.IF.type.SymbolicUnionType;
import dev.civl.sarl.util.Pair;
/**
* A {@link CoreUniverse} provides most of the functionality of a
* {@link SymbolicUniverse}, including the mechanisms to create and manipulate
* {@link SymbolicExpression}s and other {@link SymbolicObject}s. 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".
*
* @author siegel
*/
public interface CoreUniverse {
// General...
/**
* Shall the {@link Reasoner}s generated by this universe use backwards
* substitution when simplifying, in order to solve for certain numeric
* expressions in terms of others?
*
* @return the value of the "useBackwardSubstitution" flag
*/
boolean getUseBackwardSubstitution();
/**
* Sets the value of the "useBackwardSubstitution" flag. If {@code true}, the
* {@link Reasoner}s generated by this universe will use backwards substitution
* when simplifying, in order to solve for certain numeric expressions in terms
* of others.
*
* @param value the new value for the "useBackwardSubstitution" flag
*/
void setUseBackwardSubstitution(boolean value);
/**
* Gets the <code>showQueries</code> flag: if <code>true</code>, SARL theorem
* prover queries will be printed to the output stream.
*
* @return current value of the <code>showQueries</code> flag
* @see #setShowQueries(boolean)
* @see #getShowProverQueries()
* @see #setShowProverQueries(boolean)
*/
boolean getShowQueries();
/**
* Sets the <code>showQueries</code> flag. If this is set to <code>true</code>,
* SARL theorem prover queries will be printed to the output stream.
*
* @param value new value for the <code>showQueries</code> flag.
* @see #getShowQueries()
* @see #getShowProverQueries()
* @see #setShowProverQueries(boolean)
*/
void setShowQueries(boolean value);
/**
* Gets the <code>showProverQueries</code> flag: if <code>true</code>, the
* theorem prover queries processed by the underlying theorem prover(s) will be
* printed to the output stream.
*
* @return current value of the <code>showProverQueries</code> flag
* @see #setShowProverQueries(boolean)
* @see #getShowQueries()
* @see #setShowQueries(boolean)
*/
boolean getShowProverQueries();
/**
* Sets the <code>showProverQueries</code> flag. If set to <code>true</code> ,
* the theorem prover queries processed by the underlying theorem prover(s) will
* be printed to the output stream.
*
* @param value new value for the <code>showProverQueries</code> flag
* @see #getShowProverQueries()
* @see #getShowQueries()
* @see #setShowQueries(boolean)
*/
void setShowProverQueries(boolean value);
/**
* Returns the output stream to which information (such as queries) will be
* printed. By default, standard out.
*
* @return current output stream
* @see #setOutputStream(PrintStream)
*/
PrintStream getOutputStream();
/**
* Sets the output stream, the stream to which information (such as queries)
* will be printed. By default, standard out.
*
* @param out new value for output stream
* @see #getOutputStream()
*/
void setOutputStream(PrintStream out);
/**
* Returns a comparator on the set of all symbolic objects. This defines a total
* order on all symbolic objects.
*
* @return a comparator on all symbolic objects
*/
Comparator<SymbolicObject> comparator();
/**
* Returns the number of canonic symbolic objects controlled by this universe.
*
* @return the number of canonic symbolic objects
*/
int numObjects();
/**
* <p>
* Gets the canonic {@link SymbolicObject} belonging to this universe with the
* given ID number.
* </p>
*
* <p>
* 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.
* </p>
*
* @param id the ID number of a {@link SymbolicObject} belonging to this
* universe
* @return the canonic symbolic object with the given ID number.
*/
SymbolicObject objectWithId(int id);
/**
* 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.
*
* @return the current upper bound on probability of error
*/
RationalNumber getProbabilisticBound();
/**
* 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.
*
* @param epsilon the new upper bound on probability of error that should be
* used from this point forward, a rational number in [0,1)
*/
void setProbabilisticBound(RationalNumber epsilon);
// Types...
/**
* 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 {@link SymbolicArrayType} and a
* {@link SymbolicCompleteArrayType} with compatible element types are
* compatible.
*
* @param type0 a non-<code>null</code> symbolic type
* @param type1 a non-<code>null</code> symbolic type
* @return a boolean expression which holds iff the two types are compatible
* @see #pureType(SymbolicType)
*/
BooleanExpression compatible(SymbolicType type0, SymbolicType type1);
/**
* Returns the "pure" version of the type, i.e., the compatible
* {@link SymbolicType} that contains no {@link SymbolicExpression}s. 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 #compatible(SymbolicType, SymbolicType)
*/
SymbolicType pureType(SymbolicType type);
/**
* The boolean type.
*
* @return the boolean type
*/
SymbolicType booleanType();
/**
* The "ideal" integer type, representing the set of mathematical integers.
*
* @return the integer type
* @see #herbrandIntegerType()
* @see #boundedIntegerType(NumericExpression, NumericExpression, boolean)
*/
SymbolicIntegerType integerType();
/**
* <p>
* 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.
* </p>
*
* <p>
* Note: to create a concrete number of Herbrand integer type, create an ideal
* concrete integer then cast it to the Herbrand type.
* </p>
*
* @return the Herbrand integer type
* @see #integerType()
* @see #boundedIntegerType(NumericExpression, NumericExpression, boolean)
*/
SymbolicIntegerType herbrandIntegerType();
/**
* <p>
* Returns the bounded integer types with specified upper and lower bounds.
* Either of the bounds may be <code>null</code>, indicating there is no bound
* (i.e., the bound is + or - infinity). If <code>cyclic</code> is
* <code>true</code>, then all operations treat the domain cyclically (i.e.,
* max+1 = min).
* </p>
*
* <p>
* <strong>NOTE: THIS IS NOT YET IMPLEMENTED.</strong>
* </p>
*
* @param min smallest integer value in the domain or <code>null</code>
* @param max largest integer value in the domain or <code>null</code>
* @param cyclic should operations treat the domain cyclically?
* @return the bounded integer type as specified
* @see #integerType()
* @see #herbrandIntegerType()
*/
SymbolicIntegerType boundedIntegerType(NumericExpression min, NumericExpression max, boolean cyclic);
/**
* The "ideal" real type, representing the set of mathematical real numbers.
*
* @return the real type
* @see #herbrandRealType()
*/
SymbolicRealType realType();
/**
* <p>
* 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.
* </p>
*
* <p>
* A Herbrand value and non-Herbrand value are always considered to be not
* equal, even if they are concrete expressions.
* </p>
*
* <p>
* Note: to create a concrete number of herbrand real type, create an ideal
* concrete real then cast it to the herbrand type.
* </p>
*
* @return the Herbrand real type
* @see #realType()
*/
SymbolicRealType herbrandRealType();
// TODO: floating point types
/**
* Returns the character type.
*
* @return the character type
*/
SymbolicType characterType();
/**
* Returns the complete array type with the given element type and extent (array
* length). Neither argument can be <code>null</code>.
*
* @param elementType the type of the elements of the array
* @param extent length of the array
* @return the complete array type as specified
* @see #arrayType(SymbolicType)
*/
SymbolicCompleteArrayType arrayType(SymbolicType elementType, NumericExpression extent);
/**
* Returns the incomplete array type with the given element type. The element
* type cannot be <code>null</code>.
*
* @return the incomplete array type
* @see #arrayType(SymbolicType, NumericExpression)
*/
SymbolicArrayType arrayType(SymbolicType elementType);
/**
* <p>
* Returns the dimension and base type of an array type.
* </p>
*
* <p>
* The dimension and base type of an array type <i>T</i>[] are defined as
* follows: if <i>T</i> is an array type, the dimension of <i>T</i>[] is one
* plus the dimension of <i>T</i>, and the base type of <i>T</i>[] is the base
* type of <i>T</i> . Otherwise, the dimension of <i>T</i>[] is 1 and the base
* type is <i>T</i>.
* </p>
*
* @param type a non-<code>null</code> array type
* @return A {@link Pair} consisting of dimension (left) and base type (right).
*/
Pair<Integer, SymbolicType> arrayDimensionAndBaseType(SymbolicArrayType type);
/**
* Returns the tuple type defined by the given sequence of component types. The
* tuple type consists of all tuples of values (<i>x</i><sub>0</sub>, ...,
* <i>x</i><sub>n-1</sub>), where <i>x</i><sub><i>i</i></sub> has type
* <code>fieldsTypes</code><sub><i>i</i></sub>. A tuple type also has a name,
* and two tuple types are not equal if they have unequal names.
*
* @param name the name of the tuple type
* @param fieldTypes an iterable object specifying the sequence of component
* types for the tuple type
* @return the tuple type specified by the given name and field types
*/
SymbolicTupleType tupleType(StringObject name, Iterable<? extends SymbolicType> fieldTypes);
/**
* Returns the specified function type. A function type is specified by a
* sequence of input types, and an output type.
*
* @param inputTypes sequence of input types
* @param outputType the output type of the function
* @return the function type
*/
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.
*
* @param inputTypes sequence of input types
* @param outputType the output type of the function
* @param relKind the special relation kind if this function represents such
* a relation
* @return the function type
*/
SymbolicFunctionType functionType(Iterable<? extends SymbolicType> inputTypes, SymbolicType outputType,
SpecialRelationKind relKind);
/**
* <p>
* Returns the type which is the union of the given member types.
* </p>
*
* <p>
* Say the member types are <i>t</i><sub>0</sub>,...,<i>t</i><sub>n-1</sub> and
* call the union type <i>u</i>. For 0 ≤ <i>i</i> < <i>n</i>, there are
* functions inject<sub>i</sub>: <i>t</i><sub><i>i</i></sub> → <i>u</i>,
* extract<sub><i>i</i></sub>: <i>u</i> → <i>t</i><sub><i>i</i></sub>, and
* test<sub><i>i</i></sub>: <i>u</i> → {<i>true</i>,<i>false</i>}. The
* domain of <i>u</i> consists of all expressions of the form
* inject<sub><i>i</i></sub>(<i>x<sub>i</sub></i>).
* </p>
*
* <p>
* We have
* extract<sub><i>i</i></sub>(inject<sub><i>i</i></sub>(<i>x</i>))=<i>x</i> and
* extract<sub><i>i</i></sub> is undefined on any element of <i>u</i> that is
* not in the image of inject<sub><i>i</i></sub>.
* test<sub><i>i</i></sub>(<i>x</i>) is <i>true</i> iff
* x=inject<sub><i>i</i></sub>(<i>x<sub>i</sub></i>) for some
* <i>x<sub>i</sub></i> in <i>t<sub>i</sub></i>.
* </p>
*
* @param name the name of the union type
* @param memberTypes the sequence of member types
* @return the specified union type
*/
SymbolicUnionType unionType(StringObject name, Iterable<? extends SymbolicType> memberTypes);
/**
* Returns the type for "set of T"; not yet implemented.
*
* @param elementType type of elements of the set
* @return the type "set of <code>elementType</code>"
*/
SymbolicSetType setType(SymbolicType elementType);
/**
* Under construction.
*
* @param keyType
* @param valueType
* @return
*/
SymbolicMapType mapType(SymbolicType keyType, SymbolicType valueType);
/**
* 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
* {@link #entrySet(SymbolicExpression)}, which returns the set of entries of a
* map.
*
* @param mapType a map type
* @return the type of an entry in the map
*/
SymbolicTupleType entryType(SymbolicMapType mapType);
/**
* Returns an uninterpreted type which is an instance of
* {@link SymbolicUninterpretedType}.
*
* @param name the name of the returning uninterpreted type
* @return an instance of {@link SymbolicUninterpretedType} whose name is the
* given String.
*/
SymbolicUninterpretedType symbolicUninterpretedType(String name);
// Other...
/**
* Returns a substituter for which the base substitutions are specified by an
* explicit Java {@link 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.
*
* @param map a map which specifies that a key should be replaced by the
* corresponding value
* @return a substituter based on the given map
*/
UnaryOperator<SymbolicExpression> mapSubstituter(Map<SymbolicExpression, SymbolicExpression> map);
UnaryOperator<SymbolicExpression> mapSubstituter(UnaryOperator<SymbolicExpression> operator);
/**
* Returns a substituter for which the base substitutions are specified by an
* explicit Java {@link 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.
*
* @param map a map which specifies that a key should be replaced by the
* corresponding value
* @return a substituter based on the given map
*/
public UnaryOperator<SymbolicExpression> constantSubstituter(Map<SymbolicConstant, SymbolicExpression> map);
/**
* 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.
*
* @param nameMap mapping of old to new names for symbolic constants
* @return a substituter which replaces symbolic constants as specified by
* <code>nameMap</code>
*/
UnaryOperator<SymbolicExpression> nameSubstituter(Map<StringObject, StringObject> nameMap);
/**
* 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.
*
* @param var the symbolic constant
* @param value the value that will replace the symbolic constant
* @return a substituter that will replace any occurrence of <code>var</code>
* with <code>value</code>
*/
UnaryOperator<SymbolicExpression> simpleSubstituter(SymbolicConstant var, SymbolicExpression value);
/**
* <p>
* Returns an operator on {@link SymbolicExpression}s 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
* <code>root</code>. 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.
* </p>
*
* <p>
* The parameter <code>ignore</code> also provides a way to specify that certain
* symbolic constants should be ignored, i.e., they should not be renamed.
* </p>
*
* @param root the string that forms the root of the names of the new symbolic
* constants
* @param ignore a predicate providing a method that takes a
* {@link SymbolicConstant} and returns <code>true</code> or
* <code>false</code>; if it returns <code>true</code>, then that
* symbolic constant should <strong>not</strong> be renamed
* @return 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(String root, Predicate<SymbolicConstant> ignore);
/**
* <p>
* Returns an operator on {@link SymbolicExpression}s 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
* <code>root</code>. 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.
* </p>
*
* <p>
* Equivalent to invoking {@link #canonicalRenamer(String, Predicate)} with
* <code>ignore</code> the constant predicate <code>false</code>.
* </p>
*
* @param root the string that forms the root of the names of the new symbolic
* constants
* @return 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(String root);
/**
* 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
* {@link SymbolicExpression} interface, especially for the
* {@link SymbolicOperator}s. The result returned should be identical to what
* would be returned by calling the specific methods (e.g.,
* {@link #add(Iterable)}).
*
* @param operator a symbolic operator
* @param type the type which the resulting expression should have (since
* it may not be unambiguous)
* @param arguments arguments which should be appropriate for the specified
* operator
*/
SymbolicExpression make(SymbolicOperator operator, SymbolicType type, SymbolicObject[] arguments);
/**
* Returns the total number of calls made to methods
* {@link Reasoner#valid(BooleanExpression)} and
* {@link Reasoner#validOrModel(BooleanExpression)}.
*
* @return the total number of validity calls
*/
int numValidCalls();
/**
* 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 {@link #numValidCalls()}, as not every valid call requires a call
* to the prover.
*
* @return the total number of theorem prover validity calls
*/
int numProverValidCalls();
// Symbolic primitive objects: ints, boolean, reals, strings
// Note: these are not symbolic expressions, just symbolic objects!
/**
* Returns the {@link BooleanObject} wrapping the given boolean value. A
* {@link BooleanObject} is a {@link SymbolicObject}, so can be used as an
* argument of a {@link SymbolicExpression}.
*
* @param value <code>true</code> or <code>false</code>, the boolean value to
* wrap
* @return the corresponding {@link BooleanObject}
*/
BooleanObject booleanObject(boolean value);
/**
* Returns the {@link IntObject} wrapping the given Java <code>int</code> value.
* An {@link IntObject} is a {@link SymbolicObject} so can be used as an
* argument of a {@link SymbolicExpression}. It is used in cases where a "small"
* concrete integer is needed. For concrete integers of arbitrary size, use
* {@link IntegerNumber} instead and create a {@link NumberObject} .
*
* @param value any Java <code>int</code>
* @return an {@link IntObject} wrapping <code>value</code>
*/
IntObject intObject(int value);
/**
* Returns the {@link NumberObject} wrapping the given {@link Number} value.
* These are SARL {@link Number}s, not {@link java.lang.Number}s. They are used
* to represent infinite precision, unbounded integers and rational numbers.
*
* @param value a finite concrete SARL Number
* @return the {@link NumberObject} wrapping <code>value</code>
*/
NumberObject numberObject(Number value);
/**
* Returns the {@link StringObject} wrapping the given {@link String} value. A
* {@link StringObject} is a {@link SymbolicObject} so can be used as an
* argument to a {@link SymbolicExpression}.
*
* @param string any Java {@link String}
* @return the {@link StringObject} wrapping <code>string</code>
*/
StringObject stringObject(String string);
// The "null" expression...
/**
* Returns the "NULL" expression. This is a non-<code>null</code> (in the Java
* sense of "<code>null</code>") {@link SymbolicExpression} for which the method
* {@link SymbolicExpression#isNull()} returns <code>true</code>. Its type is
* <code>null</code>, and it has 0 arguments.
*
* @return the NULL expression
*/
SymbolicExpression nullExpression();
// Symbolic constants...
/**
* <p>
* Returns the {@link SymbolicConstant} with the given name and type. Two
* {@link SymbolicConstant}s 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.
* </p>
*
* <p>
* This method will return the right kind of {@link SymbolicConstant} based on
* the type. For example, if the type is numeric ( {@link SymbolicIntegerType}
* or {@link SymbolicRealType}), an instance of {@link NumericSymbolicConstant}
* will be returned. If the type is boolean, a {@link BooleanSymbolicConstant}
* will be returned.
* </p>
*
* @param name the name to give to this symbolic constant; it will be used to
* identify the object and for printing
* @param type the type of the symbolic constant
*/
SymbolicConstant symbolicConstant(StringObject name, SymbolicType type);
// Integers...
/**
* The symbolic expression representing the 0 integer value.
*
* @return the integer 0 as a numeric symbolic expression
*/
NumericExpression zeroInt();
/**
* The symbolic expression representing the integer 1.
*
* @return the integer 1 as a numeric symbolic expression
*/
NumericExpression oneInt();
/**
* Returns the integer symbolic expression with the given <code>int</code>
* value.
*
* @param value a Java <code>int</code>
* @return the symbolic expression of integer type representing that concrete
* value
*/
NumericExpression integer(int value);
/**
* Returns the numeric symbolic expression with the given <code>long</code>
* value.
*
* @param value any Java <code>long</code>
* @return the symbolic expression of integer type with that value
*/
NumericExpression integer(long value);
/**
* Returns the numeric symbolic expression with the given {@link BigInteger}
* value. The {@link BigInteger} class is a standard Java class for representing
* integers of any size.
*
* @param value any {@link BigInteger}
* @return the symbolic expression of integer type with that value
*/
NumericExpression integer(BigInteger value);
// Rationals...
/**
* 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.
*
* @return the real number 0 as a symbolic expression
*/
NumericExpression zeroReal();
/**
* Returns the symbolic expression representing the real number 1.
*
* @return the real number 1 as a symbolic expression
*/
NumericExpression oneReal();
/**
* Returns the symbolic expression of real type ({@link SymbolicRealType})
* representing the given <code>int</code> value. This is sometimes referred to
* as a "rational integer".
*
* @param value an Java <code>int</code>
* @return a concrete rational representation of this integer value;
* essentially, the rational number (value/1)
*/
NumericExpression rational(int value);
/**
* Returns the symbolic expression of real type ({@link SymbolicRealType})
* representing the given <code>long</code> value. This is sometimes referred to
* as a "rational integer".
*
* @param value a Java <code>long</code>
* @return a concrete rational representation of this <code>long</code> value;
* essentially the rational number (value/1)
*/
NumericExpression rational(long value);
/**
* Returns the symbolic expression of real type ({@link SymbolicRealType})
* representing the given {@link BigInteger} value. This is sometimes referred
* to as a "rational integer"
*
* @param value a Java {@link BigInteger}
* @return a concrete rational representation of this {@link BigInteger} value;
* essentially, the rational number (value/1)
*/
NumericExpression rational(BigInteger value);
/**
* Returns the symbolic expression of real type ({@link SymbolicRealType})
* representing the given <code>float</code> value.
*
* @param value a Java <code>float</code>
* @return a concrete rational representation of this <code>float</code> value
*/
NumericExpression rational(float value);
/**
* Returns the symbolic expression of real type ({@link SymbolicRealType})
* representing the given <code>double</code> value.
*
* @param value a Java <code>double</code>
* @return a concrete symbolic expression of real type representing the
* <code>value</code>
*/
NumericExpression rational(double value);
/**
* Returns the rational number obtained by dividing two integers,
* <code>numerator</code> and <code>denominator</code>. The result is a symbolic
* expression of {@link SymbolicRealType}. Note that this universe is free to
* transform the expression into an equivalent form, for example, by canceling
* any common factors.
*
* @param numerator a Java <code>int</code>
* @param denominator a non-0 Java <code>int</code>
* @return the real number formed by dividing <code>numerator</code> by
* <code>denominator</code>, as a symbolic expression of real type
*/
NumericExpression rational(int numerator, int denominator);
/**
* Returns the rational number obtained by dividing two long integers. The
* result will have {@link SymbolicRealType}.
*
* @param numerator a Java <code>long</code>
* @param denominator a non-0 Java <code>long</code>
* @return the real number formed by dividing <code>numerator</code> by
* <code>denominator</code>, as a {@link NumericExpression}
*/
NumericExpression rational(long numerator, long denominator);
/**
* Returns the rational number obtained by dividing two {@link BigInteger}s. The
* result will have {@link SymbolicRealType}.
*
* @param numerator an integer, the numerator
* @param denominator a non-0 integer, the denominator
* @return the rational number formed by dividing <code>numerator</code> by
* <code>denominator</code>, as a symbolic expression
*/
NumericExpression rational(BigInteger numerator, BigInteger denominator);
// General Numbers...
/**
* Returns the number factory used by this universe.
*
* @return the number factory used by this universe
*/
NumberFactory numberFactory();
/**
* Returns the concrete symbolic expression wrapping the given number. The type
* of the expression will be the "ideal" {@link SymbolicIntegerType} if
* <code>number</code> is an {@link IntegerNumber}, or the "ideal"
* {@link SymbolicRealType} if <code>number</code> is a {@link RationalNumber}.
*
* @param number any non-<code>null</code> finite SARL {@link Number}
* @return the concrete symbolic expression wrapping that number
* @see #number(NumberObject)
*/
NumericExpression number(Number number);
/**
* Returns the concrete symbolic expression wrapping the given number object.
* The type of the expression will be the "ideal" {@link SymbolicIntegerType} if
* <code>numberObject.getNumber()</code> is an {@link IntegerNumber}, or the
* "ideal" {@link SymbolicRealType} if it is a {@link RationalNumber}.
*
* @param numberObject any non-<code>null</code> {@link NumberObject}
* @see #number(Number)
* @see #numberObject(Number)
*/
NumericExpression number(NumberObject numberObject);
/**
* Returns the {@link Number} value if the given symbolic expression has a
* concrete numerical value, else returns <code>null</code>.
*
* @param expression any non-<code>null</code> numeric expression
* @return the {@link Number} value or <code>null</code>
*/
Number extractNumber(NumericExpression expression);
/**
* Returns a concrete symbolic expression of character type which wraps the
* given Java char.
*
* @param theChar the Java char
* @return symbolic expression wrapping <code>theChar</code>
* @see SymbolicType.SymbolicTypeKind#CHAR
* @see #characterType()
*/
SymbolicExpression character(char theChar);
/**
* If the given expression is a concrete character expression, this returns the
* character value, else it returns <code>null</code>.
*
* @param expression a symbolic expression
* @return the character it wraps or <code>null</code>
* @see #characterType()
* @see #character(char)
*/
Character extractCharacter(SymbolicExpression expression);
/**
* Returns a symbolic expression of type array-of-char which is a literal array
* consisting of the sequence of characters in the given string.
*
* @param theString a Java string
* @return <code>theString</code> represented as a symbolic expression of type
* array-of-char
* @see SymbolicArrayType
* @see SymbolicType.SymbolicTypeKind#CHAR
* @see #character(char)
* @see #characterType()
*/
SymbolicExpression stringExpression(String theString);
// Numeric operations...
/**
* 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.
*
* @param arg0 a symbolic expression of a numeric type
* @param arg1 a symbolic expression of the same numeric type
* @return the sum arg0+arg1
* @see SymbolicIntegerType
* @see SymbolicRealType
*/
NumericExpression add(NumericExpression arg0, NumericExpression arg1);
/**
* Returns a symbolic expression representing the sum of the given argument
* sequence.
*
* @param args a sequence of symbolic expressions of numeric type. They must all
* have the same type.
* @return expression representing the sum
* @see #add(NumericExpression, NumericExpression)
* @see SymbolicIntegerType
* @see SymbolicRealType
*/
NumericExpression add(Iterable<? extends NumericExpression> args);
/**
* 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.
*
* @param arg0 a symbolic expression of a numeric type
* @param arg1 a symbolic expression of the same numeric type
* @return the difference, arg0-arg1
* @see #add(NumericExpression, NumericExpression)
* @see SymbolicIntegerType
* @see SymbolicRealType
*/
NumericExpression subtract(NumericExpression arg0, NumericExpression arg1);
/**
* A fold sum expression. Takes three arguments: low, high and a function f:
* int-to-T. The expression means
* <code>f(low) + f(low + 1) + ... + f(high - 1)</code>
*
* @param low The lower bound of the integer set (inclusive)
* @param high The higher bound of the integer set (exclusive)
* @param 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.
* @return
*/
NumericExpression sigma(NumericExpression low, NumericExpression high, SymbolicExpression function);
/**
* <p>
* a <code>$reduction</code> 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.
* </p>
*
* @param operands a list of operands
* @param count the number of elements in each operand
* @param op an integer value representing the reduction
* operator
* @param compatibleConditionsOutput output argument, containing compatible
* conditions, if any of the given compatible
* conditions fails, the returned result is
* invalid
* @return the element-wise reduction result of given operator over the
* operands, if the output compatibale conditions are all valid.
*/
SymbolicExpression reduction(SymbolicExpression[] operands, NumericExpression count, SymbolicExpression op,
List<BooleanExpression> compatibleConditionsOutput);
boolean isSigmaCall(SymbolicExpression expr);
/**
* A permutation predicate, which asserts the slice from lower index
* <code>low</code> to higher index <code>high</code> in array
* <code>array_a</code> is a permutation of the slice from lower index
* <code>low</code> to higher index <code>high</code> in array
* <code>array_b</code>.
*
* @param array_a
* @param array_b
* @param low
* @param high
* @return an instance of the permutation predicate
*/
BooleanExpression permut(SymbolicExpression array_a, SymbolicExpression array_b, NumericExpression low,
NumericExpression high);
boolean isPermutCall(SymbolicExpression expr);
/**
* 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.
*
* @param arg0 a symbolic expression of a numeric type
* @param arg1 a symbolic expression of the same numeric type
* @return arg0 * arg1, the product of arg0 and arg1.
* @see #add(NumericExpression, NumericExpression)
* @see SymbolicIntegerType
* @see SymbolicRealType
*/
NumericExpression multiply(NumericExpression arg0, NumericExpression arg1);
/**
* Returns symbolic expression representing the product of the given sequence of
* expressions.
*
* @param args symbolic expression sequence; all elements have the same numeric
* type
* @return a symbolic expression representing the product
* @see #multiply(NumericExpression, NumericExpression)
* @see SymbolicIntegerType
* @see SymbolicRealType
*/
NumericExpression multiply(Iterable<? extends NumericExpression> args);
/**
* <p>
* 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.
* </p>
*
* <p>
* For reference, here's what C11 (Sec. 6.5.5) says about integer division:
* </p>
*
* <pre>
* 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.
* </pre>
*
* <p>
* Hence in C, a%b=a-(a/b)*b. Examples:
* <ul>
* <li>a=4, b=3: a/b=1, a%b=4-3=1</li>
* <li>a=4, b=-3: a/b=-1, a%b=4-(-1)(-3)=1</li>
* <li>a=-4, b=3: a/b=-1, a%b=-4-(-1)3=-1</li>
* <li>a=-4, b=-3: a/b=1, a%b=-4-1(-3)=-1</li>
* </ul>
* </p>
*
* <p>
* 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).
* </p>
*
* @param arg0 a symbolic expression of a numeric type
* @param arg1 a symbolic expression of the same numeric type
* @return the quotient, arg0 / arg1
* @throws ArithmeticException If there is a division by zero.
* @see SymbolicIntegerType
* @see SymbolicRealType
*/
NumericExpression divide(NumericExpression arg0, NumericExpression arg1) throws ArithmeticException;
/**
* Returns a symbolic expression which represents arg0 modulo arg1. The two
* given expressions must have the integer type.
*
* @param arg0 a symbolic expression of integer type
* @param arg1 a symbolic expression of integer type
* @return the modulus, arg0 % arg1
* @throws ArithmeticException If there is a division by zero.
* @see SymbolicIntegerType
* @see #divide(NumericExpression, NumericExpression)
* @see #divides(NumericExpression, NumericExpression)
*/
NumericExpression modulo(NumericExpression arg0, NumericExpression arg1) throws ArithmeticException;
/**
* 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.
*
* @param arg a symbolic expression of integer or real type
* @return negation: − <code>arg</code>
* @see SymbolicIntegerType
* @see SymbolicRealType
*/
NumericExpression minus(NumericExpression arg);
/**
* Concrete power operator: <i>e</i><sup><i>b</i></sup>, where <i>b</i> is a
* concrete non-negative {@link IntegerNumber}. This method might actually
* multiply out the expression, i.e., it does not necessarily return an
* expression with operator {@link SymbolicOperator#POWER}.
*
* @param base the base expression in the power expression
* @param exponent a finite non-negative concrete integer exponent
*/
NumericExpression power(NumericExpression base, IntegerNumber exponent);
/**
* Equivalent to <code>power(base, intObject(exponent))</code>.
*
* @param base the base expression in the power expression
* @param exponent a non-negative concrete integer exponent
* @return <code>power(base, intObject(exponent))</code>
*/
NumericExpression power(NumericExpression base, int exponent);
/**
* General power operator: <i>e</i><sup><i>b</i></sup>. Both <i>e</i> and
* <i>b</i> are numeric expressions.
*
* @param base the base expression in the power expression
* @param exponent the exponent in the power expression
*/
NumericExpression power(NumericExpression base, NumericExpression exponent);
// Booleans...
/**
* If the given expression has a concrete {@link Boolean} value, this returns
* it, else it returns <code>null</code>.
*
* @param expression any {@link BooleanExpression}
* @return one of the two concrete {@link Boolean} values if
* <code>expression</code> is concrete, else <code>null</code>
*/
Boolean extractBoolean(BooleanExpression expression);
/**
* Returns the boolean literal <i>true</i>.
*
* @return the symbolic expression <i>true</i>
*/
BooleanExpression trueExpression();
/**
* Returns the boolean literal <i>false</i>.
*
* @return the symbolic expression <i>false</i>
*/
BooleanExpression falseExpression();
/**
* The symbolic expression wrapping the given boolean object (true or false).
*/
BooleanExpression bool(BooleanObject object);
/**
* Short cut for symbolic(booleanObject(value)).
*
* @param value
* @return symbolic expression wrapping boolean value
*/
BooleanExpression bool(boolean value);
/**
* Returns a symbolic expression representing the conjunction of the two given
* arguments. Each argument must be non-null and have boolean type.
*
* @param arg0 a symbolic expression of boolean type
* @param arg1 a symbolic expression of boolean type
* @return conjunction of arg0 and arg1
*/
BooleanExpression and(BooleanExpression arg0, BooleanExpression arg1);
/**
* 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".
*
* @param args a sequence of expressions of boolean type
* @return the conjunction of the expressions in args
*/
BooleanExpression and(Iterable<? extends BooleanExpression> args);
/**
* Returns a symbolic expression representing the disjunction of the two given
* arguments. Each argument must be non-null and have boolean type.
*
* @param arg0 a symbolic expression of boolean type
* @param arg1 a symbolic expression of boolean type
* @return disjunction of arg0 and arg1
*/
BooleanExpression or(BooleanExpression arg0, BooleanExpression arg1);
/**
* 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".
*
* @param args a sequence of expressions of boolean type
* @return the disjunction of the expressions in args
*/
BooleanExpression or(Iterable<? extends BooleanExpression> args);
/**
* Returns a symbolic expression representing the logical negation of the given
* expression arg. arg must be non-null and have boolean type.
*
* @param arg a symbolic expression of boolean type
* @return negation of arg
*/
BooleanExpression not(BooleanExpression arg);
/**
* Returns a symbolic expression representing "p implies q", i.e., p=>q.
*
* @param arg0 a symbolic expression of boolean type (p)
* @param arg1 a symbolic expression of boolean type (q)
* @return p=>q
*/
BooleanExpression implies(BooleanExpression arg0, BooleanExpression arg1);
/**
* Returns a symbolic expression representing "p is equivalent to q", i.e.,
* p<=>q.
*
* @param arg0 a symbolic expression of boolean type (p)
* @param arg1 a symbolic expression of boolean type (q)
* @return p<=>q
*/
BooleanExpression equiv(BooleanExpression arg0, BooleanExpression arg1);
/**
* Returns expression equivalent to arg0 < arg1. The arguments must be numeric
* of the same type (i.e., both are of integer type or both are of real type).
*
* @param arg0 symbolic expression of numeric type
* @param arg1 symbolic expression of same numeric type
* @return symbolic expression of boolean type arg0 < arg1
*/
BooleanExpression lessThan(NumericExpression arg0, NumericExpression arg1);
/**
* Returns expression equivalent to arg0 <= 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).
*
* @param arg0 symbolic expression of numeric type
* @param arg1 symbolic expression of same numeric type
* @return symbolic expression of boolean type arg0 <= arg1
*/
BooleanExpression lessThanEquals(NumericExpression arg0, NumericExpression 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.
*
* @param arg0 a symbolic expression
* @param arg1 a symbolic expression
* @return symbolic expression of boolean type arg0 = arg1
*/
BooleanExpression equals(SymbolicExpression arg0, SymbolicExpression arg1);
BooleanExpression quickEquals(SymbolicExpression arg0, SymbolicExpression arg1);
/**
* Returns expression equivalent to arg0 != arg1 ("not equals").
*
* @param arg0 a symbolic expression
* @param arg1 a symbolic expression
* @return symbolic expression of boolean type arg0 != arg1
*/
BooleanExpression neq(SymbolicExpression arg0, SymbolicExpression arg1);
/**
* Returns arg with all clauses containing quantifers removed.
*
* @param arg a symbolic expression
* @return the conjunction of all quantifer-free clauses of arg.
*/
BooleanExpression removeQuantifiers(BooleanExpression arg);
/**
* Returns the universally quantified expression forall(x).e.
*
* @param boundVariable the bound variable x
* @param predicate the expression e (of boolean type)
* @return the expression forall(x).e
*/
BooleanExpression forall(SymbolicConstant boundVariable, BooleanExpression predicate);
/**
* A special case of "forall" that is very common: forall integers i such that
* low<=i<high, p(i).
*
* @param index i, a symbolic constant of integer type
* @param low a symbolic expression of integer type, lower bound of i
* (inclusive)
* @param high a symbolic expression of integer type, upper bound of i
* (exclusive)
* @param predicate some boolean symbolic expression, usually involving i
* @return an expression equivalent to "forall int i. low<=i<high -> p(i)".
*/
BooleanExpression forallInt(NumericSymbolicConstant index, NumericExpression low, NumericExpression high,
BooleanExpression predicate);
/**
* Returns the existentially quantified expression exists(x).e.
*
* @param boundVariable the bound variable x
* @param predicate the expression e (of boolean type)
* @return the expression exists(x).e
*/
BooleanExpression exists(SymbolicConstant boundVariable, BooleanExpression predicate);
/**
* A special case of "exists" that is very common: exists integer i such that
* low<=i<high and p(i).
*
* @param index i, a symbolic constant of integer type
* @param low a symbolic expression of integer type, lower bound of i
* (inclusive)
* @param high a symbolic expression of integer type, upper bound of i
* (exclusive)
* @param predicate some boolean symbolic expression, usually involving i
* @return an expression equivalent to "exists int i. low<=i<high && p(i)".
*/
BooleanExpression existsInt(NumericSymbolicConstant index, NumericExpression low, NumericExpression high,
BooleanExpression predicate);
/**
* Does the integer a divide the integer b evenly? I.e, does there exist an
* integer n such that b=a*n?
*
* @param a a symbolic expression of integer type
* @param b a symbolic expression of integer type
* @return a symbolic expression of boolean type holding iff a divides b
*/
BooleanExpression divides(NumericExpression a, NumericExpression b);
// Functions...
/**
* 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.
*
* @param boundVariable the bound variable x
* @param expression the expression e
* @return lambda(x).e
*/
SymbolicExpression lambda(SymbolicConstant boundVariable, SymbolicExpression expression);
// SymbolicExpression lambda(Collection<SymbolicConstant> boundVariables,
// SymbolicExpression expression);
/**
* 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.
*/
SymbolicExpression apply(SymbolicExpression function, Iterable<? extends SymbolicExpression> argumentSequence);
// Union type operations...
/**
* Casts an object belonging to one of the members of a union type to the union
* type.
*
* @param unionType the union type
* @param memberIndex the index of the member type of the object in the list of
* member types of the union type
* @param object an expression whose type is the member type with the given
* index
* @return an expression whose type is the union type representing the same
* object as the given object
*/
SymbolicExpression unionInject(SymbolicUnionType unionType, 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.
*
* @param memberIndex an integer in range [0,n-1], where n is the number of
* member types of the union type
* @param object an expression of the union type
* @return a boolean expression telling whether the object belongs to the
* specified member type
*/
BooleanExpression unionTest(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.
*
* @param memberIndex an integer in range [0,n-1], where n is the number of
* member types of the union types
* @param object an object whose type is the union type and for which
* unionTest(unionType, memberIndex, object) holds.
* @return a representation of the object with type the member type
*/
SymbolicExpression unionExtract(IntObject memberIndex, SymbolicExpression object);
// Arrays...
/**
* <p>
* 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.
* </p>
*
* <p>
* Precondition: every element of <code>elements</code> must have type
* <code>elementType</code>. This is <b>not</b> necessarily checked. If this
* condition is not met, behavior is undefined.
* </p>
*
* @param elementType the type of each element of <code>elements</code>
* @param elements array of symbolic expressions, each of type
* <code>elementType</code>
* @return symbolic expression of type {@link SymbolicCompleteArrayType} with
* element type <code>elementType</code> and length
* <code>elements.length</code> wrapping <code>elements</code>
*/
SymbolicExpression array(SymbolicType elementType, SymbolicExpression[] 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.
*
* @param elementType the type of each element of the array
* @param elements sequence of symbolic expressions
* @return array consisting of those elements
*/
SymbolicExpression array(SymbolicType elementType, Iterable<? extends SymbolicObject> elements);
/**
* Returns array of length 0.
*
* @param elementType the type of the non-existent elements of this array
* @return array of length 0 of given type
*/
SymbolicExpression emptyArray(SymbolicType elementType);
/**
* Returns an array in which every element has the same value.
*
* @param elementType the element type of the array
* @param length the length of the array
* @param value the value of each element
* @return an array of specified length in which every element is value
*/
SymbolicExpression constantArray(SymbolicType elementType, NumericExpression length, SymbolicExpression value);
/**
* 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
*
* @param concreteArray a concrete array
* @param element a symbolic expression whose type is compatible with
* element type of the array
* @return an array obtained by appending element to given array
*/
SymbolicExpression append(SymbolicExpression concreteArray, SymbolicExpression element);
/**
* 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
*
* @param concreteArray a concrete array
* @param index an int index
* @return 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
*/
SymbolicExpression removeElementAt(SymbolicExpression concreteArray, int index);
/**
* Inserts value an position index in array, shifting subsequence elements "up".
*
* @param concreteArray a concrete array
* @param 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.
* @param value expression to insert
* @return array obtained by inserting the element at specified index
*/
SymbolicExpression insertElementAt(SymbolicExpression concreteArray, int index, SymbolicExpression value);
/**
* Returns the length of any symbolic expression of array type. This is a
* symbolic expression of integer type.
*
* @param array a symbolic expression of array type
* @return a symbolic expression of integer type representing the length of the
* array
*/
NumericExpression length(SymbolicExpression array);
/**
* 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.
*
* @param array the given array
* @param index symbolic expression of integer type
* @return expression representing value of index-th element of the array
*/
SymbolicExpression arrayRead(SymbolicExpression array, NumericExpression index);
/**
* 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.
*
* @param array the given array
* @param index symbolic expression of integer type
* @param value the new value for the element at position index
* @return expression representing the result of changing the index-th element
* to value
*/
SymbolicExpression arrayWrite(SymbolicExpression array, NumericExpression index, SymbolicExpression value);
/**
* 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.
*
* @param array a symbolic expression of array type
* @param values a sequence of symbolic expressions, each of which is either
* null or a symbolic expression of the appropriate type
* @return the array resulting from writing to the given array in position
* 0,...,n-1, where n is the length of the sequence.
*/
SymbolicExpression denseArrayWrite(SymbolicExpression array, Iterable<? extends SymbolicExpression> values);
/**
* Returns an expression representing an array with element type T defined by a
* function f from int to T.
*/
SymbolicExpression arrayLambda(SymbolicCompleteArrayType arrayType, SymbolicExpression function);
// Tuples...
/**
* 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.
*
* @param type the tuple type
* @param components the component expressions
* @return the tuple formed from the components
*/
SymbolicExpression tuple(SymbolicTupleType type, SymbolicExpression[] components);
/**
* Returns the concrete tuple expression with the given tuple components.
*
* @param type the tuple type
* @param components the component expressions
* @return the tuple formed from the components
*/
SymbolicExpression tuple(SymbolicTupleType type, Iterable<? extends SymbolicObject> components);
/**
* 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.
*
* @param tuple the tuple value being read
* @param index index of the component to read
* @return a symbolic expression representing the component at that index
*/
SymbolicExpression tupleRead(SymbolicExpression tuple, IntObject index);
/**
* 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.
*
* @param tuple the original tuple
* @param index the index of the component to modify
* @param value the new value for the component
* @return an expression representing the new tuple
*/
SymbolicExpression tupleWrite(SymbolicExpression tuple, IntObject index, SymbolicExpression value);
// Sets...
// Under construction...
// SymbolicExpression emptySet(SymbolicSetType setType);
// SymbolicExpression singletonSet(SymbolicSetType setType,
// SymbolicExpression value);
// BooleanExpression isElementOf(SymbolicExpression value,
// SymbolicExpression set);
BooleanExpression isSubsetOf(SymbolicExpression set1, SymbolicExpression set2);
SymbolicExpression setAdd(SymbolicExpression set, SymbolicExpression value);
SymbolicExpression setRemove(SymbolicExpression set, SymbolicExpression value);
SymbolicExpression setUnion(SymbolicExpression set1, SymbolicExpression set2);
SymbolicExpression setIntersection(SymbolicExpression set1, SymbolicExpression set2);
SymbolicExpression setDifference(SymbolicExpression set1, SymbolicExpression set2);
NumericExpression cardinality(SymbolicExpression set);
// Maps...
SymbolicExpression emptyMap(SymbolicMapType mapType);
SymbolicExpression put(SymbolicExpression map, SymbolicExpression key, SymbolicExpression value);
SymbolicExpression get(SymbolicExpression map, SymbolicExpression key);
SymbolicExpression removeEntryWithKey(SymbolicExpression map, SymbolicExpression key);
SymbolicExpression keySet(SymbolicExpression map);
NumericExpression mapSize(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.
*
* @param map
* @return
*/
SymbolicExpression entrySet(SymbolicExpression map);
// Misc. expressions...
/**
* Casts expression to new type.
*
* @param newType a symbolic type
* @param expression a symbolic expression
* @return symbolic expression cast to new type
*/
SymbolicExpression cast(SymbolicType newType, SymbolicExpression expression);
/**
* "If-then-else" expression. Note that trueCase and falseCase must have the
* same type, which becomes the type of this expression.
*
* @param predicate the test condition p
* @param trueCase the value if condition is true
* @param falseCase the value if condition is false
* @return symbolic expression whose values is trueCase if predicate holds,
* falseCase if predicate is false
*/
SymbolicExpression cond(BooleanExpression predicate, SymbolicExpression trueCase, SymbolicExpression falseCase);
// References
/**
* <p>
* 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 <i>r</i> might encode "the 3rd element of the
* 2nd component". Given an expression <i>e</i> of tuple type in which the 2nd
* component has array type, that <i>r</i> specifies a particular element of a
* particular component of <i>e</i>.
* </p>
*
* <p>
* A reference may also be thought of as a <i>function</i> which takes a
* symbolic expression (of a compatible type) and returns a sub-expression of
* that expression.
* </p>
*
* @return the type of all reference expressions
*/
SymbolicType referenceType();
/**
* 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.
*
* @return the null reference
*/
ReferenceExpression nullReference();
/**
* Given a <code>reference</code> and a <code>value</code>, returns the
* sub-expression of <code>value</code> specified by the reference. Throws
* exception if the reference is not of the correct form for the type of
* <code>value</code>.
*
* @param value a non-<code>null</code> symbolic expression
* @param reference a non-<code>null</code> reference into a sub-expression of
* <code>value</code>
* @return the sub-expression of <code>value</code> specified by the reference
*/
SymbolicExpression dereference(SymbolicExpression value, ReferenceExpression reference);
/**
* Returns the type referenced by a reference into an expression of the given
* type. Example: if <code>type</code> is <i>array-of-integer</i> and
* <code>reference</code> is an array element reference, this method returns
* <i>integer</i>.
*
* @param type a non-<code>null</code> symbolic type
* @param reference a reference that is compatible with <code>type</code>, i.e.,
* can reference into an expression of that type
* @return the component of the given type which is referenced by the given
* reference
*/
SymbolicType referencedType(SymbolicType type, ReferenceExpression reference);
/**
* Returns the identity (or "trivial") reference <code>I</code>. This is the
* reference characterized by the property that <code>dereference(I,v)</code>
* returns <code>v</code> for any symbolic expression <code>v</code>.
*
* @return the identity reference
*/
ReferenceExpression identityReference();
/**
* Given a reference to an array and an <code>index</code> (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 <code>arrayReference</code> encodes "2nd component
* of element 3" and <code>index</code> is <code>X+Y</code>, the result returned
* specifies "element <code>X+Y</code> of the 2nd component of element 3".
*
* @param arrayReference a non-<code>null</code> reference for which the
* referenced sub-expression has array type
* @param index a non-<code>null</code> expression of integer type
* @return a reference to the <code>index</code>-th element of the referenced
* array
*/
ArrayElementReference arrayElementReference(ReferenceExpression arrayReference, NumericExpression index);
/**
* 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
* <code>tupleReference</code> encodes "2nd component of element 3" and
* <code>fieldIndex</code> is 15, the result returned specifies "the 15-th
* component of the 2nd component of element 3".
*
* @param tupleReference a non-<code>null</code> reference for which the
* referenced sub-expression has tuple type
* @param fieldIndex a non-<code>null</code> concrete integer object
* specifying the component of the tuple (indexed from 0)
* @return a reference to the <code>fieldIndex</code>-th element of the
* referenced tuple
*/
TupleComponentReference tupleComponentReference(ReferenceExpression tupleReference, IntObject fieldIndex);
/**
* 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.
*/
UnionMemberReference unionMemberReference(ReferenceExpression unionReference, IntObject memberIndex);
OffsetReference offsetReference(ReferenceExpression reference, NumericExpression offset);
/**
* 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.
*
* @param value a non-<code>null</code> symbolic expression
* @param reference a non-<code>null</code> reference to a subexpression of
* <code>value</code>
* @param subValue a non-<code>null</code> expression with type compatible with
* that of the referenced sub-expression of <code>value</code>
* @return the expression that results from taking <code>value</code> and
* replacing the referenced sub-expression with <code>subValue</code>
*/
SymbolicExpression assign(SymbolicExpression value, ReferenceExpression reference, SymbolicExpression subValue);
/**
* 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).
*
* @param expr a non-<code>null</code> symbolic expression
* @return set of unbound symbolic constants occurring in <code>expr</code>
*/
Set<SymbolicConstant> getFreeSymbolicConstants(SymbolicExpression expr);
/**
* Returns the result of bit-and operation for two given unsigned integers,
* those two unsigned integers are in the form of {@link NumericExpression}.
*
* @param left a non-<code>null</code> {@link NumericExpression} representing
* an unsigned integer. The length of the unsigned integer should
* be defined as a concrete integer.
* @param right a non-<code>null</code> {@link 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.
* @return a {@link NumericExpression} representing the result.
*/
NumericExpression bitand(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 {@link NumericExpression}.
*
* @param left a non-<code>null</code> {@link NumericExpression} representing
* an unsigned integer. The length of the unsigned integer should
* be defined as a concrete integer.
* @param right a non-<code>null</code> {@link 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.
* @return a {@link NumericExpression} representing the result.
*/
NumericExpression bitor(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 {@link NumericExpression}.
*
* @param left a non-<code>null</code> {@link NumericExpression} representing
* an unsigned integer. The length of the unsigned integer should
* be defined as a concrete integer.
* @param right a non-<code>null</code> {@link 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.
* @return a {@link NumericExpression} representing the result.
*/
NumericExpression bitxor(NumericExpression left, NumericExpression right);
/**
* Returns the result of bit-not operation for the given unsigned integer, the
* given unsigned integer is in the form of {@link NumericExpression}. TODO: Not
* independent with Length, and for shifts
*
* @param expression a non-<code>null</code> {@link NumericExpression}
* representing an unsigned integer. The length of the
* unsigned integer should be defined as a concrete integer.
* @return a {@link NumericExpression} representing the result.
*/
NumericExpression bitnot(NumericExpression expression);
/**
* Returns the result of bit-left-shift operation for the given unsigned
* integer, the given unsigned integer is in the form of
* {@link NumericExpression}. <br>
* Note that: all blank bits caused by shifting are filled with 0.
*
* @param left The integer will be applied with bit-shift
* @param right The integer represents the number of shifited bits.
* @return
*/
NumericExpression bitshiftLeft(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
* {@link NumericExpression}. <br>
* Note that: all blank bits caused by shifting are filled with 0.
*
* @param left The integer will be applied with bit-shift
* @param right The integer represents the number of shifited bits.
* @return
*/
NumericExpression bitshiftRight(NumericExpression left, NumericExpression right);
/**
* Returns the {@link SymbolicCompleteArrayType} representing a bitVectorType,
* which is an array of booleans with concrete length.
*
* @param length an integer representing the length of the bits of the integer
* type.
* @return a {@link SymbolicCompleteArrayType} with the base-type of boolean and
* the given length.
*/
SymbolicCompleteArrayType bitVectorType(int length);
/**
* Returns the conversion of a bit vector from an integer.
*
* @param integer a non-<code>null</code> {@link SymbolicExpression}
* representing an integer.
* @param bitVectorType a non-<code>null</code>
* {@link SymbolicCompleteArrayType} representing the type
* of bit vector with a type of boolean and a
* <strong>concrete</strong> length.
* @return a non-<code>null</code> {@link SymbolicExpression} representing a bit
* vector.
*/
SymbolicExpression integer2Bitvector(NumericExpression integer, SymbolicCompleteArrayType bitVectorType);
/**
* Converts a bit vector to an integer.
*
* Pre-conditions: The type of <code>bitvector</code> should be a
* {@link SymbolicCompleteArrayType} whose element type is Boolean with a
* <strong>concrete</strong> length.
*
* @param bitvector a non-<code>null</code> {@link SymbolicExpression}
* representing a bit vector.
* @return a non-<code>null</code> {@link SymbolicExpression} representing an
* integer.
*/
NumericExpression bitvector2Integer(SymbolicExpression bitvector);
/**
* <p>
* <b>Summary:</b>Set name (path) for prover unexpected error file.
* </p>
* <p>
* <b>Details: </b>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.
* </p>
*
* @param errFile The desired prover error file name.
*/
void setErrFile(String errFile);
/**
* <p>
* <b>Summary:</b>Get the name (path) of the prover unexpected error file. For
* details of the error file see {@link #setErrFile(String)}
* </p>
*
* @return The String type filename (including path)
*/
String getErrFile();
/**
* 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.
*
* @param expr the symbolic expression to print
* @param out the stream to which the output will be sent
*/
void printCompressed(SymbolicExpression expr, PrintStream out);
/**
* <p>
* Use this method to print large symbolic expression hierarchically.
* </p>
*
* @param prefix any string the callers of this method want to put at the
* beginning of each line.
* @param expr the input symbolic expression
* @param out the output stream
*/
void printCompressedTree(String prefix, SymbolicExpression expr, PrintStream out);
/**
* <p>
* print symbolic expression as tree structure
* </p>
*
* @param expr the input symbolic expression
* @param out the output stream
*/
void printExprTree(SymbolicExpression expr, PrintStream out);
/**
* Substitute the given {@link SymbolicExpression} expression by repeatedly
* applying the method {@link #apply(SymbolicExpression)} until no more
* substitution can happen.
*
* @param substituteMap
* @param expression
* @return The new predicate which is done the fully substitution.
*/
SymbolicExpression fullySubstitute(Map<SymbolicExpression, SymbolicExpression> substituteMap,
SymbolicExpression expression);
/**
* Get the current upper bound of the integer length.
*
* @return the maximum bit-length of the integer type
*/
int getIntegerLengthBound();
/**
* Set the upper bound of the length of the integer type.
*
* @param bound
* @return <code>true</code>
*/
boolean setIntegerLengthBound(int bound);
/**
* Returns the function which is the <code>degree</code>-th derivative of
* <code>function</code> with respect to the <code>index</code>-th parameter.
*
* @param function a function of <i>n</i> real variables, for some <i>n</i> at
* least 1
* @param index the parameter index, an integer greater than or equal to 0
* and less than <i>n</i>
* @param degree a non-negative integer, the number of times to differentiate
* @return the function which is the derivative; it has the same signature as
* the given <code>function</code>
*/
SymbolicExpression derivative(SymbolicExpression function, IntObject index, IntObject degree);
/**
* Returns an expression of boolean type which encodes the claim that a function
* is differentiable on a closed interval in R^n.
*
* @param function the function from R^n to R, for some n at least 1
* @param degree the maximal degree of the derivatives which exist and are
* continuous, a nonnegative integer
* @param lowerBounds lower bounds of the domain intervals; a sequence of
* real-valued expressions of length n
* @param upperBounds upper bounds of the domain intervals; a sequence of
* real-valued expressions of length n
* @return a boolean expression encoding the differentiability claim
* @see SymbolicOperator#DIFFERENTIABLE
*/
BooleanExpression differentiable(SymbolicExpression function, IntObject degree,
Iterable<? extends NumericExpression> lowerBounds, Iterable<? extends NumericExpression> upperBounds);
/**
* Returns a symbolic expression of a {@link SymbolicUninterpretedType}.
*
* @param type an instance of {@link SymbolicUninterpretedType}
* @param key an concrete integral key of the returning symbolic expression.
* @return a symbolic expression of a {@link SymbolicUninterpretedType}.
*/
SymbolicExpression concreteValueOfUninterpretedType(SymbolicUninterpretedType type, IntObject key);
/**
* The result of analyzing certain "forall" expressions. The expression must be
* equivalent to
*
* <pre>
* forall int i . lowerBound <= i <= upperBound -> body
* </pre>
*
* @author siegel
*/
public class ForallStructure {
/**
* The integer bound variable used in the forall expression.
*/
public NumericSymbolicConstant boundVariable;
/**
* The lower bound (inclusive) of the bound variable.
*/
public NumericExpression lowerBound;
/**
* The upper bound (inclusive) of the bound variable.
*/
public NumericExpression upperBound;
/**
* The body of the expression: the boolean formula that is claimed to hold if i
* is between the lower and upper bounds (inclusive).
*/
public BooleanExpression body;
}
/**
* Attempts to find a boolean expression equivalent to <code>forallExpr</code>
* but with the structure
*
* <pre>
* forall int i . a≤i≤b -> e
* </pre>
*
* 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
*
* <pre>
* forall int i . !(a≤i) || !(i≤b) || e
* </pre>
*
* i.e.,
*
* <pre>
* forall int i . i≤a-1 || b+1≤i || e
* </pre>
*
* @param forallExpr an expression with operator {@link SymbolicOperator#FORALL}
* @return a structure specifying the components above if the forall expression
* has the special form, else <code>null</code>
*/
ForallStructure getForallStructure(BooleanExpression forallExpr);
/**
* Decomposes an expression as a sum of terms, returning those terms as an
* array.
*
* @param expr a numeric symbolic expression
* @return an array of numeric expressions such that the sum of the elements of
* that array equals the given expression
*/
NumericExpression[] getSummands(NumericExpression expr);
/**
* Attempts to expand an expression as a sum of simpler expressions.
*
* @param expr a numeric expression, non-<code>null</code>
* @return an array of expressions whose sum is equivalent to <code>expr</code>
*/
NumericExpression[] expand(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.
*
* @param expr an expression of real type
* @return the floor of {@code expr}, the greatest integer less than or equal to
* {@code expr}
*/
NumericExpression floor(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.
*
* @param expr an expression of real type
* @return the ceil of {@code expr}, the least integer greater than or equal to
* {@code expr}
*/
NumericExpression ceil(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).
*
* @param expr an expression of real type
* @return the result of rounding {@code expr} towards 0
*/
NumericExpression roundToZero(NumericExpression expr);
/* ************* value set template & value set references ***************/
/**
* <p>
* Given a symbolic type of a symbolic value and a list of
* {@link ValueSetReference}s, returns symbolic expression representing a value
* set template.
* </p>
*
* <p>
* A value set template consists of a type <code>t</code> of some value and a
* set of ValueSetReferences. Applying a value set template to a symbolic value
* <code>v</code> of the type <code>t</code> results in a subset of the value
* <code>v</code>.
* </p>
*
* @param type symbolic type of some value <code>v</code>
* @param vsRefs references to subsets of some value <code>v</code>
* @return a symbolic expression which is a value set template
*/
SymbolicExpression valueSetTemplate(SymbolicType valueType, ValueSetReference vsRefs[]);
/**
* Returns the set of {@link ValueSetReference}s in the given value set
* template.
*
* @param valueSetTemplate a symbolic expression of
* {@link #valueSetTemplateType()}
* @return an {@link Iterable} collection of {@link ValueSetReference}s in the
* given value set template
*/
Iterable<ValueSetReference> valueSetReferences(SymbolicExpression valueSetTemplate);
/**
* Returns the {@link SymbolicType} of values, to which the given value set
* template refers.
*
* @param valueSetTemplate a symbolic expression of
* {@link #valueSetTemplateType()}
* @return the type of the values, to which the given value set template refers
*/
SymbolicType valueType(SymbolicExpression valueSetTemplate);
/**
* 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
* {@link SymbolicExpression}, in order to obtain a subset of the value.
*
* @return The symbolic type of a value set template.
*/
SymbolicType valueSetTemplateType();
/**
* <p>
* Test if a value set template <code>vst0</code> contains another value set
* template <code>vst1</code>.
* </p>
*
* <p>
* A value set template <code>vst0</code> contains another value set template
* <code>vst1</code> iff 1) both of them are associated with the same symbolic
* type; 2) all the value set references in <code>vst1</code> are contained by
* value set references in <code>vst0</code>.
* </p>
*
* @param vst0 a value set template
* @param vst1 a value set template
* @return a boolean expression representing the result of the test
*/
BooleanExpression valueSetContains(SymbolicExpression vst0, SymbolicExpression vst1);
/**
* <p>
* 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.
* </p>
*
* @param vst0 a value set template
* @param vst1 a value set template
* @return the condition that is true iff the two value set templates have no
* intersection
*/
BooleanExpression valueSetNoIntersect(SymbolicExpression vst0, SymbolicExpression vst1);
/**
* <p>
* Given two value set templates, returns their set difference.
* </p>
*/
SymbolicExpression valueSetDiff(SymbolicExpression vst0, SymbolicExpression vst1);
/**
* <p>
* Given two value set templates, returns the union of the two.
* </p>
*
* <p>
* 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.
* </p>
*
* @param vst0 a value set template
* @param vst1 a value set template
* @return the union of two value set templates
*/
SymbolicExpression valueSetUnion(SymbolicExpression vst0, SymbolicExpression vst1);
Pair<SymbolicExpression, Integer> valueSetHavoc(SymbolicExpression value, SymbolicExpression valueSetTemplate,
String prefix, int startCount);
/**
* <p>
* Copies a subset of a value <code>v</code> to another value <code>v'</code>
* with a given value set template. Returns the value after the copy operation.
* </p>
*
* @param oldValue a symbolic expression whose type is same as the one
* that is associated with the given value set template
* @param valueSetTemplate a value set template
* @param newValue a symbolic expression whose type is same as the one
* that is associated with the given value set template
* @return 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"
*/
SymbolicExpression valueSetAssigns(SymbolicExpression oldValue, SymbolicExpression valueSetTemplate,
SymbolicExpression newValue);
/**
* @return the symbolic type of {@link ValueSetReference}
*/
SymbolicType valueSetReferenceType();
/**
* 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.
*/
VSIdentityReference vsIdentityReference();
/**
* 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
*/
VSArrayElementReference vsArrayElementReference(ValueSetReference parent, NumericExpression index);
/**
* 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(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 step 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(ValueSetReference parent, NumericExpression lower,
NumericExpression upper, NumericExpression step);
/**
* 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).
*/
VSTupleComponentReference vsTupleComponentReference(ValueSetReference parent, IntObject fieldIndex);
/**
* 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).
*/
VSUnionMemberReference vsUnionMemberReference(ValueSetReference parent, IntObject memberIndex);
/**
* 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).
*/
VSOffsetReference vsOffsetReference(ValueSetReference parent, NumericExpression offset);
}