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

Age	Commit message (Collapse)	Author
2012-11-26	Improving arithmetic debugging output.	Tim King

2012-11-26	don't include internal variables in model output	Morgan Deters

2012-11-26	some fixes to language bindings and function visibility	Morgan Deters

2012-11-25	This commit fixes two incompleteness bugs (461, 459) introduced in r4611 ↵	Tim King
	dues to a problem of not correctly handling disequalities. Performance implications are uncertain.
2012-11-24	Adds ensureConstraint(...) to ConstraintDatabase. This is a slightly ↵	Tim King
	optimized way of doing getConstraint() if the user already has a ValueCollection&.
2012-11-21	- Removes getDeltaValueWithNonlinear() entirely	Tim King
	- Changes the signature of getDeltaValue to throw DeltaRationalException and ModelException -- DeltaRationalExceptions can occur with non-linear arithmetic computations that cannot be done. (0 + delta) * (1 + delta) is not a DeltaRational. -- ModelExceptions occur if getDeltaValue() is going to return a value that disagrees with its value in the model (due to non-linear arithmetic) -- ModelExceptions also occur if getDeltaValue(n) is called on a variable arithmetic has never seen before. - getEqualityStatus() now wraps and catches both of these exceptions. If either occurs, the equality status is EQUALITY_UNKNOWN. This allows arithmetic to handle terms it has never seen before in getEqualityStatus. This resolves bug 453. - Removes the dead code rowImplication() entirely.
2012-11-21	Adds a number of new capabilities to DeltaRational. This adds ↵	Tim King
	DeltaRationalException which can be called when an operation on a DeltaRational does not have well formed semantics. This allows for things like multiplying two DeltaRationals, which may or may not result in a DeltaRational.
2012-11-21	Added debugging output to --check-models. I've found this output quite ↵	Tim King
	useful while debugging.
2012-11-19	Run lastWinner thread for all commands. Earlier behavior was to run	Kshitij Bansal
	lastWinner only for (get-model) command, using thread0 otherwise.
2012-11-19	Changed the splitting-on-demand lemmas of arithmetic to no longer contain ↵	Tim King
	the equality being split on. Instead of issuing 'x != y implies (x < y or x > y)', the lemma is now '(x <= y or x >= y)'. This resolves bug 450.
2012-11-19	Fix for bug452.	Tim King

2012-11-18	Disable predicate subtyping:	Morgan Deters
	* remove from public interface (ExprManager, Type) * CVC parser reports an unimplemented feature error if used I didn't want to tear it out completely (from NodeManager, TypeNode, type-checking, pre-processing, etc.) because that's a lot of hassle and we'll add it back in after the release anyway. It does mean that CVC4::Predicate is in the public interface, but that it can't be used for anything (by users). (this commit was certified error- and warning-free by the test-and-commit script.)
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