CVC Lite 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
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]
assumptions_value.cpp [code]
assumptions_value.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
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.h [code]
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]
cvclutil.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.cpp [code]	Decision Engine
decision_engine_caching.h [code]
decision_engine_dfs.cpp [code]	Decision Engine
decision_engine_dfs.h [code]
decision_engine_mbtf.cpp [code]	Decision Engine
decision_engine_mbtf.h [code]
dictionary.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 based on xchaff
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]
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]
hash.h [code]
INSTALL [code]
kinds.h [code]
lang.h [code]	Definition of input and output languages to CVCL
LICENSE [code]
main.cpp [code]	Main program for CVC_lite
memory_manager.h [code]
memory_manager_chunks.h [code]
memory_manager_malloc.h [code]
notifylist.h [code]
parser.h [code]
parser_exception.h [code]	An exception thrown by the parser
parser_temp.h [code]
preprocess.cpp [code]
pretty_printer.h [code]
proof.h [code]
quant_proof_rules.h [code]
quant_theorem_producer.cpp [code]
quant_theorem_producer.h [code]
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]
refined_arith_theorem_producer.cpp [code]
refined_arith_theorem_producer.h [code]	TRUSTED implementation of arithmetic proof rules
sat_api.cpp [code]
sat_api.h [code]
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]
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_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_datatype2.cpp [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
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
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_api.cpp [code]
vc_api.h [code]
vc_cmd.cpp [code]
vc_cmd.h [code]
vcl.cpp [code]
vcl.h [code]	Main implementation of ValidityChecker for CVC lite
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]

---