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