Array_util 
Utility functions for arrays.

Bihashtbl 
Partial bijective hash tables.

Bunch 
Collection of elements with fast union.

Cc 
Termlevel API for
Cc_core .

Cc_core 
Congruenceclosure solver for EUF.

Cc_literal 
Literal representation for Congruence Closure.

Constant 
Constants.

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.

Equality_propagation 
Preprocessing by equality propagation.

Function 
Common functions and combinators.

Id 
Abstract unique identifiers and an implementation with natural numbers.

Index 
Fast data structures using natural number indexing.

Ite_removal 
Rewrite ITEs.

List_util 
Utility functions for lists.

Log 
Message logging.

Option 
Functions for the Option type.

Priority_queue 
Priority queue of unique integer elements.

Rational_num 
Recognize rationals.

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.

Subarray 
Functions for manipulating array subranges.

Symbol 
Symbols.

Term 
The structure of terms.

Term_constant 
Predefined Constants.

Term_literal 
Term literals.

Term_logic 
Term constructors.

Ternary 
Three valued booleans.

Time 
Elapsed user processor time points.

Union_find 
Unionfind data structure.

Util 
Utility modules and functions.

Variable 
Variables.

Vec 
Dynamically resizable arrays.
