All Classes and Interfaces

Class
Description
A reference to an element of an array.
Simple implementation of Iterable backed by an array.
 
Briefly, this transformer canonicalizes all bound variable names of the lambda expressions in array lambdas.
 
Simplifies a symbolic expression of the form ARRAY_READ(a, i): if the array has the form a = ARRAY_WRITE(a', i', v) if i == i', ARRAY_READ(a, i) = v if i != i', ARRAY_READ(a, i) = ARRAY_READ(a', i) otherwise, no simplification if the array has the form a = DENSE_ARRAY_WRITE(a', {v0, v1, ..., vn-1}) if i == j, 0 &lt= j &lt n, ARRAY_READ(a, i) = vj. if n &lt= i,, ARRAY_READ(a, i) = ARRAY_READ(a', i) otherwise, no simplification if the array has the form a = ARRAY(c, c, ..., c) where c is a constant and 0 &lt= i &lt length(a), ARRAY_READ(a, i) = c
A binary operator on a type T is an object which provides a method "apply" which takes two elements of T and returns an element of T.
A binary operator on a type T is an object which provides a method "apply" which takes two elements of T and returns a boolean.
A symbolic expression of boolean type.
 
A symbolic object wrapping a single boolean value.
A representation of a BooleanExpression using Conjunctive Normal Form.
A SymbolicConstant of boolean type.
Replaces all bound variables in expressions with new ones so that each has a unique name and a name different from any unbound symbolic constant (assuming no one else uses the "special string").
Replaces all bound variables in expressions with new ones so that each has a unique name and a name different from any unbound symbolic constant (assuming no one else uses the "special string").
A substituter used to assign new, canonical names to all symbolic constants occurring in a sequence of expressions.
A symbolic object wrapping a single char value.
A CNF factory is an implementation of BooleanExpressionFactory that works by putting all boolean expressions into a conjunctive normal form.
 
CommonArrayElement Reference extends the CommonNTReference superclass and implements the ArrayElementReference interface.
 
A substituter used to assign new, canonical names to all symbolic constants occurring in a sequence of expressions.
 
Implementation of ContextPartition.
CommonExpressionFactory is used to create many CommonExpressions.
 
 
An implementation of IdealFactory.
The identity reference I, which is characterized by the property that dereference(value, I)==value for any symbolic expression value.
Immutable implementation of Interval.
 
Straightforward implementation of ModelResult using a Java Map to store the mapping of symbolic constants to their concrete values.
A standard implementation of NTReferenceExpression, used to represent a non-trivial reference.
 
The "null reference" is a useless reference value not equal to any of the other reference values and which cannot be dereferenced.
 
Given a numeric factory that deals with expressions of ideal type, and a numeric factory that deals with expressions of herbrand type, this factory puts them together to work on any numeric type.
A straightforward implementation of ObjectFactory.
CommonOfsetReference extends the CommonNTReference superclass and implements the OffsetReference interface.
 
Very simple implementation of ProverInfo.
A very basic implementation of Reasoner based on a given Simplifier and TheoremProverFactory.
Basic factory for producing instances of CommonReasoner.
Abstract Reference Symbolic Expression.
An implementation of SARLConfig using an array for the ProverInfos as well as a map from the prover names to the ProverInfos for fast lookup.
 
 
 
A "symbolic constant" is a symbol used in symbolic execution to represent an input value.
 
an implementation of SymbolicIntegerType
 
A partial implementation of SymbolicObject.
 
an implementation of SymbolicRealType
 
 
 
An implementation of SymbolicTypeFactory.
An implementation of SymbolicTypeSequence which is a finite, ordered sequence of SymbolicType.
 
 
A standard implementation of SymbolicUniverse, relying heavily on a given NumericExpressionFactory for dealing with numeric issues and a BooleanExpressionFactory for dealing with boolean expressions.
Implementation of a non-trivial reference to a TupleComponent
Implementation of a non-trivial reference to a UnionMember
Straightforward implementation of ValidityResult.
A general implementation of ValueSetReference.
 
 
 
 
 
 
 
 
Attempt to transform the expression e := (a0 + a1 + ..., an-1) % x to its equivalence e' := (a0%x + a1%x + ..., an-1%x) % x iffe' has a smaller size than e AND all a0, a1, ..., an-1 are non-negative
Used to simplify a conditional symbolic expression p?a:b.
Used to simplify a conditional symbolic expression p?a:b.
Factory for producing and manipulating SARL configuration files and SARLConfig objects.
This is the public interface for managing SARL configuration objects and files.
A constant, i.e., a concrete number.
A structured representation of a boolean formula (assumption), used for simplifying symbolic expressions.
A context extractor is used to build up a Context by consuming a BooleanExpression.
A context is an abstract representation of a boolean expression suitable for normalizing (simplifying) other expressions under the assumption that the context holds.
A Reasoner based on context minimization.
A factory for producing instances of ContextMinimizingReasoner.
Provides a partition of the set of conjunctive clauses of a BooleanExpression (the context) and a method to use that partition for context minimization.
A CoreUniverse provides most of the functionality of a SymbolicUniverse, including the mechanisms to create and manipulate SymbolicExpressions and other SymbolicObjects.
The result of analyzing certain "forall" expressions.
This is a class provides a PowerReal theory for CVC translator.
A CVCTranslator object is used to translate a single symbolic expression to the language of CVC.
 
 
 
An immutable, empty set.
The parent of all EvalNodeInt nodes
 
The parent of all EvalNodeRat nodes
An efficient implementation of raising something to some power.
Comparator of symbolic expressions.
An ExpressionFactory is used to instantiate instances of SymbolicExpression.
This class provides static methods for producing factories that create various kinds of SymbolicExpression.
A generic, abstract class for performing substitutions on symbolic expressions.
An object for storing some information about the state of the search through a symbolic expression.
Walks a symbolic expression to collect all free (unbound) symbolic constants occurring anywhere in that expression.
 
An object used to determine whether an expression is equivalent to 0 within some probability.
An efficient doubly-linked list.
 
Performs Gaussian Elimination on the numeric entries of a Context's substitution map.
 
 
 
 
 
Implementation of SymbolicExpression in which every argument belongs to some type T which extends SymbolicObject.
Entry point for the ideal module, providing static methods to create an IdealFactory and a SimplifierFactory.
Comparator for ideal numeric expressions.
An IdealFactory provides a few services beyond those guaranteed by an arbitrary NumericExpressionFactory.
An implementation of Simplifier for the "ideal" numeric factory IdealFactory.
A factory for producing new instances of IdealSimplifier.
An ideal simplifier worker is created to simplify one symbolic expression.
A SymbolicConstant which is also a Primitive.
A trivial implementation of Simplifier which does nothing: given an expression, it returns the expression unchanged.
Factory for producing instances of IdentitySimplifier.
Thrown when it has been determined that a @{link Context} is inconsistent, i.e., equivalent to false.
An instance of this class represents an integer number.
An instance of Interval represents a numeric interval.
 
Implementation of Range in which a set is represented as a finite union of intervals.
A symbolic object wrapping a single Java "int" value.
A collection representing the disjoint union of two collections.
 
A set representing the union of two *disjoint* sets.
 
 
A class used to simplify a constant map by applying linear reasoning.
A structured representation of a set of Monics.
A substituter specified by giving an explicit Java Map from SymbolicExpression to SymbolicExpression to specify the base substitutions.
 
A result to a validity query which also requested a model in case the answer was "NO", and for which the answer was "NO".
A Monic is a product of powers of primitive expressions x1i 1*...*xnin, where the x i are primitives and the ij are positive concrete ints.
A Monomial is the product of a constant and a Monic.
 
An implementation of TheoremProver which wraps a sequence of underlying TheoremProvers.
A factory for producing instances of MultiProver.
A substituter used to change the names of symbolic constants.
 
 
A constant which is not 1.
A non-trivial monic ("NTMonic") is the product of at least two PrimitivePowers.
A non-trivial Monomial is the product of a Constant and a Monic.
An NTPolynomial ("non-trivial polynomial") is the sum of at least 2 Monomials with different underlying monics, e.g., 1+x 2, x+y, or x+xy.
A non-trivial primitive power represents a Primitive expression raised to some concrete integer exponent; the exponent is at least 2.
A nontrivial RationalExpression.
A non-trivial ReferenceExpression, i.e., one which is not the null reference or the identity reference.
A non-trivial ValueSetReference, i.e., one which is not the identity reference.
A number is some kind of representation of a real number.
A number factory is used to produce concrete rational and integer numbers.
A simple type for recording the result of attempting to take the union of two intervals i1 and i2.
A symbolic object wrapping a single instance of Number.
 
Marker interface for an expression of numeric type ( SymbolicIntegerType SymbolicRealType).
A NumericExpressionFactory provides all of the functionality needed to create and manipulate expressions of numeric type.
 
A numeric primitive expression---one which is to be considered as an atomic "variable" when used in other numeric expressions.
A SymbolicConstant which has integer or real type, i.e., type belonging to SymbolicIntegerType or SymbolicRealType.
The default Comparator on all SymbolicObjects.
A factory for producing certain SymbolicObjects.
 
A reference to some point which is specified by an integer "offset" from another reference.
Empty monic: equivalent to 1.
Some things that should happen: all clauses involving inequalities/equations on the same monic should be combined and unified.
An ordered pair.
A polynomial: an expression which is the sum of monomials.
 
A simplification that applies to expressions in which the operator is SymbolicExpression.SymbolicOperator.POWER.
A Predicate on type T is an object that provides a method "apply" which takes an element of T and returns true or false.
A PreUniverse provides most of the services of a SymbolicUniverse, but not those that require reasoning, specifically theorem proving and simplification.
 
A numeric primitive expression, e.g., a symbolic constant of numeric type, an array read expression of numeric type, or a tuple read expression of numeric type.
A Comparator on Primitives, using the same order as that of IdealComparator.
A power of a Primitive expression, xi, where x is a Primitive and i is a concrete positive int.
Utility class providing means to control processes.
This is the entry point for module prove.
A data structure that represents the interpretation of a LogicFunction.
Abstract interface representing information about an external theorem prover: what kind of prover it is, where it can be found, etc.
A classification of the different kinds of theorem provers.
 
An abstract representation of a set of Numbers.
A categorization of ranges based on their relationship to 0.
Factory for producing instances of Range.
Normalizes the range map of a Context.
A RationalExpression is the quotient of two Monomials of real type.
A key used in the rational map.
An instance of this class represents a rational number.
 
An abstract class represents the infinite real number.
An infinite precision representation of integer numbers, based on Java's BigInteger class.
A representation of the integral infinity, it could be either postive or negative.
 
An implementation of number factory based on infinite precision real arithmetic.
An infinite precision representation of the mathematical rational numbers.
A representation of the rational infinity, it could be either postive or negative.
Provides a static method for producing a new ReasonerFactory.
A reasoner provides methods to simplify SymbolicExpressions and prove or disprove certain theorems, all under an over-arching assumption known as the "context".
The key of cached Reasoners which is a pair of a BooleanExpression which represents the context and an array of ProverFunctionInterpretation
A factory for producing instances of Reasoner.
An expression representing a way to reference into values.
The different kinds of references.
 
An implementation of TheoremProver using one of the automated theorem provers CVC3 or CVC4.
Factory for producing new instances of RobustCVCTheoremProver.
 
 
An implementation of TheoremProver using the automated theorem provers Z3.
Factory for producing new instances of RobustCVCTheoremProver.
The SARL class provides static methods for creating new symbolic universes.
An exception that occurs when an index is out of bounds.
A SARL configuration encapsulates information about the complete set of external theorem provers available to SARL.
 
Root of the SARL exception type hierarchy.
A SARL internal exception represents an error that is "not supposed to happen." It can be used like an assertion, whenever you feel that something should always be true.
 
A SetFactory is used to manipulate arrays as if they were sets.
Very basic reasoner that does not use any theorem prover, only simplification.
Implementation based on arrays.
A substituter specified by a single symbolic constant and a value that is to replace that symbolic constant.
A Simplification takes a SymbolicExpression and returns an equivalent SymbolicExpression in a simplified form.
An enumerated type corresponding 1-1 with the different Simplification classes.
A simplifier is an object for simplifying symbolic expressions.
A factory for producing instances of Simplifier.
An object that gathers together a variety of objects as fields needed to perform simplification.
Entry point for module "simplify", providing static method to create basic simplifiers, simplifier factories, and range factories.
Simple implementation of Iterator for iterating over a sequence consisting of a single element.
 
 
 
Transform sigma (sum) expressions to the forms that are accepted by all provers
A symbolic object wrapping a single String.
A sub-context represents a boolean expression that holds within the context of some other assumption.
A Simplification that proceeds by creating a SubContext of the current Context to process a BooleanSymbolicExpression.
Simplifies the context's substitution map.
An array type T[].
A complete array type specifies not only the element type but also the extent (length) of the array.
A "symbolic constant" is a symbol used in symbolic execution to represent an input value.
An instance SymbolicExpression represents a symbolic expression.
An enumerated type for the different kinds of symbolic expressions.
A function type is specified by the number and types of inputs, and a single output type.
SymbolicIntegerType is an interface that contains representation for a Symbolic Integer Type: It has three kinds: - herbrand: it doesn't do simplifications, when used in equations - ideal: - bounded: Also it has a method to return the kind of the integer.
three kinds for the integer type
T map type is a type consisting of two components: a key type K and a value type V.
The root of the symbolic object type hierarchy.
 
A real number type.
The different kinds of real types.
A finite ordered immutable sequence of symbolic expressions.
The type representing a set.
A tuple type is specified by (1) a name, and (2) an ordered, finite sequence of component types.
A symbolic type represents the type of a symbolic expression.
The different kinds of types.
A factory used to produce SymbolicTypes and other related objects.
A finite, ordered sequence of SymbolicType.
This class represents uninterpreted types.
A union type of a sequence of types t_i.
A symbolic universe is used for the creation and manipulation of SymbolicObjects.
A substituter that replaces certain function calls with their truncated Taylor polynomial expansions.
 
 
 
Provides an abstract interface for an automated theorem prover operating under a fixed context (i.e., a boolean expression assumed to hold).
 
A factory for producing instances of TheoremProver.
Given a partial order lt on T.
A Transform from type S to type T is an object that provides a method "apply" which takes an element of S and returns an element of T.
This class is used to deal with integer division or modulo during the CVC translation.
A reference into a specified field of a tuple value.
Simplify non-concrete tuple type expressions to concrete tuples.
This class provides a static method for the creation of a new SymbolicTypeFactory.
A UnaryOperator on a type T is an object which provides a method "apply" that takes an element of T and returns an element of T.
A reference to a member of a SymbolicUnionType.
This class provides static methods for the creation of new SymbolicUniverses.
 
A ValidityResult represents the result of a validity query.
The 3 kinds of results to the "valid" question: yes, no, or maybe (a.k.a, "I don't know").
 
The different kinds of reference set elements.
A reference to an (set-of) element(s) of a (set-of) array value(s).
A reference to a (set-of) section(s) of a (set-of) array(s).
A reference to a single object value.
A reference to some point(s) which is specified by an integer "offset" from another value set reference.
The factory provides interfaces for creating instances of ValueSetReferences operations over ValueSetReferences
A reference into a (set-of) specified field(s) of a (set-of) tuple value(s).
A reference to a (set-of) members of a (set-of) union value(s).
 
A translation of permut(a, b, l, h) predicate, where a, b are arrays and l, h are integral bounds.
This class provides a set of Why3 primitives, including types and operations, to help the translation.
 
Libraries in Why3.
A factory that generates new Why3Reasoners.
This class manages all stateful informations that are needed during the translation from SARL to Why3.
Translates SARL SymbolicExpressions to the why3 (logic) language of the verification platform Why3 ( why3-website).
A special kind of map for use in "work list" algorithms.
Translates SARL SymbolicExpressions to the language of the automated theorem prover Z3.