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