| Array_util |
Utility functions for arrays.
|
| Bihashtbl |
Partial bijective hash tables.
|
| Bunch |
Collection of elements with fast union.
|
| Cc |
Term-level API for
Cc_core.
|
| Cc_core |
Congruence-closure solver for EUF.
|
| Cc_literal |
Literal representation for Congruence Closure.
|
| Constant |
Constants.
|
| 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.
|
| Equality_propagation |
Pre-processing 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 |
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.
|
| 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 |
Union-find data structure.
|
| Util |
Utility modules and functions.
|
| Variable |
Variables.
|
| Vec |
Dynamically resizable arrays.
|