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

Age	Commit message (Collapse)	Author
2012-06-11	Fix for array bug with decision heuristic	Clark Barrett
	Also fixed one bv rewrite failure (more to come)
2012-06-11	fix issue referred to in bug 352 regarding infinite loop between ↵	Morgan Deters
	SubstitutionMap (when debugging tag "substitutions" is on) and DagificationVisitor
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	Turning on unconstrained simp for QF_AUFBV	Clark Barrett

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	The option --arith-presolve-lemmas had previously been renamed --unate-lemmas.	Morgan Deters
	This commit just renames it in --help documentation, etc.
2012-06-08	Extend Printer infrastructure also to the "Result" class, meaning that ↵	Morgan Deters
	different output languages can write "sat", "unsat", etc., in different ways. No output is changed by this commit, but the flexibility is added that Francois wanted at today's meeting.
2012-06-08	minor fixes, for Mac OS	Morgan Deters

2012-06-08	Fix SMT-LIBv2 ALL_SUPPORTED logic inference (by inferring it earlier).	Morgan Deters

2012-06-08	handle BitVectorSignExtend in pickler	Kshitij Bansal

2012-06-08	threadlocal	Kshitij Bansal

2012-06-08	Merge from decision branch (till r3663)	Kshitij Bansal
	(no performace or search behavior changes expected)
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	Adding EchoCommand and associated printer and parser rules:	Morgan Deters
	* SMT-LIBv2 parser now supports (echo...). * Dump() gestures can now dump EchoCommands in CVC and SMT-LIB formats. This can make it much easier to interpret output.
2012-06-07	fixing some bugs in propagation of disequalities	Dejan Jovanović
	still doesnt fix the wrong answers thought :(
2012-06-06	Don't ever call nonclausalSimplify if simplificationMode = NONE (even if	Clark Barrett
	repeatSimp is true)
2012-06-06	Fixed assertion failures	Clark Barrett

2012-06-06	removing std::cout from trunk	Morgan Deters

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

2012-06-05	More clean-up	Clark Barrett

2012-06-05	Fixed a performance issue with unconstrained simplifier	Clark Barrett

2012-06-05	Adding missing files...	Clark Barrett

2012-06-04	Added preprocessing pass that propagates unconstrained values - solves all of	Clark Barrett
	the unconstrained examples in QF_AUFBV/brummayerbiere3 - should also help generally on at least BV and maybe others. Off by default for now - results are mixed and it's hard to evaluate with so many existing assertion failures and segfaults - will re-evaluate once those are fixed
2012-06-01	add a global user-context push/pop in smt engine, just like clark's addition ↵	Morgan Deters
	the other day of a push/pop of the sat context
2012-05-31	Fixed bug in bv: one more case where non-shared equality was getting propagated	Clark Barrett
	Added a global push and pop around solving - fixes an assertion failure when TNodes are still around in a CDHashMap at destruction time.
2012-05-31	pass JAVA_CPPFLAGS properly	Morgan Deters

2012-05-30	Added BitwiseEq bitvector rewrite	Clark Barrett
	Added option "--repeat-simp" which repeats nonclausal simplification: 4 times, twice before ite removal and twice after Enabled these options (plus ite-simp) on QF_AUFBV, obtaining significant speedup on dwp examples
2012-05-30	Fixed problem with array queue growing too large	Clark Barrett

2012-05-30	remove unused/broken check build target	Morgan Deters

2012-05-29	removing now-unused TheoryEngine::setLogic() interface function	Morgan Deters

2012-05-29	Enabled SolveEq bv rewrite	Clark Barrett

2012-05-28	Added some BV rewrites, fixed bugs in array theory, made ite simp work with BV	Clark Barrett

2012-05-27	some reordering to keep invariants	Dejan Jovanović

2012-05-27	Committing the work on equality engine, I need to see how it does on the ↵	Dejan Jovanović
	regressions. New additions: * areDisequal(x, y) -> areDisequal(x, y, needProof): when asking for a disequality you must say needProof if you will ask for an explanation later. * propagation of shared dis-equalities (not yet complete, once case missing) * changes to the theories that use it, authors should check up on the changes
2012-05-27	Another expensive function call in a Debug trace	Clark Barrett

2012-05-27	Another expensive function call in a Debug line	Clark Barrett

2012-05-25	init bug fix	Kshitij Bansal

2012-05-25	Checking in fix for bug 340 - somehow didn't get checked in earlier	Clark Barrett

2012-05-24	Separating the subtheory implementations in the bitvector theory.	Dejan Jovanović

2012-05-24	Significant changes to the internals of the equality engine. Equality is not ↵	Dejan Jovanović
	handled natively and not as a generic predicate. The changes also change the order of propagation, and can produce different conflicts. Since the engine is now used everywhere this means that so some crazy results are to be expected.
2012-05-22	This commit merges in the branch arithmetic/cprop.	Tim King