File List

Here is a list of all files with brief descriptions:

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