Age | Commit message (Collapse) | Author | |
---|---|---|---|
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 | Disabling test/regress/regress0/push-pop/bug396.smt2. This takes 2m to run ↵ | Tim King | |
in debug mode. This is too long for a regress0 test. | |||
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-26 | Makefile fix for new versions of Make (thanks Clark for noticing this); see ↵ | Morgan Deters | |
e.g. http://osdir.com/ml/bug-make-gnu/2011-04/msg00011.html | |||
2012-11-25 | Adding a regression test from bug 462. | Tim King | |
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-23 | Example of rewrite rules use that comes from an harness test | François Bobot | |
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 | Adding hand minimized test for bug 450. | Tim King | |
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 | fix for "make examples" | Morgan Deters | |
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 | fuzz15 should have been fuzz14 | Clark Barrett | |
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-15 | Fixing comments in print_lambda.cvc. | Tim King | |
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 |