- Removes getDeltaValueWithNonlinear() entirely
authorTim King <taking@cs.nyu.edu>
Wed, 21 Nov 2012 18:46:23 +0000 (18:46 +0000)
committerTim King <taking@cs.nyu.edu>
Wed, 21 Nov 2012 18:46:23 +0000 (18:46 +0000)
commit9fe111daad65bc1b6375cc5ed18d3c8eba65887f
treea15be31aee95147a3866e358073e3a7919879dcd
parent369440efdcf26321f588b6b485e40f7c609f12da
- Removes getDeltaValueWithNonlinear() entirely
- 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.
src/theory/arith/theory_arith.cpp
src/theory/arith/theory_arith.h