Age | Commit message (Collapse) | Author |
|
(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.)
|
|
|
|
failing regression for bug 472
|
|
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
|
|
Integer((long int)((1<<29)+1)) gave different values. This was confirmed on vm-int1.cims.nyu.edu. See http://www.ginac.de/CLN/cln_3.html#SEC15 for more details. rational_white and integer_white have tests covering this.
|
|
also a regression for bug 411
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
|
|
|
|
|
|
smt.setLogic("QF_LRA"); works.
|
|
|
|
Minor changes to RELASE-NOTES
|
|
|
|
|
|
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
nagging bug Tim found in API examples
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
|
|
introduced by decision procedure
|
|
an example for combination.
|
|
documentation in base_options.
|
|
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
pattern first
just after the bindings
Do it before the release in order to not break user files later
|
|
|
|
canonical), this fixes the followup issue of bug 438
|
|
parameterized datatypes
|
|
in this release
|
|
|
|
|
|
- Adds GlobalVarAttr node attribute
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
|
|
|
|
|
|
added.
Sharing is turned on only when Boolean terms are detected during preprocessing. QF_UF problems (and others)
that don't use any Boolean terms won't have BV turned on.
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
|
|
* Fix creation of bound variables in CVC native language parser
* This corrects a problem with misleading model output
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
|
|
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.)
|
|
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
|
|
|
|
Add notice/warning when using incremental-mode + decision (it was
already disabled)
Some other minor cleanup
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
(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.)
|
|
tests to sanity check both versions CLN and GMP versions of length.
|
|
a bit more..
|
|
|
|
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().
|