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-28	fix a link error on church, due to Antlr #defining "true" and "false" :-( ↵smtcomp2012-resubmission	Morgan Deters
	--for now, just #undef them after the #include
2012-06-27	Fixing a bug in proof production for the DioSolver.	Tim King

2012-06-27	This adds TheoryArith::safeToReset(). This fixes bug 363.	Tim King

2012-06-27	Adding access to simplex's ArithPriorityQueue to TheoryArith for ↵	Tim King
	ArithPriorityQueue::reduce(), ::begin() and ::end().
2012-06-27	Improved debugging output.	Tim King

2012-06-27	Improved debugging output.	Tim King

2012-06-27	Adding reduce() to the ArithPriorityQueue. This reduces the queue from a ↵	Tim King
	superset of the basic variables that violate a bound to the exact set.
2012-06-25	Added a warning to arithmetic for a known dio solver bug. Somehow the fix ↵	Tim King
	never made it to trunk. Do not know how. The fix to the bug is pending the hunt for bug 363.
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-22	parser: add some acces function and recover the original nextToken from antlr3	François Bobot
	in order to be able to use the stack of streams.
2012-06-22	fix : function AntlrInput::tokenTextSubstr	François Bobot

2012-06-22	Parser: add the possibility to bind at level 0.	François Bobot

2012-06-18	qf_lra strategysmtcomp2012	Morgan Deters

2012-06-18	Reverting buggy rewriter code	Clark Barrett

2012-06-18	another qf_lra strategy update	Morgan Deters

2012-06-18	Fixed bug in rewriter	Clark Barrett

2012-06-18	unnecessary ^ in regular expression; warning produced on smt-exec	Morgan Deters

2012-06-18	QF_LRA strategy in run script, now final (?) for smt-comp 2012	Morgan Deters

2012-06-18	final sources (?) for competition	Morgan Deters

2012-06-18	Fix for slow array rewrite and minor bug fix in arrays that popped up as a ↵	Clark Barrett
	result
2012-06-18	small bug fix and performance fix in ite simplifier	Clark Barrett

2012-06-18	fixed smt version 1 parser for quantifiers	Andrew Reynolds

2012-06-18	tracing code to make sure decision options are being set correctly	Kshitij Bansal

2012-06-18	bugfix, enable only QF_LRA, not other arith	Kshitij Bansal

2012-06-18	QF_LRA, Quantifiers: enable use decision for (only for) stopping search	Kshitij Bansal

2012-06-18	Fixing bug 360. The driver wasn't exiting when there was an error (it just ↵	Morgan Deters
	plowed ahead to the next command). Now the driver exits on the first error, unless it's in interactive mode.
2012-06-17	QF_AUFLIA: enable use decision for (only for) stopping search	Kshitij Bansal

2012-06-17	fixing a problem due to lemmas produced while backtracking	Dejan Jovanović

2012-06-17	--decision=justification-stoponly : use decision engine only for stopping	Kshitij Bansal
	search early, not to make decisions new options.h :)
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	Removed assertion that can fail	Clark Barrett

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	small change to equality assertions so that one doesn't get x = y and y = x	Dejan Jovanović

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	This is an attempt to fix the bug in the justification heuristic. The	Kshitij Bansal
	other minor change is removing dependency of header file in theory_engine.h It fixes all known wrong answers in QF_BV and QF_AUFBV. It doesn't fix a wrong answer for QF_AUFLIA -- it is currently unclear what is the cause of this bug, could be sharing. Performance impact (turns out) is none on QF_BV and QF_AUFBV (except, of course, those for which the answer was wrong earlier; and also perhaps one or two off-cases) The issue was with how the infinite loop in justification stuff was prevented. To keep it short, I skip what was wrong earlier, and this is what is done now: * whenever an atomic formula is seen, a list of pairs of <IteSkolemVariable, AssertionCorrespondingToIteSkolem> is created for each skolem occuring in the atom. * we iterate over this list, doing the following: check if skolem is marked as visited. if not, mark visited, recurse, when back unmark. I lied, I will tell you what was being done earlier was -- 1. the check for not being visited was being done in each recursive call, not just for atoms. 2. The AssertionCorrespondingToIteSkolem was being used to check if something is visited and not IteSkolemVariable. I don't know if this makes any difference, but anyhow, I think this is cleaner & clearer, so I keep this.
2012-06-16	updated build script for smt-comp submission	Morgan Deters

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-16	Fixing if condition for trivial equalities in arithmetic. Also some ↵	Tim King
	whitespace issues in smt_engine.cpp.
2012-06-15	Bug fix in justification heuristic. Had to do with how	Kshitij Bansal
	a "visited" node in the recursive findSplitter method was handled (which would lead to infinite loop). Earlier, they were ignored assuming the ancestor would split on it later. The right thing to do is to split on it right away. (Fixes errors from the fuzzer, not the ones from last night's regression)
2012-06-15	Reverting rewrite rule to working version	Clark Barrett

2012-06-15	Fixes some assertion failures	Clark Barrett

2012-06-15	Fix for incompleteness bug with decision engine: repeated simplification	Clark Barrett
	could introduce additional assertions that were not beign processed by the decision engine. Now these assertions are merged in with pre-ITE-removal assertions, ensuring the decision engine sees them.
2012-06-15	Fixing mac compilation issues.	Tim King

2012-06-15	one bug fixed	Kshitij Bansal

2012-06-14	WIP	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