A | |
A [SrkUtil] | |
Abstract |
Symbolic abstraction routines.
|
B | |
BigO |
Simplification for Big-O expressions.
|
C | |
CHC [SrkZ3] |
Constrained Horn Clauses
|
ContextTable [Syntax] |
A context table is a hash table mapping contents to values.
|
CoordinateSystem |
A coordinate system is a bijection between a set of coordinates and a set
of terms.
|
D | |
DisjointSet |
Disjoint set data structure
|
E | |
Env [SrkApron] | |
Env [Syntax] |
Environments are maps whose domain is a set of free variable symbols.
|
Expr [Syntax] | |
F | |
FeatureTree |
A feature tree organizes a collection by vectors of integer features.
|
Formula [Syntax] | |
H | |
HT [Syntax.Expr] | |
HT [DisjointSet.Make] | |
I | |
I [SrkUtil.Int] | |
Infix [Syntax] | |
Int [SrkUtil] | |
Interpretation |
An interpretation is a mapping from symbols to values.
|
Interval |
Operations for manipulating numeric intervals.
|
Iter [Transition.Make] |
Iteration domain.
|
Iteration |
Approximate transitive closure computation.
|
L | |
Linear |
Various operations for the vector space
int -> QQ
|
Log |
Logging
|
M | |
Make [Transition] | |
Make [Memo.Tabulate] | |
Make [Memo] |
Functorized memoization with user-defined hash function.
|
Make [DisjointSet] | |
Make [Log] | |
MakeContext [Syntax] | |
MakeRec [Memo.Tabulate] | |
MakeSimplifyingContext [Syntax] |
Create a context which simplifies expressions on the fly
|
Map [Syntax.Expr] | |
Map [Syntax.Symbol] | |
Map [SrkUtil.Int] | |
Memo |
Function memoization
|
Monomial [Polynomial] |
Monomials
|
Mvp [Polynomial] |
Multi-variate polynomials
|
N | |
Nonlinear |
Operations for manipulating non-linear terms and formulas.
|
P | |
Polyhedron |
Convex polyhedra.
|
Polynomial |
Polynomials and Grobner bases.
|
Q | |
Unbounded rationals
| |
QQMatrix [Linear] | |
QQVector [Linear] | |
QQX [Polynomial] |
Univariate polynomials with rational coefficients
|
Quantifier |
Satisfiability via strategy improvement
|
R | |
Rewrite [Polynomial] |
Rewrite systems for multi-variate polynomials.
|
RingMap [Linear] |
Lift a map type over a ring to a left-module
|
S | |
Set [Syntax.Expr] | |
Set [Syntax.Symbol] | |
Set [SrkUtil.Int] | |
SetMap [DisjointSet.Make] | |
Smt |
Common interface for SMT solvers
|
Solver [SrkZ3] | |
Solver [Smt] | |
Split [Iteration] | |
SrkApron |
Interface to Apron numerical
abstract domain library
|
SrkSimplify |
Formula and term simplification.
|
SrkUtil |
Common utility functions
|
SrkZ3 |
Interface to Z3 SMT solver
|
Sum [Iteration] | |
Symbol [Syntax] | |
Syntax |
Defines Formulas, Terms, Symbols, Types, and Contexts.
|
T | |
Tabulate [Memo] | |
Term [Syntax] | |
TermPolynomial [SrkSimplify] | |
Transition |
Transition formulas.
|
U | |
Uvp [Polynomial] |
Univariate polynomials over a given ring
|
V | |
V [Polyhedron] | |
W | |
Wedge |
Wedge abstract domain.
|
WedgeMatrix [Iteration] | |
WedgeVector [Iteration] | |
WedgeVectorOCRS [Iteration] | |
Z | |
ZZ |
Unbounded integers
|
ZZVector [Linear] |