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 <= j < n,
ARRAY_READ(a, i) = vj.
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").
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.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
SymbolicIntegerTypeA partial implementation of
SymbolicObject.an implementation of
SymbolicRealTypeAn 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-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 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 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
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
Comparator on Monics.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.
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.
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.
A
Comparator on SymbolicTypes.This class provides a static method for the creation of a new
SymbolicTypeFactory.compares two
SymbolicTypeSequenceA 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.