include Directory Reference

Files

• file assumptions.h [code]
• file assumptions_value.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]
• 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 cvclutil.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 based on xchaff.
  

• 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]
• 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]
• file kinds.h [code]
• file lang.h [code]

  Definition of input and output languages to CVCL.
  

• file memory_manager.h [code]
• file memory_manager_chunks.h [code]
• file memory_manager_malloc.h [code]
• file notifylist.h [code]
• 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 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]
• 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_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 CVC lite.
  

---