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] |