CVC3  2.4.1
include Directory Reference

Files

file  assumptions.h [code]
file  cdflags.h [code]
 Context Dependent Vector of Flags.
file  cdlist.h [code]
file  cdmap.h [code]
file  cdmap_ordered.h [code]
file  cdo.h [code]
file  circuit.h [code]
 Circuit class.
file  clause.h [code]
file  cnf.h [code]
 Basic classes for reasoning about formulas in CNF.
file  cnf_manager.h [code]
 Manager for conversion to and traversal of CNF formulas.
file  command_line_exception.h [code]
file  command_line_flags.h [code]
file  common_proof_rules.h [code]
file  compat_hash_map.h [code]
file  compat_hash_set.h [code]
file  context.h [code]
file  cvc_util.h [code]
 basic helper utilities
file  debug.h [code]
 Description: Collection of debugging macros and functions.
file  dpllt.h [code]
 Generic DPLL(T) module.
file  dpllt_basic.h [code]
 Basic implementation of dpllt module.
file  dpllt_minisat.h [code]
 Implementation of dpllt module based on minisat.
file  eval_exception.h [code]
file  exception.h [code]
file  expr.h [code]
 Definition of the API to expression package. See class Expr for details.
file  expr_hash.h [code]
 Definition of the API to expression package. See class Expr for details.
file  expr_manager.h [code]
 Expression manager API.
file  expr_map.h [code]
file  expr_op.h [code]
 Class Op representing the Expr's operator.
file  expr_stream.h [code]
file  expr_transform.h [code]
 Generally Useful Expression Transformations.
file  expr_value.h [code]
file  fdstream.h [code]
 The following code declares classes to read from and write to file descriptore or file handles.
file  formula_value.h [code]
 enumerated type for value of formulas
file  hash_fun.h [code]
 hash functions
file  hash_map.h [code]
 hash map implementation
file  hash_set.h [code]
 hash map implementation
file  hash_table.h [code]
 hash table implementation
file  kinds.h [code]
file  lang.h [code]
 Definition of input and output languages to CVC3.
file  memory_manager.h [code]
file  memory_manager_chunks.h [code]
file  memory_manager_context.h [code]
 Stack-based memory manager.
file  memory_manager_malloc.h [code]
file  notifylist.h [code]
file  os.h [code]
 Abstraction over different operating systems.
file  parser.h [code]
file  parser_exception.h [code]
 An exception thrown by the parser.
file  pretty_printer.h [code]
file  proof.h [code]
file  queryresult.h [code]
 enumerated type for result of queries
file  rational.h [code]
file  sat_api.h [code]
file  search.h [code]
 Abstract API to the proof search engine.
file  search_fast.h [code]
file  search_impl_base.h [code]
 Abstract API to the proof search engine.
file  search_sat.h [code]
 Search engine that uses an external SAT engine.
file  search_simple.h [code]
file  smartcdo.h [code]
 Smart context-dependent object wrapper.
file  smtlib_exception.h [code]
 An exception to be thrown by the smtlib translator.
file  sound_exception.h [code]
 An exception to be thrown when unsoundness is detected in a proof rule.
file  statistics.h [code]
 Description: Counters and flags for collecting run-time statistics.
file  theorem.h [code]
file  theorem_manager.h [code]
file  theorem_producer.h [code]
file  theory.h [code]
 Generic API for Theories plus methods commonly used by theories.
file  theory_arith.h [code]
file  theory_arith3.h [code]
file  theory_arith_new.h [code]
file  theory_arith_old.h [code]
file  theory_array.h [code]
file  theory_bitvector.h [code]
file  theory_core.h [code]
file  theory_datatype.h [code]
file  theory_datatype_lazy.h [code]
file  theory_quant.h [code]
file  theory_records.h [code]
file  theory_simulate.h [code]
 Implementation of a symbolic simulator.
file  theory_uf.h [code]
file  translator.h [code]
 An exception to be thrown by the smtlib translator.
file  type.h [code]
file  typecheck_exception.h [code]
 An exception to be thrown at typecheck error.
file  variable.h [code]
file  vc.h [code]
 Generic API for a validity checker.
file  vc_cmd.h [code]
file  vcl.h [code]
 Main implementation of ValidityChecker for CVC3.