CVC3
2.4.1
|
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 |