Code cleanup for TheoryArith.

5 files changed, 155 insertions, 128 deletions

diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index f099e77b9..c764d0d2e 100644
--- a/src/theory/arith/arith_utilities.h
+++ b/src/theory/arith/arith_utilities.h
@@ -206,6 +206,41 @@ inline int deltaCoeff(Kind k){
   }
 }
 
+/**
+ * Given a rewritten predicate to TheoryArith return a single kind to
+ * to indicate its underlying structure.
+ * The function returns the following in each case:
+ * - (K left right) -> K where is a wildcard for EQUAL, LEQ, or GEQ:
+ * - (NOT (EQUAL left right)) -> DISTINCT
+ * - (NOT (LEQ left right))   -> GT
+ * - (NOT (GEQ left right))   -> LT
+ * If none of these match, it returns UNDEFINED_KIND.
+ */
+ inline Kind simplifiedKind(TNode assertion){
+  switch(assertion.getKind()){
+  case kind::LEQ:
+  case  kind::GEQ:
+  case  kind::EQUAL:
+    return assertion.getKind();
+  case  kind::NOT:
+    {
+      TNode atom = assertion[0];
+      switch(atom.getKind()){
+      case  kind::LEQ: //(not (LEQ x c)) <=> (GT x c)
+        return  kind::GT;
+      case  kind::GEQ: //(not (GEQ x c) <=> (LT x c)
+        return  kind::LT;
+      case  kind::EQUAL:
+        return  kind::DISTINCT;
+      default:
+        return  kind::UNDEFINED_KIND;
+      }
+    }
+  default:
+    return kind::UNDEFINED_KIND;
+  }
+}
+
 }; /* namesapce arith */
 }; /* namespace theory */
 }; /* namespace CVC4 */
diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp
index bee24aa39..39685a2a1 100644
--- a/src/theory/arith/partial_model.cpp
+++ b/src/theory/arith/partial_model.cpp
@@ -50,6 +50,8 @@ void ArithPartialModel::setAssignment(ArithVar x, const DeltaRational& r){
     d_hasSafeAssignment[x] = true;
     d_history.push_back(x);
   }
+
+  d_deltaIsSafe = false;
   d_assignment[x] = r;
 }
 void ArithPartialModel::setAssignment(ArithVar x, const DeltaRational& safe, const DeltaRational& r){
@@ -65,6 +67,8 @@ void ArithPartialModel::setAssignment(ArithVar x, const DeltaRational& safe, con
       d_history.push_back(x);
     }
   }
+
+  d_deltaIsSafe = false;
   d_assignment[x] = r;
 }
 
@@ -101,14 +105,14 @@ void ArithPartialModel::initialize(ArithVar x, const DeltaRational& r){
 /** Must know that the bound exists both calling this! */
 const DeltaRational& ArithPartialModel::getUpperBound(ArithVar x) {
   Assert(inMaps(x));
-  Assert(!d_upperConstraint[x].isNull());
+  Assert(hasUpperBound(x));
 
   return d_upperBound[x];
 }
 
 const DeltaRational& ArithPartialModel::getLowerBound(ArithVar x) {
   Assert(inMaps(x));
-  Assert(!d_lowerConstraint[x].isNull());
+  Assert(hasLowerBound(x));
 
   return d_lowerBound[x];
 }
@@ -122,6 +126,15 @@ const DeltaRational& ArithPartialModel::getSafeAssignment(ArithVar x) const{
   }
 }
 
+const DeltaRational& ArithPartialModel::getAssignment(ArithVar x, bool safe) const{
+  Assert(inMaps(x));
+  if(safe && d_hasSafeAssignment[x]){
+    return d_safeAssignment[x];
+  }else{
+    return d_assignment[x];
+  }
+}
+
 const DeltaRational& ArithPartialModel::getAssignment(ArithVar x) const{
   Assert(inMaps(x));
   return d_assignment[x];
@@ -146,20 +159,20 @@ void ArithPartialModel::setUpperConstraint(ArithVar x, TNode constraint){
 
 TNode ArithPartialModel::getLowerConstraint(ArithVar x){
   Assert(inMaps(x));
-  Assert(!d_lowerConstraint[x].isNull());
+  Assert(hasLowerBound(x));
   return d_lowerConstraint[x];
 }
 
 TNode ArithPartialModel::getUpperConstraint(ArithVar x){
   Assert(inMaps(x));
-  Assert(!d_upperConstraint[x].isNull());
+  Assert(hasUpperBound(x));
   return d_upperConstraint[x];
 }
 
 
 
 bool ArithPartialModel::belowLowerBound(ArithVar x, const DeltaRational& c, bool strict){
-  if(d_lowerConstraint[x].isNull()){
+  if(!hasLowerBound(x)){
     // l = -\intfy
     // ? c < -\infty |-  _|_
     return false;
@@ -172,7 +185,7 @@ bool ArithPartialModel::belowLowerBound(ArithVar x, const DeltaRational& c, bool
 }
 
 bool ArithPartialModel::aboveUpperBound(ArithVar x, const DeltaRational& c, bool strict){
-  if(d_upperConstraint[x].isNull()){
+  if(!hasUpperBound(x)){
     // u = \intfy
     // ? c > \infty |-  _|_
     return false;
@@ -183,14 +196,13 @@ bool ArithPartialModel::aboveUpperBound(ArithVar x, const DeltaRational& c, bool
     return c >= d_upperBound[x];
   }
 }
-
-bool ArithPartialModel::hasBounds(ArithVar x){
-  return !d_lowerConstraint[x].isNull() || !d_upperConstraint[x].isNull();
+bool ArithPartialModel::hasEitherBound(ArithVar x){
+  return hasLowerBound(x) || hasUpperBound(x);
 }
 
 bool ArithPartialModel::strictlyBelowUpperBound(ArithVar x){
   Assert(inMaps(x));
-  if(d_upperConstraint[x].isNull()){ // u = \infty
+  if(!hasUpperBound(x)){ // u = \infty
     return true;
   }
   return d_assignment[x] < d_upperBound[x];
@@ -198,7 +210,7 @@ bool ArithPartialModel::strictlyBelowUpperBound(ArithVar x){
 
 bool ArithPartialModel::strictlyAboveLowerBound(ArithVar x){
   Assert(inMaps(x));
-  if(d_lowerConstraint[x].isNull()){ // l = -\infty
+  if(!hasLowerBound(x)){ // l = -\infty
     return true;
   }
   return  d_lowerBound[x] < d_assignment[x];
@@ -224,6 +236,10 @@ void ArithPartialModel::clearSafeAssignments(bool revert){
     }
   }
 
+  if(revert && !d_history.empty()){
+    d_deltaIsSafe = true;
+  }
+
   d_history.clear();
 }
 
@@ -236,13 +252,13 @@ void ArithPartialModel::commitAssignmentChanges(){
 
 void ArithPartialModel::printModel(ArithVar x){
   Debug("model") << "model" << x << ":"<< getAssignment(x) << " ";
-  if(d_lowerConstraint[x].isNull()){
+  if(!hasLowerBound(x)){
     Debug("model") << "no lb ";
   }else{
     Debug("model") << getLowerBound(x) << " ";
     Debug("model") << getLowerConstraint(x) << " ";
   }
-  if(d_upperConstraint[x].isNull()){
+  if(!hasUpperBound(x)){
     Debug("model") << "no ub ";
   }else{
     Debug("model") << getUpperBound(x) << " ";
@@ -270,11 +286,11 @@ void ArithPartialModel::computeDelta(){
 
   for(ArithVar x = 0; x < d_mapSize; ++x){
     const DeltaRational& a = getAssignment(x);
-    if(!d_lowerConstraint[x].isNull()){
+    if(hasLowerBound(x)){
       const DeltaRational& l = getLowerBound(x);
       deltaIsSmallerThan(l,a);
     }
-    if(!d_upperConstraint[x].isNull()){
+    if(hasUpperBound(x)){
       const DeltaRational& u = getUpperBound(x);
       deltaIsSmallerThan(a,u);
     }
diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h
index 518d59fbd..2edfdebca 100644
--- a/src/theory/arith/partial_model.h
+++ b/src/theory/arith/partial_model.h
@@ -88,6 +88,7 @@ public:
 
   /* Gets the last assignment to a variable that is known to be conistent. */
   const DeltaRational& getSafeAssignment(ArithVar x) const;
+  const DeltaRational& getAssignment(ArithVar x, bool safe) const;
 
   /* Reverts all variable assignments to their safe values. */
   void revertAssignmentChanges();
@@ -131,7 +132,13 @@ public:
   void printModel(ArithVar x);
 
   /** returns true iff x has both a lower and upper bound. */
-  bool hasBounds(ArithVar x);
+  bool hasEitherBound(ArithVar x);
+  inline bool hasLowerBound(ArithVar x){
+    return !d_lowerConstraint[x].isNull();
+  }
+  inline bool hasUpperBound(ArithVar x){
+    return !d_upperConstraint[x].isNull();
+  }
 
   bool hasEverHadABound(ArithVar var){
     return d_hasHadABound[var];
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 9458ab153..f913eda93 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -127,7 +127,7 @@ bool isNormalAtom(TNode n){
 
 
 bool TheoryArith::shouldEject(ArithVar var){
-  if(d_partialModel.hasBounds(var)){
+  if(d_partialModel.hasEitherBound(var)){
     return false;
   }else if(d_tableau.isEjected(var)) {
     return false;
@@ -171,8 +171,8 @@ void TheoryArith::reinjectVariable(ArithVar x){
   d_tableau.reinjectBasic(x);
 
 
-  DeltaRational safeAssignment = computeRowValueUsingSavedAssignment(x);
-  DeltaRational assignment = computeRowValueUsingAssignment(x);
+  DeltaRational safeAssignment = computeRowValue(x, true);
+  DeltaRational assignment = computeRowValue(x, false);
   d_partialModel.setAssignment(x,safeAssignment,assignment);
 }
 
@@ -307,8 +307,8 @@ void TheoryArith::setupInitialValue(ArithVar x){
 
     //This can go away if the tableau creation is done at preregister
     //time instead of register
-    DeltaRational safeAssignment = computeRowValueUsingSavedAssignment(x);
-    DeltaRational assignment = computeRowValueUsingAssignment(x);
+    DeltaRational safeAssignment = computeRowValue(x, true);
+    DeltaRational assignment = computeRowValue(x, false);
     d_partialModel.initialize(x,safeAssignment);
     d_partialModel.setAssignment(x,assignment);
 
@@ -317,10 +317,6 @@ void TheoryArith::setupInitialValue(ArithVar x){
     //lower bound. This is done to strongly enforce the notion that basic
     //variables should not be changed without begin checked.
 
-    //Strictly speaking checking x is unnessecary as it cannot have an upper or
-    //lower bound. This is done to strongly enforce the notion that basic
-    //variables should not be changed without begin checked.
-
   }
   Debug("arithgc") << "setupVariable("<<x<<")"<<std::endl;
 };
@@ -328,7 +324,7 @@ void TheoryArith::setupInitialValue(ArithVar x){
 /**
  * Computes the value of a basic variable using the current assignment.
  */
-DeltaRational TheoryArith::computeRowValueUsingAssignment(ArithVar x){
+DeltaRational TheoryArith::computeRowValue(ArithVar x, bool useSafe){
   Assert(d_basicManager.isBasic(x));
   DeltaRational sum = d_constants.d_ZERO_DELTA;
 
@@ -336,29 +332,14 @@ DeltaRational TheoryArith::computeRowValueUsingAssignment(ArithVar x){
   for(Row::iterator i = row->begin(); i != row->end();++i){
     ArithVar nonbasic = i->first;
     const Rational& coeff = i->second;
-    const DeltaRational& assignment = d_partialModel.getAssignment(nonbasic);
-    sum = sum + (assignment * coeff);
-  }
-  return sum;
-}
-
-/**
- * Computes the value of a basic variable using the current assignment.
- */
-DeltaRational TheoryArith::computeRowValueUsingSavedAssignment(ArithVar x){
-  Assert(d_basicManager.isBasic(x));
-  DeltaRational sum = d_constants.d_ZERO_DELTA;
 
-  Row* row = d_tableau.lookup(x);
-  for(Row::iterator i = row->begin(); i != row->end();++i){
-    ArithVar nonbasic = i->first;
-    const Rational& coeff = i->second;
-    const DeltaRational& assignment = d_partialModel.getSafeAssignment(nonbasic);
+    const DeltaRational& assignment = d_partialModel.getAssignment(nonbasic, useSafe);
     sum = sum + (assignment * coeff);
   }
   return sum;
 }
 
+
 RewriteResponse TheoryArith::preRewrite(TNode n, bool topLevel) {
   return d_nextRewriter.preRewrite(n);
 }
@@ -368,12 +349,7 @@ void TheoryArith::registerTerm(TNode tn){
 }
 
 /* procedure AssertUpper( x_i <= c_i) */
-bool TheoryArith::AssertUpper(TNode n, TNode original){
-  TNode nodeX_i = n[0];
-  ArithVar x_i = asArithVar(nodeX_i);
-  Rational dcoeff = Rational(Integer(deltaCoeff(n.getKind())));
-  DeltaRational c_i(n[1].getConst<Rational>(), dcoeff);
-
+bool TheoryArith::AssertUpper(ArithVar x_i, const DeltaRational& c_i, TNode original){
 
   Debug("arith") << "AssertUpper(" << x_i << " " << c_i << ")"<< std::endl;
   if(d_basicManager.isBasic(x_i) && d_tableau.isEjected(x_i)){
@@ -409,12 +385,7 @@ bool TheoryArith::AssertUpper(TNode n, TNode original){
 }
 
 /* procedure AssertLower( x_i >= c_i ) */
-bool TheoryArith::AssertLower(TNode n, TNode original){
-  TNode nodeX_i = n[0];
-  ArithVar x_i = asArithVar(nodeX_i);
-  Rational dcoeff = Rational(Integer(deltaCoeff(n.getKind())));
-  DeltaRational c_i(n[1].getConst<Rational>(),dcoeff);
-
+bool TheoryArith::AssertLower(ArithVar x_i, const DeltaRational& c_i, TNode original){
   Debug("arith") << "AssertLower(" << x_i << " " << c_i << ")"<< std::endl;
 
   if(d_basicManager.isBasic(x_i) && d_tableau.isEjected(x_i)){
@@ -449,11 +420,7 @@ bool TheoryArith::AssertLower(TNode n, TNode original){
 }
 
 /* procedure AssertLower( x_i == c_i ) */
-bool TheoryArith::AssertEquality(TNode n, TNode original){
-  Assert(n.getKind() == EQUAL);
-  TNode nodeX_i = n[0];
-  ArithVar x_i = asArithVar(nodeX_i);
-  DeltaRational c_i(n[1].getConst<Rational>());
+bool TheoryArith::AssertEquality(ArithVar x_i, const DeltaRational& c_i, TNode original){
 
   Debug("arith") << "AssertEquality(" << x_i << " " << c_i << ")"<< std::endl;
 
@@ -501,7 +468,7 @@ bool TheoryArith::AssertEquality(TNode n, TNode original){
 
   return false;
 }
-void TheoryArith::update(ArithVar x_i, DeltaRational& v){
+void TheoryArith::update(ArithVar x_i, const DeltaRational& v){
   Assert(!d_basicManager.isBasic(x_i));
   DeltaRational assignment_x_i = d_partialModel.getAssignment(x_i);
   ++(d_statistics.d_statUpdates);
@@ -757,61 +724,66 @@ Node TheoryArith::generateConflictBelow(ArithVar conflictVar){
   return conflict;
 }
 
+template <bool selectLeft>
+TNode getSide(TNode assertion, Kind simpleKind){
+  switch(simpleKind){
+  case LT:
+  case GT:
+  case DISTINCT:
+    return selectLeft ? (assertion[0])[0] : (assertion[0])[1];
+  case LEQ:
+  case GEQ:
+  case EQUAL:
+    return selectLeft ? assertion[0] : assertion[1];
+  default:
+    Unreachable();
+    return TNode::null();
+  }
+}
 
-//TODO get rid of this!
-Node TheoryArith::simulatePreprocessing(TNode n){
-  if(n.getKind() == NOT){
-    Node sub = simulatePreprocessing(n[0]);
-    Assert(sub.getKind() != NOT);
-    return NodeManager::currentNM()->mkNode(NOT,sub);
+ArithVar TheoryArith::determineLeftVariable(TNode assertion, Kind simpleKind){
+  TNode left = getSide<true>(assertion, simpleKind);
 
+  if(isTheoryLeaf(left)){
+    return asArithVar(left);
   }else{
-    Assert(isNormalAtom(n));
-    Kind k = n.getKind();
-
-    Assert(isRelationOperator(k));
-    if(n[0].getMetaKind() == metakind::VARIABLE){
-      return n;
-    }else {
-      TNode left = n[0];
-      TNode right = n[1];
-      Assert(left.hasAttribute(Slack()));
-      Node slack = left.getAttribute(Slack());
-      return NodeManager::currentNM()->mkNode(k,slack,right);
-    }
+    Assert(left.hasAttribute(Slack()));
+    TNode slack = left.getAttribute(Slack());
+    return asArithVar(slack);
   }
 }
 
-bool TheoryArith::assertionCases(TNode original, TNode assertion){
-  switch(assertion.getKind()){
+DeltaRational determineRightConstant(TNode assertion, Kind simpleKind){
+  TNode right = getSide<false>(assertion, simpleKind);
+
+  Assert(right.getKind() == CONST_RATIONAL);
+  const Rational& noninf = right.getConst<Rational>();
+
+  Rational inf = Rational(Integer(deltaCoeff(simpleKind)));
+  return DeltaRational(noninf, inf);
+}
+
+bool TheoryArith::assertionCases(TNode assertion){
+  Kind simpKind = simplifiedKind(assertion);
+  Assert(simpKind != UNDEFINED_KIND);
+  ArithVar x_i = determineLeftVariable(assertion, simpKind);
+  DeltaRational c_i = determineRightConstant(assertion, simpKind);
+
+  Debug("arith_assertions") << "arith assertion(" << assertion
+                            << " \\-> "
+                            <<x_i<<" "<< simpKind <<" "<< c_i << ")" << std::endl;
+  switch(simpKind){
   case LEQ:
-    return AssertUpper(assertion, original);
+  case LT:
+    return AssertUpper(x_i, c_i, assertion);
+  case GT:
   case GEQ:
-    return AssertLower(assertion, original);
+    return AssertLower(x_i, c_i, assertion);
   case EQUAL:
-    return AssertEquality(assertion,original);
-  case NOT:
-    {
-      TNode atom = assertion[0];
-      switch(atom.getKind()){
-      case LEQ: //(not (LEQ x c)) <=> (GT x c)
-        {
-          Node pushedin = pushInNegation(assertion);
-          return AssertLower(pushedin,original);
-        }
-      case GEQ: //(not (GEQ x c) <=> (LT x c)
-        {
-          Node pushedin = pushInNegation(assertion);
-          return AssertUpper(pushedin,original);
-        }
-      case EQUAL:
-        d_diseq.push_back(assertion);
-        return false;
-      default:
-        Unreachable();
-        return false;
-      }
-    }
+    return AssertEquality(x_i, c_i, assertion);
+  case DISTINCT:
+    d_diseq.push_back(assertion);
+    return false;
   default:
     Unreachable();
     return false;
@@ -823,14 +795,10 @@ void TheoryArith::check(Effort level){
 
   while(!done()){
 
-    Node original = get();
-    Node assertion = simulatePreprocessing(original);
-    Debug("arith_assertions") << "arith assertion(" << original
-                              << " \\-> " << assertion << ")" << std::endl;
-
-    d_propagator.assertLiteral(original);
-    bool conflictDuringAnAssert = assertionCases(original, assertion);
+    Node assertion = get();
 
+    d_propagator.assertLiteral(assertion);
+    bool conflictDuringAnAssert = assertionCases(assertion);
 
     if(conflictDuringAnAssert){
       d_partialModel.revertAssignmentChanges();
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 26dcc9825..5d00c4cc8 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -153,16 +153,18 @@ private:
    *
    * returns true if a conflict was asserted.
    */
-  bool AssertLower(TNode n, TNode orig);
-  bool AssertUpper(TNode n, TNode orig);
+  bool AssertLower(ArithVar x_i, const DeltaRational& c_i, TNode orig);
+  bool AssertUpper(ArithVar x_i, const DeltaRational& c_i, TNode orig);
+  bool AssertEquality(ArithVar x_i, const DeltaRational& c_i, TNode orig);
+
+  ArithVar determineLeftVariable(TNode assertion, Kind simpleKind);
 
-  bool AssertEquality(TNode n, TNode orig);
 
   /**
    * Updates the assignment of a nonbasic variable x_i to v.
    * Also updates the assignment of basic variables accordingly.
    */
-  void update(ArithVar x_i, DeltaRational& v);
+  void update(ArithVar x_i, const DeltaRational& v);
 
   /**
    * Updates the value of a basic variable x_i to v,
@@ -233,12 +235,14 @@ private:
   /** Initial (not context dependent) sets up for a new slack variable.*/
   void setupSlack(TNode left);
 
-
-  /** Computes the value of a row in the tableau using the current assignment.*/
-  DeltaRational computeRowValueUsingAssignment(ArithVar x);
-
-  /** Computes the value of a row in the tableau using the safe assignment.*/
-  DeltaRational computeRowValueUsingSavedAssignment(ArithVar x);
+  /**
+   * Computes the value of a basic variable using the assignments
+   * of the values of the variables in the basic variable's row tableau.
+   * This can compute the value using either:
+   * - the the current assignment (useSafe=false) or
+   * - the safe assignment (useSafe = true).
+   */
+  DeltaRational computeRowValue(ArithVar x, bool useSafe);
 
   /** Checks to make sure the assignment is consistent with the tableau. */
   void checkTableau();
@@ -250,16 +254,13 @@ private:
    * Handles the case splitting for check() for a new assertion.
    * returns true if their is a conflict.
    */
-  bool assertionCases(TNode original, TNode assertion);
+  bool assertionCases(TNode assertion);
 
   ArithVar findBasicRow(ArithVar variable);
   bool shouldEject(ArithVar var);
   void ejectInactiveVariables();
   void reinjectVariable(ArithVar x);
 
-  //TODO get rid of this!
-  Node simulatePreprocessing(TNode n);
-
   void asVectors(Polynomial& p,
                  std::vector<Rational>& coeffs,
                  std::vector<ArithVar>& variables) const;