| SrkUtil |
Common utility functions
|
| Log |
Logging
|
| DisjointSet |
Disjoint set data structure
|
| Memo |
Function memoization
|
| FeatureTree |
A feature tree organizes a collection by vectors of integer features.
|
Unbounded rationals
| |
| ZZ |
Unbounded integers
|
| Syntax |
Defines Formulas, Terms, Symbols, Types, and Contexts.
|
| Interval |
Operations for manipulating numeric intervals.
|
| Smt |
Common interface for SMT solvers
|
| SrkZ3 |
Interface to Z3 SMT solver
|
| Linear |
Various operations for the vector space
int -> QQ
|
| Polynomial |
Polynomials and Grobner bases.
|
| Interpretation |
An interpretation is a mapping from symbols to values.
|
| SrkApron |
Interface to Apron numerical
abstract domain library
|
| Polyhedron |
Convex polyhedra.
|
| SrkSimplify |
Formula and term simplification.
|
| Abstract |
Symbolic abstraction routines.
|
| Nonlinear |
Operations for manipulating non-linear terms and formulas.
|
| CoordinateSystem |
A coordinate system is a bijection between a set of coordinates and a set
of terms.
|
| Wedge |
Wedge abstract domain.
|
| Quantifier |
Satisfiability via strategy improvement
|
| Iteration |
Approximate transitive closure computation.
|
| Transition |
Transition formulas.
|
| BigO |
Simplification for Big-O expressions.
|