# 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', {v`_{0},
v_{1}, ..., v_{n-1}})

if `i == j, 0 <= j < n`

,
`ARRAY_READ(a, i) = v`_{j}

.
if ` n <= 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 <= i < 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").

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.

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`

.Basic factory for producing instances of

`CommonReasoner`

.Abstract Reference Symbolic Expression.

An implementation of

`SARLConfig`

using an array for the
`ProverInfo`

s as well as a map from the prover names to the
`ProverInfo`

s 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 := (a
```_{0} + a_{1} + ..., a_{n-1}) % x

to its equivalence ```
e' := (a
```_{0}%x + a_{1}%x + ..., a_{n-1}%x) % x

iff`e'`

has a smaller size than `e`

AND all
```
a
```_{0}, a_{1}, ..., a_{n-1}

are non-negativeUsed 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 `SymbolicExpression`

s and other `SymbolicObject`

s.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`

nodesThe parent of all

`EvalNodeRat`

nodesAn 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

`Monic`

s.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 x

_{1}^{i 1}*...*x_{n}^{in}, where the x_{i}are primitives and the i_{j}are positive concrete ints.A

`Comparator`

on `Monic`

s.An implementation of

`TheoremProver`

which wraps a sequence of
underlying `TheoremProver`

s.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

`PrimitivePower`

s.
An

`NTPolynomial`

("non-trivial polynomial") is the sum of at least 2
`Monomial`

s 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 `SymbolicObject`

s.A factory for producing certain

`SymbolicObject`

s.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.

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

`Number`

s.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 `Monomial`

s 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

`SymbolicExpression`

s and prove
or disprove certain theorems, all under an over-arching assumption known as
the "context".The key of cached

`Reasoner`

s 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

`SymbolicType`

s 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

`SymbolicObject`

s.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.

A

`Comparator`

on `SymbolicType`

s.This class provides a static method for the creation of a new

`SymbolicTypeFactory`

.compares two

`SymbolicTypeSequence`

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

`SymbolicUniverse`

s.
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

`ValueSetReference`

s
operations over `ValueSetReference`

s
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

`Why3Reasoner`

s.This class manages all stateful informations that are needed during the
translation from SARL to Why3.

Translates SARL

`SymbolicExpression`

s 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

`SymbolicExpression`

s to the language of the automated
theorem prover Z3.