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

Age	Commit message (Collapse)	Author
2012-02-21	Fix for bug303. The problem was with function applications that get ↵	Dejan Jovanović
	normalized when added to the term database. For example, if x=y exists, and the term f(x) is added, f(y) was stored. So, when getExplanation(f(x), f(y)) was called, trouble ensued. I now keep the original version so that explanations can be properly produced. Also added theory::assertions debug flag that will printout assertions of each theory for ease and uniformity of debugging in the future.
2012-02-21	don't require libboost_thread (its presence is detected at configure-time), ↵	Morgan Deters
	and other build/documentation fixes from yesterday's portfolio merge; resolves bug 302
2012-02-20	fix sharing issue for portfolio (full lit-to-node map wasn't being kept in ↵	Morgan Deters
	my previous checkin)
2012-02-20	fix "make dist"	Morgan Deters

2012-02-20	zlib not required; remove configure's dependency on it	Morgan Deters

2012-02-20	portfolio merge	Morgan Deters

2012-02-20	readline links in -ltermcap -ltinfo too (fixes breakage in static-binary builds)	Morgan Deters

2012-02-20	Added Theory::postsolve() infrastructure as Clark requested.	Morgan Deters
	(Though currently unused.) For theories that request presolve and postsolve (in their kinds file), they will get a presolve() notification before the first check(). After the final check during the current search, they get a postsolve(). presolve() and postsolve() notifications always come in pairs, bracketing all check()/propagate()/getValue() calls related to a single query. In the case of incremental benchmarks, theories may get additional presolve()/postsolve() pairs, but again, they always come in pairs. Expected performance impact: none (for theories that don't use it) http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3598&reference_id=3581&p=5
2012-02-20	By default, ONLY enable symmetry breaker ONLY for QF_UF (both SMT-LIBv1	Morgan Deters
	and SMT-LIBv2). There are --enable-symmetry-breaker and --disable-symmetry-breaker options that are always respected regardless of this default. Expected performance impact: positive New default (UF only) compared to old default (always on): http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3594&reference_id=3595&p=5 Symmetry breaker remains a big win on UF: http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3594&reference_id=3596&p=5 The last link to results looks at first that the symmetry breaker should always be turned off, since its use loses more regressions than it gains. However, the lost ones are only our "QF_SAT" benchmarks. For these, we should indeed turn off the symmetry breaker, but that's impossible for now because we tag them internally with the logic "QF_UF."
2012-02-16	clarify wording in README, thanks for finding this Francois!	Morgan Deters

2012-02-16	Last commit accidentally lacked r2778 and r2779 from integer2. I have ↵	Tim King
	manually brought these changes over. Changed the tests used by test/regress/regress0/arith/integers/Makefile.am to be 15 of the more interesting tests. Did a bit of cleanup on TheoryArith to eliminate a warning and remove dead code.
2012-02-15	This commit merges into trunk the branch branches/arithmetic/integers2 from ↵	Tim King
	r2650 to r2779. - This excludes revision 2777. This revision had some strange performance implications and was delaying the merge. - This includes the new DioSolver. The DioSolver can discover conflicts, produce substitutions, and produce cuts. - The DioSolver can be disabled at command line using --disable-dio-solver. - This includes a number of changes to the arithmetic normal form. - The Integer class features a number of new number theoretic function. - This commit includes a few rather loud warning. I will do my best to take care of them today.
2012-02-13	precision in theoryskel	François Bobot

2012-02-13	proper handling of improper get-value	Morgan Deters

2012-02-12	copyright year updated to 2012	Morgan Deters

2012-02-12	separate new-theory components into a "theoryskel" directory so that new ↵	Morgan Deters
	files can be added to it without modifying the script.
2012-02-11	ensure using bash for new-theory script	Morgan Deters

2012-02-10	attempt at a fix for the local regression failure (CLN linking issues on oneiric	Morgan Deters

2012-02-10	script to ease creating a new theory from scratch (will go along with new ↵	Morgan Deters
	reference documentation)
2012-02-10	correct comment typo found during today's architectural meeting	Morgan Deters

2012-02-09	fixing antoher small bug in backtracking	Dejan Jovanović

2012-02-08	fixing a bug in uf_engine application lookup backtracking	Dejan Jovanović
	this should also fix bug299
2012-02-08	Number of changes to cvc_printer.cpp. Specialized the printing for BVPLUS, ↵	Tim King
	BVSUB, and BVMULT. Fixed a bug in printing on PREFIX operators. Added parenthsis for POSTFIX operators. Passing the ouroborous test now.
2012-02-07	re-adding comment about available languages	Morgan Deters

2012-02-07	removing the 100 integer benchmarks from regress0, too many	Dejan Jovanović

2012-02-07	fixing some missing stuff	Dejan Jovanović

2012-02-06	Fixing a bug in the integer unit tests when configured for GMP with ↵	Tim King
	assertions off.
2012-02-05	changes to the cvc4 language printer, so that it actually prints the cvc4 ↵	Dejan Jovanović
	language all theory writers should take a look a what's being printed, to ensure all cases are covered
2012-02-04	support for isWellFounded/mkGroundTerm on uninterpretted sorts. cvc4 now ↵	Andrew Reynolds
	assumes uninterpretted sorts are well-founded, allowing datatypes to work with uninterpretted sort subdata
2012-02-03	updating configure to use python-config for building python bindings	Dejan Jovanović

2012-01-27	effecting the same change in the compat Java binding as was done to CVC3 ↵	Morgan Deters
	yesterday (ValidityChecker::value() and ValidityChecker::getValue())
2012-01-25	Adding regress1 test ooo.rf6.smt2.	Tim King

2012-01-23	Partial fix to TheoryEngine::getExplanation so that SharedAssertions request ↵	Tim King
	explanations from the theory that can explain them. This partially fixes bug 295.
2012-01-23	fix for bug295	Dejan Jovanović

2012-01-17	updates to smt2 parser to support datatypes, minor updates to datatypes ↵	Andrew Reynolds
	theory/rewriter to support datatypes with non-datatype subdata
2011-12-15	Partial fix to bug 295.	Tim King

2011-12-15	Fix to the previous commit.	Tim King

2011-12-15	Partial fix in arithmetic for propagating shared terms. This partially ↵	Tim King
	resolves bug 289. Adds failing tests to regress1.
2011-12-14	added minor documentation for parametric datatypes, for bug 283	Andrew Reynolds

2011-12-14	minor fixes to printing and parsing of CVC-language defined functions and ↵	Morgan Deters
	lambdas; resolves bug 294
2011-12-14	some more bug fixes (TNode -> Node, normalize literals in explanations)	Dejan Jovanović

2011-12-12	* merging some uf stuff from incremental_work branch that somehow nobody ↵	Dejan Jovanović
	merged-in * since two theories can propagate the same literal minisat now explicitly checks that a propagated literal has not been asserted yet
2011-12-10	adding additional checks for theories propagating literals that already have ↵	Dejan Jovanović
	a value
2011-12-10	a bit more changes, when propagting equalities/dis-equalities don't assert ↵	Dejan Jovanović
	them to theories that rewrite them to true. for example, 1 != 0 rewrites to true, so it shouldn't get propagated to arithmetic.
2011-12-10	attempt to fix bug 293: if a split on a trivial shared pair is requested ↵	Dejan Jovanović
	from a theory, such as 1 = 0, it is reasserted to the theory.
2011-12-08	Disable a BV rewriter statistic (after checking with Liana) that was static,	Morgan Deters
	and thus caused big problems with programs that create two SmtEngines in one process. If we need state like this in the rewriters, we'll need to make them nonstatic.
2011-12-06	LemmaStatus changes, as agreed to during 12/2 meeting.	Morgan Deters

2011-12-06	oops, removing some integer operations that leaked in (they aren't part of ↵	Morgan Deters
	trunk yet)
2011-12-06	fix errors in smt-lib2 output; needed for debugging	Morgan Deters

2011-12-05	change short-circuiting behavior of Command execution in the main driver; ↵	Morgan Deters
	allows a (limited) form of error recovery, matching what we had previously