| Age | Commit message (Collapse) | Author |
|---|
|
|
|
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.)
|
|
|
|
|
|
Also refactored some header file includes to reduce compile time
|
|
restoring after a flipDecision().
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
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.
|
|
printer now properly prints LAMBDAs. Model builing now gives bound variables names that can be parsed bypresentation language.
|
|
infrastructure for recognizing quantifier macros
|
|
|
|
be in the final total order.
|
|
|
|
|
|
refactoring code out of instantiators in preparation for quantifiers equality engine
|
|
smt_engine.cpp
|
|
|
|
|
|
|
|
|
|
arithmetic.
|
|
DeltaRational values for lowerbounds, upperbounds, assignments and disequalities. Throws LogicException when a non-linear term is asserted and the the LogicInfo isLinear() disagrees.
|
|
be used yet), added new totality lemma option for uf strong solver
|
|
constants for total functions.
|
|
|
|
Fixed another model bug and added previously failing fuzz testcase
|
|
|
|
* ALL_SUPPORTED/QF_ALL_SUPPORTED don't include nonlinear
* Change "Notice" to "Warning" when produce-models turned off due to non-linear
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
fullModel=true, within a SAT context. This fixes some outstanding model bugs.
Committing also a Clark-provided assertion the Model code to ensure the call is only done once per context.
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
LogicException for errors where the user uses a feature not permitted in the current logic (e.g., a quantifier in a QF logic)
|
|
|
|
for division by 0.
|
|
* fixed TypeNode::getBaseType() for predicate subtypes
* added Type::getBaseType() for public interface
* added unit testing
To avoid confusion, also:
* renamed PredicateType::getBaseType() to "getParentType()"
* renamed TypeNode::getSubtypeBaseType() to "getSubtypeParentType()"
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
uninterpreted functions for division by 0.
|
|
|
|
discovered (still outstanding). :-(
* Fix a documentation-building problem when building from tarballs (fixes distcheck build failure last night)
* Provide expected output for arith regression 'mod.01.smt2'
* Also, fix a compiler warning in inst_gen.cpp
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
|
|
|
|
equality query
|
