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

Age	Commit message (Collapse)	Author
2012-11-18	support for quantifiers macros, bug fix for bug 454 involving E-matching ↵	Andrew Reynolds
	Array select terms (thanks for the bug report Francois)
2012-11-17	Fixed last currently known bug in array models	Clark Barrett

2012-11-17	* enable previously-failing (now succeeding) datatype example that uses records	Morgan Deters
	* some bindings cleanup (this commit was certified error- and warning-free by the test-and-commit script.)
2012-11-17	fix for language bindings (fixes debian build fail last night)	Morgan Deters

2012-11-17	* Fix for bug 445 agreed to in meeting 11/13/2012: always dump in ↵	Morgan Deters
	ALL_SUPPORTED logic * Java bindings fixes: fixed access to ostreams, iterators * Make SmtEngine::setUserAttribute() (and others) take a const string& * Also a few compliance fixes (this commit was certified error- and warning-free by the test-and-commit script.)
2012-11-16	Fix for bug451	Clark Barrett

2012-11-16	fixing and refactoring the equality iterator	Dejan Jovanović

2012-11-16	Fix dumping of array-select expressions in CVC native language.	Morgan Deters
	Thanks to Wei for the bug report.
2012-11-16	fix a compiler warning in models	Morgan Deters

2012-11-15	some fixes for --threads=1	Kshitij Bansal

2012-11-15	More fixes to model generation, with previously failing testcases	Clark Barrett
	Also refactored some header file includes to reduce compile time
2012-11-15	forgot to uncomment setLogicInternal for THEORY_BV	Liana Hadarean

2012-11-15	changed logic options so that justification is turned on for QF_ABV and ↵	Liana Hadarean
	QF_UFBV as well
2012-11-15	d_incomplete is context-dependent; we shouldn't be saving its value and ↵	Morgan Deters
	restoring after a flipDecision(). (this commit was certified error- and warning-free by the test-and-commit script.)
2012-11-15	Fix for bug 447.	Tim King

2012-11-15	Fixed another AUFBV model bug. BV equality subtheory needed to do something	Clark Barrett
	similar to arrays - limit the set of terms reported to those relevant in the current context. Also removed collectModelInfo from sharedTermsDatabase - doesn't seem to be needed any more.
2012-11-14	Fix for bug 407. mkAnonymousFunction() in the parser no longer uses ':'. CVC ↵	Tim King
	printer now properly prints LAMBDAs. Model builing now gives bound variables names that can be parsed bypresentation language.
2012-11-14	replaced all static member data from rewrite rule triggers, added ↵	Andrew Reynolds
	infrastructure for recognizing quantifier macros
2012-11-14	Fixed a typo in r4576	Tim King

2012-11-14	Beautifying smt_engine.cpp.	Tim King

2012-11-14	Fix to bug449. Adds shared constants to the set of DeltaRationals that must ↵	Tim King
	be in the final total order.
2012-11-14	bug fixes to models, array rewriter with previously failing testcases	Clark Barrett

2012-11-14	Quantifiers enabled with portfolio, closing bug 423.	Kshitij Bansal

2012-11-14	fix a race problem. due to interrupt mechanism minisat returned true instead ↵	Kshitij Bansal
	of undef.
2012-11-13	More bugfixes for models	Clark Barrett

2012-11-13	SmtEngine::checkModel() should only be called if the result is sat or ↵	Tim King
	unknown because of incompleteness. Other unknown results are not safe to build models for, timeout, interrupted, etc.
2012-11-13	refactoring of quantifiers rewriter based on code review from yesterday, ↵	Andrew Reynolds
	refactoring code out of instantiators in preparation for quantifiers equality engine
2012-11-13	fixed failed bv regressions by refactoring out some rewrite rules from ↵	Liana Hadarean
	smt_engine.cpp
2012-11-13	added support for division by zero for bit-vector division operators	Liana Hadarean

2012-11-13	Relaxing too-strict assertion	Clark Barrett

2012-11-13	Fixed an array rewriting bug found by fuzzer	Clark Barrett

2012-11-13	Fixed bug in array constant normalization found by fuzzer.	Clark Barrett

2012-11-12	Improved error reporting for improperly using non-linear division in linear ↵	Tim King
	arithmetic.
2012-11-12	Delta is now generated in arithmetic to keep consistent the total order of ↵	Tim King
	DeltaRational values for lowerbounds, upperbounds, assignments and disequalities. Throws LogicException when a non-linear term is asserted and the the LogicInfo isLinear() disagrees.
2012-11-12	changed BitVector::unsignedRem to match the behavior of the bit-blasted ↵	Liana Hadarean
	circuit for division by 0; temporary fix for bug440
2012-11-12	Fix for bug 444, dealing with the placing of set-logic in dumping modes.	Morgan Deters
	CVC4 now produces equivalent output when dumping the SMT1 and SMT2 attachments to that bug report. This also fixes a memory leak in the new-variable-notification mechanism. (this commit was certified error- and warning-free by the test-and-commit script.)
2012-11-12	* Fix language bindings: various issues	Morgan Deters
	remove a number of warnings in bindings generation give appropriate names for operator-overloading ** make sure Java language bindings are built with -fno-strict-aliasing, to ensure the optimizer doesn't produce bad code * Also remove BitVector::equals(), which wasn't used and was inconsistently implemented (operator==() is still there). (this commit was certified error- and warning-free by the test-and-commit script.)
2012-11-12	minor bug fixes for quantifiers, added sort inference module (not ready to ↵	Andrew Reynolds
	be used yet), added new totality lemma option for uf strong solver
2012-11-11	Fixes for the arithmetic normal form and rewriter to handle arbitrary ↵	Tim King
	constants for total functions.
2012-11-10	Beautifying integer_cln_imp.h	Tim King

2012-11-10	Fix to quantifier rewritting not being idempotent. See bug 441.	Tim King

2012-11-10	Removing rewriter call in SmtEngine::addFormula().	Tim King

2012-11-10	Fixed missing \ in uflra/Makefile.ma	Clark Barrett
	Fixed another model bug and added previously failing fuzz testcase
2012-11-10	Fix for bug 439. Delta computation now includes disequality information.	Tim King

2012-11-10	Updates to Clark's commit r4540:	Morgan Deters
	* ALL_SUPPORTED/QF_ALL_SUPPORTED don't include nonlinear * Change "Notice" to "Warning" when produce-models turned off due to non-linear (this commit was certified error- and warning-free by the test-and-commit script.)
2012-11-10	fix typo in language bindings	Morgan Deters

2012-11-10	Finally tracked down problems in regressions and fuzz results (this also	Clark Barrett
	explains why my build was giving different answers from Dejan's build). Problem was that if you run: cvc4 --check-models foo.smt it would fail, but if you run cvc4 --check-models --produce-models foo.smt it would succeed. Even though produce-models is supposed to be automatically set when you set check-models, it seems this was happening too late. Fixed by removing any distinction between produce-models and check-models in the heuristic setting code. Kind of ugly though. Also, disable models if nonlinear arithmetic is on.
2012-11-09	TheoryEngineModelBuilder::buildModel() is only called once with ↵	Morgan Deters
	fullModel=true, within a SAT context. This fixes some outstanding model bugs. Committing also a Clark-provided assertion the Model code to ensure the call is only done once per context. (this commit was certified error- and warning-free by the test-and-commit script.)
2012-11-09	export null nodes (fixes a bug in portfolio model stuff)	Kshitij Bansal

2012-11-09	Bug-fix for a crash involving improperly-thrown exceptions; also, add ↵	Morgan Deters
	LogicException for errors where the user uses a feature not permitted in the current logic (e.g., a quantifier in a QF logic)