CVC3
2.4.1
|
Files | |
file | assumptions.h [code] |
file | cdflags.h [code] |
Context Dependent Vector of Flags. | |
file | cdlist.h [code] |
file | cdmap.h [code] |
file | cdmap_ordered.h [code] |
file | cdo.h [code] |
file | circuit.h [code] |
Circuit class. | |
file | clause.h [code] |
file | cnf.h [code] |
Basic classes for reasoning about formulas in CNF. | |
file | cnf_manager.h [code] |
Manager for conversion to and traversal of CNF formulas. | |
file | command_line_exception.h [code] |
file | command_line_flags.h [code] |
file | common_proof_rules.h [code] |
file | compat_hash_map.h [code] |
file | compat_hash_set.h [code] |
file | context.h [code] |
file | cvc_util.h [code] |
basic helper utilities | |
file | debug.h [code] |
Description: Collection of debugging macros and functions. | |
file | dpllt.h [code] |
Generic DPLL(T) module. | |
file | dpllt_basic.h [code] |
Basic implementation of dpllt module. | |
file | dpllt_minisat.h [code] |
Implementation of dpllt module based on minisat. | |
file | eval_exception.h [code] |
file | exception.h [code] |
file | expr.h [code] |
Definition of the API to expression package. See class Expr for details. | |
file | expr_hash.h [code] |
Definition of the API to expression package. See class Expr for details. | |
file | expr_manager.h [code] |
Expression manager API. | |
file | expr_map.h [code] |
file | expr_op.h [code] |
Class Op representing the Expr's operator. | |
file | expr_stream.h [code] |
file | expr_transform.h [code] |
Generally Useful Expression Transformations. | |
file | expr_value.h [code] |
file | fdstream.h [code] |
The following code declares classes to read from and write to file descriptore or file handles. | |
file | formula_value.h [code] |
enumerated type for value of formulas | |
file | hash_fun.h [code] |
hash functions | |
file | hash_map.h [code] |
hash map implementation | |
file | hash_set.h [code] |
hash map implementation | |
file | hash_table.h [code] |
hash table implementation | |
file | kinds.h [code] |
file | lang.h [code] |
Definition of input and output languages to CVC3. | |
file | memory_manager.h [code] |
file | memory_manager_chunks.h [code] |
file | memory_manager_context.h [code] |
Stack-based memory manager. | |
file | memory_manager_malloc.h [code] |
file | notifylist.h [code] |
file | os.h [code] |
Abstraction over different operating systems. | |
file | parser.h [code] |
file | parser_exception.h [code] |
An exception thrown by the parser. | |
file | pretty_printer.h [code] |
file | proof.h [code] |
file | queryresult.h [code] |
enumerated type for result of queries | |
file | rational.h [code] |
file | sat_api.h [code] |
file | search.h [code] |
Abstract API to the proof search engine. | |
file | search_fast.h [code] |
file | search_impl_base.h [code] |
Abstract API to the proof search engine. | |
file | search_sat.h [code] |
Search engine that uses an external SAT engine. | |
file | search_simple.h [code] |
file | smartcdo.h [code] |
Smart context-dependent object wrapper. | |
file | smtlib_exception.h [code] |
An exception to be thrown by the smtlib translator. | |
file | sound_exception.h [code] |
An exception to be thrown when unsoundness is detected in a proof rule. | |
file | statistics.h [code] |
Description: Counters and flags for collecting run-time statistics. | |
file | theorem.h [code] |
file | theorem_manager.h [code] |
file | theorem_producer.h [code] |
file | theory.h [code] |
Generic API for Theories plus methods commonly used by theories. | |
file | theory_arith.h [code] |
file | theory_arith3.h [code] |
file | theory_arith_new.h [code] |
file | theory_arith_old.h [code] |
file | theory_array.h [code] |
file | theory_bitvector.h [code] |
file | theory_core.h [code] |
file | theory_datatype.h [code] |
file | theory_datatype_lazy.h [code] |
file | theory_quant.h [code] |
file | theory_records.h [code] |
file | theory_simulate.h [code] |
Implementation of a symbolic simulator. | |
file | theory_uf.h [code] |
file | translator.h [code] |
An exception to be thrown by the smtlib translator. | |
file | type.h [code] |
file | typecheck_exception.h [code] |
An exception to be thrown at typecheck error. | |
file | variable.h [code] |
file | vc.h [code] |
Generic API for a validity checker. | |
file | vc_cmd.h [code] |
file | vcl.h [code] |
Main implementation of ValidityChecker for CVC3. | |