include Directory Reference

Directory dependency graph for include:

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.