Index of modules

evaluation, not affecting function bodies

Symbols

Reducing patterns of the form select(update(a,i,x), j) according to the equations select(create(a), j) = a i = j => select(update(a,i,x), j) = x i <> j => select(update(a,i,x),j) = select(a,j)

Set of atoms

Creating fresh bitvector variables for solver.

Constants

update x i s updates the constraint map with the constraint x in i and modifies the use lists accordingly.

Decision procedure state

Fold iterator

Known disequalities; x |-> {y,z} is interpreted as x <> y & x <> z.

Union of two domains

Given two rational numbers a, b, euclid finds integers , y0 satisfying a * x0 + b * y0 = (a, b), where (a, b) denotes the greatest common divisor of a, b.

Exceptions that are used throughout ICS.

modified by

raise Sys.Break exception upon

Accessors

Global state.

A lexer for terms.

Multi-precision arithmetic using the gmp library.

cons(car(x), cdr(x)) reduces to x.

Equalities and disequalities over variables and constraints on variables

Symbols.

Redirecting output.

Translations to/from ICSAT propositions

Mapping a term transformer f over a.

Constructors

Fold over the find structure.

Fold over the find structure.

Function symbols for the theory of S-expressions.

Some recognizers.

Classification of function symbols.

Functions to run at exit

empty use list.

remove the inverse of x.

Sets and maps of terms