cvc5.git - CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

Age	Commit message (Collapse)	Author
2010-09-14	ensure uf/congruence closure debugging stuff isn't called in production builds	Morgan Deters

2010-08-19	UF theory bug fixes, code cleanup, and extra debugging output.	Morgan Deters
	Enabled new UF theory by default. Added some UF regressions. Some work on the whole equality-over-bool-removed-in-favor-of-IFF thing. (Congruence closure module and other things have to handle IFF as a special case of equality, etc..) Added pre-rewriting to TheoryBool which rewrites: * (IFF true x) => x * (IFF false x) => (NOT x) * (IFF x true) => x * (IFF x false) => (NOT x) * (IFF x x) => true * (IFF x (NOT x)) => false * (IFF (NOT x) x) => false * (ITE true x y) => x * (ITE false x y) => y * (ITE cond x x) => x Added post-rewriting that does all of the above, plus normalize IFF and ITE: * (IFF x y) => (IFF y x), if y < x * (ITE (NOT cond) x y) => (ITE cond y x) (Note: ITEs survive the removal-of-ITEs pass only if they are Boolean-valued.) A little more debugging output from CNF stream, context pushes/pops, ITE removal. Some more documentation. Fixed some typos.
2010-08-17	Merge from "cc" branch:	Morgan Deters
	CongruenceClosure implementation; CongruenceClosure white-box test. New UF theory implementation based on new CC module. This one supports predicates. The two UF implementations exist in parallel (they can be selected at runtime via the new command line option "--uf"). Added type infrastructure for TUPLE. Fixes to unit tests that failed in 16-August-2010 regressions. Needed to instantiate TheoryEngine with an Options structure, and explicitly call ->shutdown() on it before destruction (like the SMTEngine does). Fixed test makefiles to (1) perform all tests even in the presence of failures, (2) give proper summaries of subdirectory tests (e.g. regress0/uf and regress0/precedence) Other minor changes.
2010-06-30	add documentation for additional clarity, re-add addTerm()	Morgan Deters

2010-06-30	checking in CC module interface for reference.	Morgan Deters