modified by

Multi-precision arithmetic using the gmp library.

Functions to run at exit

Redirecting output.

Exceptions that are used throughout ICS.

Union of two domains

Accessors

Sets and maps of terms

Function symbols for the theory of S-expressions.

Some recognizers.

Constructors

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.

Symbols

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

Fold iterator

Creating fresh bitvector variables for solver.

Constants

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)

Mapping a term transformer f over a.

evaluation, not affecting function bodies

Classification of function symbols.

Set of atoms

empty use list.

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

remove the inverse of x.

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

Equalities and disequalities over variables and constraints on variables

Fold over the find structure.

Fold over the find structure.

Decision procedure state

Translations to/from ICSAT propositions

Global state.

A lexer for terms.

raise Sys.Break exception upon