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	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	fix quantifier non-bug	Kshitij Bansal

2012-06-14	Removed an assertion, unneeded header file	Clark Barrett

2012-06-14	some changes to make CVC4 work nicely with trace executor for application ↵	Morgan Deters
	track; (set-option :print-success true) supported, (exit) causes immediate exit regardless of EOF, etc.
2012-06-14	making --simplification=none the default for quantified logics; this a ↵	Morgan Deters
	request from andy. evidence of performance improvement: http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=4516&reference_id=4475&p=5
2012-06-14	bug ifx, mv	Kshitij Bansal

2012-06-14	restore destruction of stuff in driver	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	The "no-tears-in-competition-mode" commit. Change all (non-driver, ↵	Morgan Deters
	non-SAT-solver) uses of std::cout to the Message stream, and all uses of std::cerr to the Warning stream.
2012-06-14	fix cout, fix statname, rm deadcode	Kshitij Bansal

2012-06-14	changing to a more natural propagation order in uf, seems to pay off	Dejan Jovanović

2012-06-14	some changes to the uf engine	Dejan Jovanović
	* dramatically less terms to manage by doing reflexivity semantically * fixes the problem clark had with not detecting inconsistencies with shared terms i'm not sure what's the performance impact, but this is so much better and we'll deal with performance later
2012-06-14	Brings the tuning branch into trunk. This includes the changes from ↵	Tim King
	restricted-simplex.
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	Added witnesses to Constraints.	Tim King

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	Fixed whitespace warning on Makefile.	Tim King

2012-06-13	Adds debugging output to theory_engine.cpp.	Tim King

2012-06-13	Don't use the "inlined" feature of ANTLR 3.2, which causes a buffer overflow ↵	Morgan Deters
	condition when reading from stdin. This should completely resolve bug #319. However, on large inputs especially (like the stp/testcase benchmarks), this inlining feature can speed parsing by 5-10%, at the cost of not supporting interactive sessions on stdin (like in the SMT-COMP application track). So I updated the submission script and competition build so that * a competition build with antlr-inlining is built for the main and parallel tracks * a competition build without antlr-inlining is built for the application track Again, the effect is only when reading the stdin stream (but that's how SMT-COMP works). For normal (non-competition) builds, we need to support interactive sessions (from e.g. KIND) on stdin, so this inlining is off for all builds except main- and parallel-track competition builds. Also added a "get-antlr-3.4" script that automatically downloads and locally installs a copy of libantlr3c and the antlr parser generator inside the CVC4 source tree. Closing bug #319.
2012-06-13	fix for bug 354	Dejan Jovanović

2012-06-13	Fixed failing assertion when EqualityEngine is in conflict	Clark Barrett

2012-06-13	Make d_result in DE context dependent	Kshitij Bansal
	(fixes bugs in bv, others with JH on)
2012-06-13	Fixed definition of bvsmod	Clark Barrett

2012-06-13	Fixes more problems in bv rewrites	Clark Barrett

2012-06-13	Fixes lots of problems in bv rewrite rules and adds lots of assertions	Clark Barrett
	to catch any that I may have missed
2012-06-12	Fix some compile warnings (but they never showed up on church)	Morgan Deters

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	Moved some things around in the preprocessor. Now theory preprocessing gets	Clark Barrett
	called before ite simplification unless arithrewriteequality is on
2012-06-12	Fixed fuzzing bug	Clark Barrett

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

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	conflicts from theories are removable	Dejan Jovanović

2012-06-12	Changed bitvector theory rewriter so that equalities always get rewritten to	Clark Barrett
	equalities or true or false
2012-06-12	cleanup of exit mechanism when decisionEngine is on\n\n fixes some bugs we ↵	Kshitij Bansal
	were seeing in quantifiers+decision stuff
2012-06-12	Fixed bug causing QF_LIA/solver_cvc4/incorrect1.smt and ↵	Clark Barrett
	QF_LIA/solver_cvc4/incorrect3.smt
2012-06-12	Fixed failing assertion in arrays for bug 347	Clark Barrett

2012-06-12	minor cleanup, and replace a "private:" in equality engine that had been ↵	Morgan Deters
	removed by the quantifiers merge (I had reengineered some things from quantifiers so that the equality engine didn't have to expose internals as public, but then had neglected to re-privatize them)
2012-06-12	Fixed compile error	Clark Barrett

2012-06-12	Enabling constant propagation	Clark Barrett

2012-06-12	fix a few compatibility bindings issues	Morgan Deters

2012-06-12	Adding constant propagation code - needs more testing - off by default	Clark Barrett

2012-06-12	fix ordering issue of --dump-to and --default-dag-thresh. now can be ↵	Morgan Deters
	specified in either order and the DAG threshold takes.
2012-06-11	Fix to term normalization of integer equalities. Adds a regression test that ↵	Tim King
	triggered it.
2012-06-11	Fixing type comparision assertion in getEqualityStatus().	Tim King

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	mark a quantifiers global var as "static" so we can find it easier later	Morgan Deters

2012-06-11	OK, now the rewrite issues are fixed	Clark Barrett

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