| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
fixes bug 484
|
|
|
|
|
|
|
|
1.0.x
|
|
* added printing for total bit-vector division kinds for debugging purposes
|
|
handling user attributes in quantifiers (was broken)
(cherry-picked from commit 206edb6f11674e954f5762a1db9712131151a276)
|
|
handling user attributes in quantifiers (was broken)
|
|
* build bugfix for win32
* also fix a bug re: tuples and records in the datatypes rewriter
These fixes are for both trunk and 1.0.x branches.
(cherry picked from commit 8c8985f024cec925f774ff32ebccc306be8e4b26)
|
|
(cherry picked from commit 25c6e1331d338c6ba8d60224711343986e11cf79)
|
|
* build bugfix for win32
* also fix a bug re: tuples and records in the datatypes rewriter
These fixes are for both trunk and 1.0.x branches.
|
|
over from branches/arithmetic/converge except for the new code for simplex.
|
|
fcsimplex code.
|
|
CDInsertHashMap. CDHashSet<TNode> have been changed to CDHashSet<Node>. Switching CnfStream to use CDInsertSet. Switches a few CDHashMaps in arithmetic to use CDTrailHashMap. Documentation changes to CDHashMap.
|
|
|
|
|
|
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
Also support array-store-all for Boolean terms (related to abstract values, since that's the only way for the user to include an array-store-all in an assertion).
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
instantiation strategies moved from instantiators to central instantiation engine, removed instantiator objects, simplified rewrite rules candidate generator to use central equality engine, efficient e-matching now uses central equality engine
|
|
|
|
|
|
introduced by decision procedure
|
|
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
canonical), this fixes the followup issue of bug 438
|
|
|
|
|
|
output correct
models for such functions (though they are somewhat ugly at present).
There's still a problem with model extraction, but it's not Boolean terms' fault.
Sometimes checkModel() can report that the model is just fine, but if a user extracts
values with getValue(), they find problems with the model (i.e., it doesn't satisfy some
assertions). This appears to be due to an asymmetry between how checkModel() works and
how Model::getValue() works. I'll open a bugzilla report to discuss this after thinking
some more on it.
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
Passes simple tests and doesn't break existing functionality.
Still need some work merged in for models.
This version enables BV except for pure arithmetic (since we might otherwise need Boolean term support, which uses BV). Tonight's nightly regression run should tell us if/how that hurts performance.
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
Also some fixes to parametric datatypes I found, and fixes for a handful of bugs, including some observed with --check-models --incremental on together.
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
|
|
strong, and was broken by r4620. This commit resolves bug463. Adding a previously triggering test case.
|
|
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().
|
|
|
|
dues to a problem of not correctly handling disequalities. Performance implications are uncertain.
|
|
optimized way of doing getConstraint() if the user already has a ValueCollection&.
|
|
- 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.
|
|
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.
|
|
useful while debugging.
|
|
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.
|
|
|
|
Array select terms (thanks for the bug report Francois)
|
|
|
|
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.)
|
|
|
