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	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	don't run rewriterules regressions by default; fixes needed	Morgan Deters

2012-06-14	fix quantifier non-bug	Kshitij Bansal

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	failing quantifier	Kshitij Bansal

2012-06-14	add passing regression	Kshitij Bansal

2012-06-14	bug 346 resolved	Morgan Deters

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	removing bug233 until morgan commits the actual file	Dejan Jovanović

2012-06-13	adding some regressions to the usual regressions runs; several ↵	Morgan Deters
	recently-fixed incremental bugs are closed
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	add passing regression	Kshitij Bansal

2012-06-13	enabling regressions from last night, all fixed	Dejan Jovanović

2012-06-13	enable some decision regressions	Kshitij Bansal

2012-06-13	decision regressions, all but one fail	Kshitij Bansal

2012-06-13	!(*child_it).isConst() assertion fail	Dejan Jovanović
	this is delta minimal with the same assertion
2012-06-13	r2.node == response.node failure	Dejan Jovanović

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

2012-06-13	!current[0].isConst() failure	Dejan Jovanović

2012-06-13	benchmark to show that we don't rewrite bvsmod correctly	Dejan Jovanović
	the definition in smtlib was buggy and was changed on 2011-06-15 check http://goedel.cs.uiowa.edu/smtlib/logics/QF_BV.smt2
2012-06-12	Fix to SMT-LIBv1 parser: QF_UF declares sort "U", but other UF logics do ↵	Morgan Deters
	not (e.g. QF_UFLIA). Also fix a syntax error in a regression test (CVC4 is too lenient to catch it though---CVC3 tripped over it). Also add additional parts for "make submission" in the top-level makefile
2012-06-12	missing problems	Dejan Jovanović

2012-06-12	wrong answer for bv	Dejan Jovanović

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

2012-06-12	bv reduced with decision: sat instead of unsat	Kshitij Bansal

2012-06-12	Assert fail equaility_engine.cpp: hasTerm(node) with --decision=justification	Kshitij Bansal

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	wrong answer benchmarks	Dejan Jovanović
	these should be simple constant propagation problems
2012-06-12	wrong result benchmark	Dejan Jovanović

2012-06-12	tests for the	Dejan Jovanović
	!isEliminated(var(ps[i])) assert fails
2012-06-12	test cases for the	Dejan Jovanović
	d_disequalityReasonsMap.find(pair) != d_disequalityReasonsMap.end() assertion fail
2012-06-12	Adding incorrect qf_lia result.	Tim King

2012-06-11	Fix to term normalization of integer equalities. Adds a regression test that ↵	Tim King
	triggered it.
2012-06-11	another benchmark that used to fail	Dejan Jovanović

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	distribute an .expect file. fixes a "make check" failure not for svn ↵	Morgan Deters
	working dirs but for distributed tarballs.
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	failing bv examples	Dejan Jovanović

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-09	Cleanup and comments for the dag-ifier. Also some unit testing for it.	Morgan Deters

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-08	very small fast example for the bv fail	Dejan Jovanović

2012-06-08	Merge from decision branch (till r3663)	Kshitij Bansal
	(no performace or search behavior changes expected)
2012-06-08	small fuzz examples where bv fails	Dejan Jovanović

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.