A  
Array_util 
Utility functions for arrays.

B  
Big_int_solver [Dl]  
Big_integers [Dl_number]  
Bihashtbl 
Partial bijective hash tables.

Bunch 
Collection of elements with fast union.

C  
Cc 
Termlevel API for
Cc_core .

Cc_core 
Congruenceclosure solver for EUF.

Cc_literal 
Literal representation for Congruence Closure.

Constant 
Constants.

D  
Dl 
A termlevel API for
Dl_core

Dl_core 
A solver for difference logic.

Dl_number 
Representation of numbers for Difference Logic.

Dpll 
A termlevel DPLL solver.

Dpll_core 
State and actions of a MiniSat like DPLL solver.

Dpll_literal 
Literals and variables.

E  
Equality_propagation 
Preprocessing by equality propagation.

F  
Floats [Dl_number]  
Function 
Common functions and combinators.

H  
Hashed_list [List_util]  
I  
Id 
Abstract unique identifiers and an implementation with natural numbers.

Index 
Fast data structures using natural number indexing.

Integer [Util] 
Integers in a form suitable for use with
Map and Hashtbl .

Ite_removal 
Rewrite ITEs.

L  
List_util 
Utility functions for lists.

Literal [Dpll_literal] 
Literals are unique identifiers.

Literal [Dl_core.T] 
Literals.

Literal_map [Dpll_literal] 
Maps keyed off literals.

Literal_set [Dpll_literal] 
Sets of literals.

Log 
Message logging.

M  
Make [Union_find] 
Functor building a unionfind data structure.

Make [Dl_core]  
Make [Bihashtbl] 
Functor building an implementation of the partial bijective hash
table structure.

Make_hashed_set [Index] 
Functor building an implementation of sets over hashable elements.

Make_map [Index] 
Functor building an implementation of maps overs indices.

Make_map2 [Index] 
A two argument map where the first key is an indexed type and the
second is a hashed type.

Make_priority_queue [Index] 
Functor building an implementation of priority queues for indexed types.

Make_set [Index] 
Functor building an implementation of sets over indices.

N  
Nat [Id] 
Natural numbers as identifiers.

Nat_generator [Id] 
Generators for identifiers in an initial region of the naturals.

Nat_map [Index] 
A map for natural numbers.

Nat_map2 [Index] 
A two argument map where the first key is a natural number and the
second is a hashed type.

Nat_priority_queue [Index] 
An implementation of priority queue with natural number elements.

Nat_set [Index] 
A set implementation for natural numbers.

O  
Option 
Functions for the Option type.

P  
Primitive [Symbol]  
Priority_queue 
Priority queue of unique integer elements.

R  
Rational_num 
Recognize rationals.

Rational_solver [Dl]  
Rationals [Dl_number]  
Rbc [Term_logic] 
Logical constructors with syntactic simplification based on
Reduced Boolean Circuits.

Rbc_rewriter [Term_logic] 
A term rewriter based on Reduced Boolean Circuits.

S  
Safe_int_solver [Dl]  
Safe_integers [Dl_number]  
Small_integers [Dl_number]  
Smtlib_attribute 
SMTLIB benchmark, logic and theory attributes.

Smtlib_lexer 
Lexical analysis for SMTLIB theory, logic, and benchmark files.

Smtlib_parser 
Combined SMTLIB file parser interface.

Smtlib_syntax 
Compound syntactic constructs occurring in SMTLIB terms and formulas.

Solver_api 
Term level interface specifications.

Solver_dpll 
DPLLbased SAT Solver

Solver_dpllt 
A DPLL(T) solver.

Solver_dtc 
Delayed Theory Combination based solver.

Standard [Term_logic] 
Logical constructors with no syntactic simplifications.

Stretch_solver [Dl]  
Stretched_integers [Dl_number]  
String [Util] 
Strings in a form suitable for use with
Map and Hashtbl .

Subarray 
Functions for manipulating array subranges.

Symbol 
Symbols.

T  
Term 
The structure of terms.

Term_compared [Term] 
Terms augmented with comparison functions.

Term_constant 
Predefined Constants.

Term_hashtbl [Term] 
Hash tables keyed off terms.

Term_literal 
Term literals.

Term_logic 
Term constructors.

Term_map [Term] 
Maps from terms.

Term_mutable_set [Term] 
Mutable sets of terms.

Term_set [Term] 
Sets of terms.

Term_union_find [Term] 
Unionfind over terms.

Ternary 
Three valued booleans.

Time 
Elapsed user processor time points.

U  
Union_find 
Unionfind data structure.

Util 
Utility modules and functions.

V  
Variable 
Variables.

Variable [Dpll_literal] 
Variables are represented by unique identifiers.

Variable [Dl_core]  
Variable [Cc_literal] 
Variables are represented by unique identifiers.

Variable_hash [Cc_literal]  
Variable_hashtbl [Variable] 
Hash tables from variables.

Variable_map [Variable] 
Maps from variables.

Variable_map [Dpll_literal] 
Maps keyed off variables.

Variable_map [Dl_core]  
Variable_map [Cc_literal]  
Variable_map2 [Cc_literal]  
Variable_queue [Dpll_literal] 
Priorities queues of variables.

Variable_set [Variable] 
Sets of variables.

Variable_set [Dpll_literal] 
Sets of variables.

Variable_set [Cc_literal]  
Vec 
Dynamically resizable arrays.
