CVC3  2.4.1
File List
Here is a list of all files with brief descriptions:
 arith_exception.hAn exception thrown by the arithmetic decision procedure
 arith_proof_rules.hArithmetic proof rules
 arith_theorem_producer.cpp
 arith_theorem_producer.hTRUSTED implementation of arithmetic proof rules
 arith_theorem_producer3.cpp
 arith_theorem_producer3.hTRUSTED implementation of arithmetic proof rules
 arith_theorem_producer_old.cpp
 arith_theorem_producer_old.hTRUSTED implementation of arithmetic proof rules
 array_proof_rules.h
 array_theorem_producer.cppDescription: TRUSTED implementation of array proof rules
 array_theorem_producer.h
 assumptions.cppImplementation of class Assumptions
 assumptions.h
 bitvector_exception.hAn exception thrown by the bitvector decision procedure
 bitvector_expr_value.hSubclasses of ExprValue for bit-vector expressions
 bitvector_proof_rules.hArithmetic proof rules
 bitvector_theorem_producer.cpp
 bitvector_theorem_producer.hTRUSTED implementation of bitvector proof rules
 bryant.cpp
 cdflags.cppImplementation for CDFlags class
 cdflags.hContext Dependent Vector of Flags
 cdlist.h
 cdmap.h
 cdmap_ordered.h
 cdo.h
 circuit.cppCircuit class
 circuit.hCircuit class
 clause.cppImplementation of class Clause
 clause.h
 cnf.cppImplementation of classes used for generic CNF formulas
 cnf.hBasic classes for reasoning about formulas in CNF
 cnf_manager.cppImplementation of CNF_Manager
 cnf_manager.hManager for conversion to and traversal of CNF formulas
 cnf_rules.hAbstract proof rules for CNF conversion
 cnf_theorem_producer.cppImplementation of CNF_TheoremProducer
 cnf_theorem_producer.hImplementation of CNF_Rules API
 command_line_exception.h
 command_line_flags.h
 common_proof_rules.h
 common_theorem_producer.cppImplementation of common proof rules
 common_theorem_producer.h
 compat_hash_map.h
 compat_hash_set.h
 context.cpp
 context.h
 core_proof_rules.hProof rules used by theory_core
 core_theorem_producer.cpp
 core_theorem_producer.h
 cvc_util.hBasic helper utilities
 datatype_proof_rules.hAbstract interface for recursive datatype proof rules
 datatype_theorem_producer.cppTRUSTED implementation of recursive datatype rules
 datatype_theorem_producer.hTRUSTED implementation of recursive datatype proof rules
 debug.cppDescription: Implementation of debugging facilities
 debug.hDescription: Collection of debugging macros and functions
 decision_engine.cppDecision Engine
 decision_engine.h
 decision_engine_caching.h
 decision_engine_dfs.cppDecision Engine
 decision_engine_dfs.h
 decision_engine_mbtf.h
 dpllt.hGeneric DPLL(T) module
 dpllt_basic.cppBasic implementation of dpllt module using generic sat solver
 dpllt_basic.hBasic implementation of dpllt module
 dpllt_minisat.cppImplementation of dpllt module using MiniSat
 dpllt_minisat.hImplementation of dpllt module based on minisat
 eval_exception.h
 exception.h
 expr.cpp
 expr.hDefinition of the API to expression package. See class Expr for details
 expr_hash.hDefinition of the API to expression package. See class Expr for details
 expr_manager.cpp
 expr_manager.hExpression manager API
 expr_map.h
 expr_op.cpp
 expr_op.hClass Op representing the Expr's operator
 expr_stream.cpp
 expr_stream.h
 expr_transform.cpp
 expr_transform.hGenerally Useful Expression Transformations
 expr_value.cpp
 expr_value.h
 fdstream.hThe following code declares classes to read from and write to file descriptore or file handles
 formula_value.hEnumerated type for value of formulas
 hash_fun.hHash functions
 hash_map.hHash map implementation
 hash_set.hHash map implementation
 hash_table.hHash table implementation
 INSTALL
 kinds.h
 lang.hDefinition of input and output languages to CVC3
 LFSCBoolProof.cpp
 LFSCBoolProof.h
 LFSCConvert.cpp
 LFSCConvert.h
 LFSCLraProof.cpp
 LFSCLraProof.h
 LFSCObject.cpp
 LFSCObject.h
 LFSCPrinter.cpp
 LFSCPrinter.h
 LFSCProof.cpp
 LFSCProof.h
 LFSCUtilProof.cpp
 LFSCUtilProof.h
 LICENSE
 main.cppMain program for cvc3
 memory_manager.h
 memory_manager_chunks.h
 memory_manager_context.hStack-based memory manager
 memory_manager_malloc.h
 minisat_derivation.cppMiniSat proof logging
 minisat_derivation.hMiniSat proof logging
 minisat_global.hMiniSat global functions
 minisat_heap.hMiniSat internal heap implementation
 minisat_solver.cppAdaptation of MiniSat to DPLL(T)
 minisat_solver.hAdaptation of MiniSat to DPLL(T)
 minisat_types.cppMiniSat internal types
 minisat_types.hMiniSat internal types
 minisat_varorder.hMiniSat decision heuristics
 notifylist.h
 Object.h
 os.hAbstraction over different operating systems
 parser.h
 parser_exception.hAn exception thrown by the parser
 parser_temp.h
 pretty_printer.h
 proof.h
 quant_proof_rules.h
 quant_theorem_producer.cpp
 quant_theorem_producer.h
 queryresult.hEnumerated type for result of queries
 rational-gmp.cppImplementation of class Rational using GMP library (C interface)
 rational-native.cppImplementation of class Rational using native (bounded precision) computer arithmetic
 rational.cpp
 rational.h
 README
 records_proof_rules.h
 records_theorem_producer.cpp
 records_theorem_producer.h
 sat_api.cpp
 sat_api.h
 sat_proof.hSat solver proof representation
 search.cpp
 search.hAbstract API to the proof search engine
 search_fast.cpp
 search_fast.h
 search_impl_base.cpp
 search_impl_base.hAbstract API to the proof search engine
 search_rules.hAbstract proof rules interface to the simple search engine
 search_sat.cppImplementation of Search engine with generic external sat solver
 search_sat.hSearch engine that uses an external SAT engine
 search_simple.cpp
 search_simple.h
 search_theorem_producer.cppImplementation of the proof rules for the simple search engine
 search_theorem_producer.hImplementation API to proof rules for the simple search engine
 simulate_proof_rules.hAbstract interface to the symbolic simulator proof rules
 simulate_theorem_producer.cppTrusted implementation of the proof rules for symbolic simulator
 simulate_theorem_producer.hImplementation of the symbolic simulator proof rules
 smartcdo.hSmart context-dependent object wrapper
 smtlib_exception.hAn exception to be thrown by the smtlib translator
 sound_exception.hAn exception to be thrown when unsoundness is detected in a proof rule
 statistics.cppDescription: Implementation of Statistics class
 statistics.hDescription: Counters and flags for collecting run-time statistics
 theorem.cpp
 theorem.h
 theorem_manager.cpp
 theorem_manager.h
 theorem_producer.cppSee theorem_producer.h file for more information
 theorem_producer.h
 theorem_value.h
 theory.cpp
 theory.hGeneric API for Theories plus methods commonly used by theories
 theory_arith.cpp
 theory_arith.h
 theory_arith3.cpp
 theory_arith3.h
 theory_arith_new.cpp
 theory_arith_new.h
 theory_arith_old.cpp
 theory_arith_old.h
 theory_array.cpp
 theory_array.h
 theory_bitvector.cpp
 theory_bitvector.h
 theory_core.cpp
 theory_core.h
 theory_datatype.cpp
 theory_datatype.h
 theory_datatype_lazy.cpp
 theory_datatype_lazy.h
 theory_quant.cpp
 theory_quant.h
 theory_records.cpp
 theory_records.h
 theory_simulate.cppImplementation of class TheorySimulate
 theory_simulate.hImplementation of a symbolic simulator
 theory_uf.cpp
 theory_uf.h
 translator.cppDescription: Code for translation between languages
 translator.hAn exception to be thrown by the smtlib translator
 TReturn.cpp
 TReturn.h
 type.h
 typecheck_exception.hAn exception to be thrown at typecheck error
 uf_proof_rules.hAbstract interface for uninterpreted function/predicate proof rules
 uf_theorem_producer.cppTRUSTED implementation of uninterpreted function/predicate rules
 uf_theorem_producer.hTRUSTED implementation of uninterpreted function/predicate proof rules
 Util.cpp
 Util.h
 variable.cppImplementation of class Variable; see variable.h for detail
 variable.h
 vc.hGeneric API for a validity checker
 vc_cmd.cpp
 vc_cmd.h
 vcl.cpp
 vcl.hMain implementation of ValidityChecker for CVC3
 xchaff.cpp
 xchaff.h
 xchaff_base.h
 xchaff_dbase.cpp
 xchaff_dbase.h
 xchaff_solver.cpp
 xchaff_solver.h
 xchaff_utils.cpp
 xchaff_utils.h