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