Index of modules


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