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-22	TPTP: add parser for cnf and fof	François Bobot
	- include directive works - no keyword : 'fof', 'cnf', ... can be used for symbols name - real -> unsorted -> real (for the one that appear, so no bijection bitween real and unsorted) - same thing for string But: - string not distinct by projection to real, not sure if the current state of string theory make them distinct - filtering in include is not done - the result is not printed in the TPTP way (currently SMT2 way)
2012-06-17	enabling theoryof=term for quantifiers with sharing	Dejan Jovanović
	disableing one test case in equantifiers/decision that runs long
2012-06-17	fixing wrong assertion	Dejan Jovanović

2012-06-17	fixing makefile error that brakes build	Dejan Jovanović

2012-06-17	Fix array bug causing incorrect answers	Clark Barrett

2012-06-16	Adding the failing QF_AUFLIA regression mentioned in last commit.	Kshitij Bansal
	pp-regfile.delta02.smt is the one to look at with --decision=justificaiton, the delta minimized version of pp-regfile, which also gives wrong answer. due to various commits/fixes, delta01 gives correct answer currently.
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-15	one bug fixed	Kshitij Bansal

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	add failing regression, move error up	Kshitij Bansal

2012-06-14	bug fixes in justification heuristic	Kshitij Bansal
	* remove assert iteSkolemMap gives ite-s (not true with repeatSimp) * handle a corner case in findSplitter triggered by repeatSimp
2012-06-14	enabling fixed bug345 case	Dejan Jovanović

2012-06-14	fixes for the hasTerm issues in the shared database under the decision heuristic	Dejan Jovanović

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	* 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ć