include Directory Reference

Files

• file assumptions.h
• file assumptions_value.h
• file cdlist.h
• file cdmap.h
• file cdmap_ordered.h
• file cdo.h
• file circuit.h
• file clause.h
• file command_line_exception.h
• file command_line_flags.h
• file common_proof_rules.h
• file compat_hash_map.h
• file compat_hash_set.h
• file context.h
• file debug.h

  Description: Collection of debugging macros and functions.
  

• file eval_exception.h
• file exception.h
• file expr.h

  Definition of the API to expression package. See class Expr for details.
  

• file expr_hash.h
• file expr_manager.h

  Expression manager API.
  

• file expr_map.h
• file expr_op.h

  Class Op representing the Expr's operator.
  

• file expr_stream.h
• file expr_value.h
• file fdstream.h
• file kinds.h
• file lang.h

  Definition of input and output languages to CVCL.
  

• file memory_manager.h
• file memory_manager_chunks.h
• file memory_manager_malloc.h
• file notifylist.h
• file parser.h
• file parser_exception.h

  An exception thrown by the parser.
  

• file pretty_printer.h
• file proof.h
• file rational.h
• file search.h

  Abstract API to the proof search engine.
  

• file search_fast.h
• file search_simple.h
• file smartcdo.h

  Smart context-dependent object wrapper.
  

• file smtlib_exception.h

  An exception to be thrown by the smtlib translator.
  

• file sound_exception.h

  An exception to be thrown when unsoundness is detected in a proof rule.
  

• file statistics.h

  Description: Counters and flags for collecting run-time statistics.
  

• file theorem.h
• file theorem_manager.h
• file theorem_producer.h
• file theory.h

  Generic API for Theories plus methods commonly used by theories.
  

• file theory_arith.h
• file theory_array.h
• file theory_bitvector.h
• file theory_core.h
• file theory_datatype.h
• file theory_quant.h
• file theory_records.h
• file theory_simulate.h

  Implementation of a symbolic simulator.
  

• file theory_uf.h
• file type.h
• file typecheck_exception.h

  An exception to be thrown at typecheck error.
  

• file variable.h
• file vc.h

  Generic API for a validity checker.
  

• file vc_cmd.h
• file vcl.h

  Main implementation of ValidityChecker for CVC lite.
  

---