All Classes and Interfaces
Class
Description
A reference to an element of an array.
A symbolic expression of boolean type.
A symbolic object wrapping a single boolean value.
A
SymbolicConstant of boolean type.
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.
This is the public interface for managing SARL configuration objects and
files.
A constant, i.e., a concrete number.
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.
An ExpressionFactory is used to instantiate instances of SymbolicExpression.
This class provides static methods for producing factories that create
various kinds of
SymbolicExpression.Entry point for the ideal module, providing static methods to create an
.
IdealFactory and a
invalid reference
SimplifierFactory
An
IdealFactory provides a few services beyond those guaranteed by an
arbitrary NumericExpressionFactory.An instance of this class represents an integer number.
An instance of Interval represents a numeric interval.
A symbolic object wrapping a single Java "int" value.
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 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
SymbolicConstant which has integer or real type, i.e., type
belonging to SymbolicIntegerType or SymbolicRealType.A factory for producing certain
SymbolicObjects.A reference to some point which is specified by an integer "offset" from
another reference.
A polynomial: an expression which is the sum of monomials.
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.
This is the entry point for module prove.
A data structure that represents the interpretation of a
.
invalid reference
LogicFunctionAbstract 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.A
RationalExpression is the quotient of two Monomials of real
type.An instance of this class represents a rational number.
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".
A factory for producing instances of
Reasoner.
An expression representing a way to reference into values.
The different kinds of references.
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.
Entry point for module "simplify", providing static method to create basic
range factories and context partitions
A symbolic object wrapping a single String.
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.
Represents a symbolic range of integer values.
Factory for creating and manipulating
SymbolicRange's.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.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.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.
A reference into a specified field of a tuple value.
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.
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).