- 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.

1 files changed, 6 insertions, 7 deletions

diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 8cd8a01b2..0773ab7ba 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -75,7 +75,6 @@ private:
   //                     if unknown, the simplex priority queue cannot be emptied
   int d_unknownsInARow;
 
-  bool rowImplication(ArithVar v, bool upperBound, const DeltaRational& r);
 
   /**
    * This counter is false if nothing has been done since the last cut.
@@ -298,14 +297,14 @@ private:
   /** The constraint database associated with the theory. */
   ConstraintDatabase d_constraintDatabase;
 
-  /** Internal model value for the atom */
-  bool getDeltaAtomValue(TNode n) const;
+  class ModelException : public Exception {
+  public:
+    ModelException(TNode n, const char* msg) throw ();
+    virtual ~ModelException() throw ();
+  };
 
   /** Internal model value for the node */
-  DeltaRational getDeltaValue(TNode n) const;
-
-  /** TODO : get rid of this. */
-  DeltaRational getDeltaValueWithNonlinear(TNode n, bool& failed) const;
+  DeltaRational getDeltaValue(TNode n) const throw (DeltaRationalException, ModelException);
 
   /** Uninterpretted function symbol for use when interpreting
    * division by zero.