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 |
Term-level API for
Cc_core.
|
| Cc_core |
Congruence-closure solver for EUF.
|
| Cc_literal |
Literal representation for Congruence Closure.
|
| Constant |
Constants.
|
D | |
| Dl |
A term-level API for
Dl_core
|
| Dl_core |
A solver for difference logic.
|
| Dl_number |
Representation of numbers for Difference Logic.
|
| Dpll |
A term-level DPLL solver.
|
| Dpll_core |
State and actions of a MiniSat like DPLL solver.
|
| Dpll_literal |
Literals and variables.
|
E | |
| Equality_propagation |
Pre-processing 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 union-find 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 |
SMT-LIB benchmark, logic and theory attributes.
|
| Smtlib_lexer |
Lexical analysis for SMT-LIB theory, logic, and benchmark files.
|
| Smtlib_parser |
Combined SMT-LIB file parser interface.
|
| Smtlib_syntax |
Compound syntactic constructs occurring in SMT-LIB terms and formulas.
|
| Solver_api |
Term level interface specifications.
|
| Solver_dpll |
DPLL-based 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] |
Union-find over terms.
|
| Ternary |
Three valued booleans.
|
| Time |
Elapsed user processor time points.
|
U | |
| Union_find |
Union-find 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.
|