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

Age	Commit message (Collapse)	Author
2012-06-14	New substitutions implementation - fixes performance issue seen in nonclausal	Clark Barrett
	simplification for some benchmarks
2012-06-14	Fixed arithmetic consistency issue. The simplex conflict variable had to be ↵	Tim King
	reenqueued so that the queue was a superset of the failing assertions. This adds a super expensive debug routine unenqueuedVariablesAreConsistent() that catches this bug. This is enabled when -d arith::consistency is turned on. make check passes with this flag enabled.
2012-06-14	fix for clark's bug	Dejan Jovanović
	imporant: theories SHOULD NOT use getSatValue at all, otherwise they might create a conflict with a literal they didn't get()
2012-06-14	fix quantifier non-bug	Kshitij Bansal

2012-06-14	Removed an assertion, unneeded header file	Clark Barrett

2012-06-14	The "no-tears-in-competition-mode" commit. Change all (non-driver, ↵	Morgan Deters
	non-SAT-solver) uses of std::cout to the Message stream, and all uses of std::cerr to the Warning stream.
2012-06-14	fix cout, fix statname, rm deadcode	Kshitij Bansal

2012-06-14	changing to a more natural propagation order in uf, seems to pay off	Dejan Jovanović

2012-06-14	some changes to the uf engine	Dejan Jovanović
	* dramatically less terms to manage by doing reflexivity semantically * fixes the problem clark had with not detecting inconsistencies with shared terms i'm not sure what's the performance impact, but this is so much better and we'll deal with performance later
2012-06-14	Brings the tuning branch into trunk. This includes the changes from ↵	Tim King
	restricted-simplex.
2012-06-14	* removing rewriteEquality from the rewriter	Dejan Jovanović
	* theories now get either an assertion from the SAT solver (normalized) or an (dis-)equality between two shared terms that is non-normalized
2012-06-13	Added witnesses to Constraints.	Tim King

2012-06-13	- Added a loop to internally assert constraints that are marked as true.	Tim King
	- Changes how CongruenceManager reports conflicts. - ConstraintDatabase can now detect and raise conflicts when doing unate propagation.
2012-06-13	Adds debugging output to theory_engine.cpp.	Tim King

2012-06-13	fix for bug 354	Dejan Jovanović

2012-06-13	Fixed failing assertion when EqualityEngine is in conflict	Clark Barrett

2012-06-13	Fixed definition of bvsmod	Clark Barrett

2012-06-13	Fixes more problems in bv rewrites	Clark Barrett

2012-06-13	Fixes lots of problems in bv rewrite rules and adds lots of assertions	Clark Barrett
	to catch any that I may have missed
2012-06-12	Fix some compile warnings (but they never showed up on church)	Morgan Deters

2012-06-12	Fixed fuzzing bug	Clark Barrett

2012-06-12	Fix to yesterday's change in arithmetic.	Tim King

2012-06-12	bufixes and the bugs	Dejan Jovanović
	* array now only propagates thropugh the equality engine * assertions in the equality rewriting to ensure eq -> { eq, T, F }
2012-06-12	conflicts from theories are removable	Dejan Jovanović

2012-06-12	Changed bitvector theory rewriter so that equalities always get rewritten to	Clark Barrett
	equalities or true or false
2012-06-12	Fixed bug causing QF_LIA/solver_cvc4/incorrect1.smt and ↵	Clark Barrett
	QF_LIA/solver_cvc4/incorrect3.smt
2012-06-12	Fixed failing assertion in arrays for bug 347	Clark Barrett

2012-06-12	minor cleanup, and replace a "private:" in equality engine that had been ↵	Morgan Deters
	removed by the quantifiers merge (I had reengineered some things from quantifiers so that the equality engine didn't have to expose internals as public, but then had neglected to re-privatize them)
2012-06-12	Adding constant propagation code - needs more testing - off by default	Clark Barrett

2012-06-11	Fix to term normalization of integer equalities. Adds a regression test that ↵	Tim King
	triggered it.
2012-06-11	Fixing type comparision assertion in getEqualityStatus().	Tim King

2012-06-11	fixing bitvector bugs	Dejan Jovanović
	* clauses shouldn't be erased when they could be a reason for outside propagation * propagation of p and !p is ignored as this must lead to a conflict in the subtheory internally
2012-06-11	mark a quantifiers global var as "static" so we can find it easier later	Morgan Deters

2012-06-11	OK, now the rewrite issues are fixed	Clark Barrett

2012-06-11	Merge from quantifiers2-trunkmerge branch.	Morgan Deters
	Adds TheoryQuantifiers and TheoryRewriteRules, QuantifiersEngine, and other infrastructure. Adds theory instantiators to many theories. Adds the UF strong solver.
2012-06-11	Fix for array bug with decision heuristic	Clark Barrett
	Also fixed one bv rewrite failure (more to come)
2012-06-11	Fixed bug 352	Clark Barrett

2012-06-10	Fixed one more bug in rewriter	Clark Barrett

2012-06-10	Added a very fruitful assertion to the rewriter: checks that rewriting after ↵	Clark Barrett
	"REWRITE_DONE" is idempotent Found several problems where this is not the case and fixed them
2012-06-10	adding an assertion to trigger the problem of bug349 and the testcase	Dejan Jovanović
	bv rewriter apparently deosn't have a proper normal form for equalities
2012-06-10	fixes for bug347	Dejan Jovanović
	it was an issue with constants being merged, which influenced explanations of disequalities. when constants are attempted to be merged, equality engine now enters conflict mode immediately
2012-06-09	Dagification of output expressions.	Morgan Deters
	By default, common subexpressions are dagified if they appear > 1 time and are not constants or variables. This can be changed with --default-expr-dag=N --- N is a threshold such that if the subexpression occurs > N times, it is dagified; a setting of 0 turns off dagification entirely. If you notice strange dumping behavior (taking too long to print anything, e.g.), revert to the old behavior with --default-expr-dag=0 and let me know of the problem.
2012-06-07	fixing the wrong results. arrays equality adaptor had a missing case when ↵	Dejan Jovanović
	propagating disequalities between shared terms.
2012-06-07	LogicInfo locking implemented, and some initialization-order issues in ↵	Morgan Deters
	SmtEngine resolved. ALL_SUPPORTED and QF_ALL_SUPPORTED logics now supported by SMT-LIB parsers. In SMT-LIBv2, if a (set-logic..) command is missing, ALL_SUPPORTED is assumed, and a warning is issued, as discussed on the cvc4-devel mailing list.
2012-06-07	Fixed performance issue with ite_simplifier on some QF_AUFBV benchmarks	Clark Barrett

2012-06-07	fixing some bugs in propagation of disequalities	Dejan Jovanović
	still doesnt fix the wrong answers thought :(
2012-06-06	Fixed assertion failures	Clark Barrett

2012-06-06	disabling a super-expensive assertions to speed up debug runs	Dejan Jovanović

2012-06-06	Changes to the combination mechanism, lots of details. Not done yet, there ↵	Dejan Jovanović
	are still the AUFBV wrong results, but it seems better. http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=4382&reference_id=4359&p=5
2012-06-06	Fixed problem causing crash at destruction time	Clark Barrett