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	Improved implementation of Integer::length() with CLN enabled. Additional ↵	Tim King
	tests to sanity check both versions CLN and GMP versions of length.
2012-11-26	rolling back r4625 for now (closes bug 464), Andy we should talk about this ↵	Morgan Deters
	a bit more..
2012-11-26	fixup for incremental solving	Dejan Jovanović

2012-11-26	Removing DioSolver::acceptableOriginalNodes(). This assertion was too ↵	Tim King
	strong, and was broken by r4620. This commit resolves bug463. Adding a previously triggering test case.
2012-11-26	Adding support for a master equality engine. Each theory gets the master ↵	Dejan Jovanović
	equality engine through the setMasterEqualityEngine method. This is a read-only equality engine, so nothing should be added to it directly. Instead each equality engine that is of interest should have the master equality engine attached to it. To set when to use the master equality engine see TheoryEngine::finishInit().
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.