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

Age	Commit message (Collapse)	Author
2012-06-28	Fixed bug in bv rewriter that caused wrong answer in SMT-COMPsmtcomp2012-resubmission-2	Clark Barrett

2012-06-17	fixing wrong assertion	Dejan Jovanović

2012-06-16	changing theoryOf in shared mode with arrays to move equalities to arrays	Dejan Jovanović
	disabled in bitvectors due to non-stably infinite problems the option to enable it is --theoryof-mode=term
2012-06-15	Fixes some assertion failures	Clark Barrett

2012-06-14	fixing the problems with the bvminisat. there was a case when things would ↵	Dejan Jovanović
	get bitblasted, it would restart to add the clauses, and loose propagation information.
2012-06-14	fixes for the hasTerm issues in the shared database under the decision heuristic	Dejan Jovanović

2012-06-14	This commit:	Kshitij Bansal
	* enables decision heuristic (justification) for QF_BV and QF_AUFBV * disables a failing regression in aufbv (because of equality engine assert failure trigerred by above change) * moves around the init procedure smt_engine * destruction time issues because of moving this -- still to be fixed, currently get around by not destucting stuff in driver
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	enabling regressions from last night, all fixed	Dejan Jovanović

2012-06-13	r2.node == response.node failure	Dejan Jovanović

2012-06-12	missing problems	Dejan Jovanović

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	more breakage in aufbv	Dejan Jovanović
	Assertion `value(l) == (lbool((uint8_t)0))' failed. and d_disequalityReasonsMap.find(pair) != d_disequalityReasonsMap.end()
2012-06-12	tests for the	Dejan Jovanović
	!isEliminated(var(ps[i])) assert fails
2012-06-11	some failing examples	Dejan Jovanović

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-07	fixing the wrong results. arrays equality adaptor had a missing case when ↵	Dejan Jovanović
	propagating disequalities between shared terms.
2012-06-07	cleaning up the expample for the future	Dejan Jovanović

2012-06-07	Added small test case for diseq propagation	Clark Barrett

2012-06-07	fixing some bugs in propagation of disequalities	Dejan Jovanović
	still doesnt fix the wrong answers thought :(
2012-06-06	Fixing numerous issues with tests and "make dist":	Morgan Deters
	* test/regress/regress0/unconstrained wasn't being distributed. This caused the debian build failure last night. (It still doesn't run on "make check", but had to be distributed properly.) * Fixing an issue where a test name was longer than 99 characters and couldn't be distributed in the "old" tar format. (Told automake to use a newer tar format.)
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-05-17	Fixed bug 338:	Liana Hadarean
	- fixed buggy rewrite rules assuming certain nodes only had 2 children - added support for bv-rewrite dump - fixed smt2_printer for bv constants
2012-05-08	Merging in bvprop branch, with proper bit-vector propagation.	Liana Hadarean
	This should also fix bug 325.
2012-04-18	add the missing BINARY variable in some test/regress makefiles	Kshitij Bansal

2012-04-11	merge from arrays-clark branch	Morgan Deters