File List

Here is a list of all files with brief descriptions:

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