Some assorted fixes and local optimizations for theory arith.

diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp
index d4be75559c078c2ef933c5c45ed3d8a50f09bdb7..bb2864cf9ce96dae1e19bc6afd4929c4788e1c9c 100644 (file)
--- a/src/theory/arith/partial_model.cpp
+++ b/src/theory/arith/partial_model.cpp
@@ -44,19 +44,16 @@ void ArithPartialModel::setLowerBound(TNode x, const DeltaRational& r){
 
 void ArithPartialModel::setAssignment(TNode x, const DeltaRational& r){
   Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
-
   Assert(x.hasAttribute(partial_model::Assignment()));
+  Assert(x.hasAttribute(partial_model::SafeAssignment()));
 
   DeltaRational* curr = x.getAttribute(partial_model::Assignment());
 
-  if(d_unsafeMode){
-    Assert(x.hasAttribute(partial_model::SafeAssignment()));
-    DeltaRational* saved = x.getAttribute(partial_model::SafeAssignment());
-    if(saved == NULL){
-      saved = new DeltaRational(*curr);
-      x.setAttribute(partial_model::SafeAssignment(), saved);
-      d_history.push_back(x);
-    }
+  DeltaRational* saved = x.getAttribute(partial_model::SafeAssignment());
+  if(saved == NULL){
+    saved = new DeltaRational(*curr);
+    x.setAttribute(partial_model::SafeAssignment(), saved);
+    d_history.push_back(x);
   }
 
   *curr = r;
@@ -99,14 +96,14 @@ DeltaRational ArithPartialModel::getLowerBound(TNode x) const{
 
 DeltaRational ArithPartialModel::getSafeAssignment(TNode x) const{
   Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
-  if(d_unsafeMode){
-    Assert( x.hasAttribute(partial_model::SafeAssignment()));
-    DeltaRational* safeAssignment = x.getAttribute(partial_model::SafeAssignment());
-    if(safeAssignment != NULL){
-      return *safeAssignment;
-    }
+  Assert( x.hasAttribute(SafeAssignment()));
+
+  DeltaRational* safeAssignment = x.getAttribute(SafeAssignment());
+  if(safeAssignment != NULL){
+    return *safeAssignment;
+  }else{
+    return getAssignment(x); //The current assignment is safe.
   }
-  return getAssignment(x);
 }
 
 const DeltaRational& ArithPartialModel::getAssignment(TNode x) const{
@@ -238,34 +235,19 @@ bool ArithPartialModel::assignmentIsConsistent(TNode x){
   return  above_li && below_ui;
 }
 
-void ArithPartialModel::turnOnUnsafeMode(){
-  Assert(!d_unsafeMode);
-  Assert(d_history.empty());
-
-  d_unsafeMode = true;
-}
-
-void ArithPartialModel::turnOffUnsafeMode(){
-  Assert(d_unsafeMode);
-  Assert(d_history.empty());
-
-  d_unsafeMode = false;
-}
 
 void ArithPartialModel::clearSafeAssignments(bool revert){
-  Assert(d_unsafeMode);
 
   for(HistoryList::iterator i = d_history.begin(); i != d_history.end(); ++i){
     TNode x = *i;
 
-    Assert(x.hasAttribute(partial_model::SafeAssignment()));
+    Assert(x.hasAttribute(SafeAssignment()));
+    Assert(x.hasAttribute(Assignment()));
 
-    DeltaRational* safeAssignment = x.getAttribute(partial_model::SafeAssignment());
+    DeltaRational* safeAssignment = x.getAttribute(SafeAssignment());
 
     if(revert){
-      Assert(x.hasAttribute(partial_model::Assignment()));
-
-      DeltaRational* assign = x.getAttribute(partial_model::Assignment());
+      DeltaRational* assign = x.getAttribute(Assignment());
       *assign = *safeAssignment;
     }
     x.setAttribute(partial_model::SafeAssignment(), NULL);

diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h
index d04d8dd8cf24e51f78739914cac6f66125e4d587..26f9a135bb70798bff5800779c161be08cf22275 100644 (file)
--- a/src/theory/arith/partial_model.h
+++ b/src/theory/arith/partial_model.h
@@ -60,12 +60,13 @@ typedef expr::Attribute<SafeAssignmentAttrID,
  * each variable.  This information is conext dependent.
  */
 typedef context::CDMap<TNode, DeltaRational, TNodeHashFunction> CDDRationalMap;
-/* Side disucssion for why new tables are introduced instead of using the attribute
- * framework.
- * It comes down to that the obvious ways to use the current attribute framework do
- * do not provide a terribly satisfying answer.
+/* Side disucssion for why new tables are introduced instead of using the
+ * attribute framework.
+ * It comes down to that the obvious ways to use the current attribute
+ * framework do not provide a terribly satisfying answer.
  * - Suppose the type of the attribute is CD and maps to type DeltaRational.
- *   Well it can't map to a DeltaRational, and it thus it will be a DeltaRational*
+ *   Well it can't map to a DeltaRational, and it thus it will be a
+ *   DeltaRational*
  *   However being context dependent means givening up cleanup functions.
  *   So this leaks memory.
  * - Suppose the type of the attribute is CD and the type mapped to
@@ -74,22 +75,23 @@ typedef context::CDMap<TNode, DeltaRational, TNodeHashFunction> CDDRationalMap;
  *   Inefficiency: Every lookup and comparison will require going through the
  *   massaging in between a node and the constant being wrapped. Every update
  *   requires going through the additional expense of creating at least 1 node.
- *   The Uglyness: If this was chosen it would also suggest using comparisons against
- *   DeltaRationals for the tracking the constraints for conflict analysis.
- *   This seems to invite misuse and introducing Nodes that should probably not escape
- *   arith.
- * - Suppose that the of the attribute was not CD and mapped to a CDO<DeltaRational*>
- *   or similarly a ContextObj that wraps a DeltaRational*.
+ *   The Uglyness: If this was chosen it would also suggest using comparisons
+ *   against DeltaRationals for the tracking the constraints for conflict
+ *   analysis. This seems to invite misuse and introducing Nodes that should
+ *   probably not escape arith.
+ * - Suppose that the of the attribute was not CD and mapped to a
+ *   CDO<DeltaRational*> or similarly a ContextObj that wraps a DeltaRational*.
  *   This is currently rejected just because this is difficult to get right,
- *   and maintain. However with enough effort this the best solution is probably of
- *   this form.
+ *   and maintain. However with enough effort this the best solution is
+ *   probably of this form.
  */
 
 
 /**
  * This is the literal that was asserted in the current context to the theory
  * that asserted the tightest lower bound on a variable.
- * For example: for a variable x this could be the constraint (>= x 4) or (not (<= x 50))
+ * For example: for a variable x this could be the constraint
+ *    (>= x 4) or (not (<= x 50))
  * Note the strong correspondence between this and LowerBoundMap.
  * This is used during conflict analysis.
  */
@@ -117,18 +119,18 @@ private:
   partial_model::CDDRationalMap d_UpperBoundMap;
 
 
+  /**
+   * List contains all of the variables that have an unsafe assignment.
+   */
   typedef std::vector<TNode> HistoryList;
   HistoryList d_history;
 
-  bool d_unsafeMode;
-
 public:
 
   ArithPartialModel(context::Context* c):
     d_LowerBoundMap(c),
     d_UpperBoundMap(c),
-    d_history(),
-    d_unsafeMode(false)
+    d_history()
   { }
 
   void setLowerConstraint(TNode x, TNode constraint);
@@ -138,23 +140,24 @@ public:
 
 
 
+  /* Initializes a variable to a safe value.*/
   void initialize(TNode x, const DeltaRational& r);
 
+  /* Gets the last assignment to a variable that is known to be conistent. */
   DeltaRational getSafeAssignment(TNode x) const;
 
-  bool isInUnsafeMode() { return d_unsafeMode;  }
-
-  void turnOnUnsafeMode();
-  void turnOffUnsafeMode();
-
+  /* Reverts all variable assignments to their safe values. */
   void revertAssignmentChanges();
-  void commitAssignmentChanges();
 
+  /* Commits all variables assignments as safe.*/
+  void commitAssignmentChanges();
 
 
 
   void setUpperBound(TNode x, const DeltaRational& r);
   void setLowerBound(TNode x, const DeltaRational& r);
+
+  /* Sets an unsafe variable assignment */
   void setAssignment(TNode x, const DeltaRational& r);
 
   /** Must know that the bound exists before calling this! */
@@ -182,6 +185,11 @@ public:
   void printModel(TNode x);
 
 private:
+
+  /**
+   * This function implements the mostly identical:
+   * revertAssignmentChanges() and commitAssignmentChanges().
+   */
   void clearSafeAssignments(bool revert);
 };
 

diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h
index e43b48c6690256b0d7993860becfd93f17c8a22a..a5499db0825bbc18be112877cba3025d55ea70e5 100644 (file)
--- a/src/theory/arith/tableau.h
+++ b/src/theory/arith/tableau.h
@@ -55,7 +55,6 @@ public:
 
     //TODO Assert(d_x_i.getType() == REAL);
     Assert(sum.getKind() == PLUS);
-    Rational zero(0,1);
 
     for(TNode::iterator iter=sum.begin(); iter != sum.end(); ++iter){
       TNode pair = *iter;
@@ -68,10 +67,9 @@ public:
       //TODO Assert(var_i.getKind() == REAL);
       Assert(!has(var_i));
       d_nonbasic.insert(var_i);
-      Rational q = coeff.getConst<Rational>();
-      d_coeffs[var_i] = q;
-      Assert(q != zero);
-      Assert(d_coeffs[var_i] != zero);
+      d_coeffs[var_i] = coeff.getConst<Rational>();
+      Assert(coeff.getConst<Rational>() != Rational(0,1));
+      Assert(d_coeffs[var_i] != Rational(0,1));
     }
   }
 
@@ -134,7 +132,21 @@ public:
         iter != row_s.d_nonbasic.end();
         ++iter){
       TNode x_j = *iter;
-      Rational a_sj = a_rs * row_s.lookup(x_j);
+      Rational a_sj = row_s.lookup(x_j);
+      a_sj *= a_rs;
+      CoefficientTable::iterator coeff_iter = d_coeffs.find(x_j);
+
+      if(coeff_iter != d_coeffs.end()){
+        coeff_iter->second += a_sj;
+        if(coeff_iter->second == zero){
+          d_coeffs.erase(coeff_iter);
+          d_nonbasic.erase(x_j);
+        }
+      }else{
+        d_nonbasic.insert(x_j);
+        d_coeffs.insert(make_pair(x_j,a_sj));
+      }
+      /*
       if(has(x_j)){
         d_coeffs[x_j] = d_coeffs[x_j] + a_sj;
         if(d_coeffs[x_j] == zero){
@@ -145,6 +157,7 @@ public:
         d_nonbasic.insert(x_j);
         d_coeffs[x_j] = a_sj;
       }
+      */
     }
   }
 

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 92781e0bafc102820e450f1570344501a395ecb8..6c6a61adfcc07c6ccb45404dbf499b5a8e9e28f4 100644 (file)
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -30,7 +30,6 @@
 #include "theory/arith/delta_rational.h"
 #include "theory/arith/partial_model.h"
 #include "theory/arith/tableau.h"
-//#include "theory/arith/normal.h"
 #include "theory/arith/slack.h"
 #include "theory/arith/basic.h"
 
@@ -87,7 +86,7 @@ bool isBasicSum(TNode n){
 }
 
 bool isNormalAtom(TNode n){
-  
+
   if(!(n.getKind() == LEQ|| n.getKind() == GEQ || n.getKind() == EQUAL)){
     return false;
   }
@@ -109,6 +108,7 @@ void TheoryArith::preRegisterTerm(TNode n) {
   Debug("arith_preregister") << "arith: begin TheoryArith::preRegisterTerm("
                              << n << ")" << endl;
 
+  Kind k = n.getKind();
   if(n.getKind() == EQUAL){
     if(!n.getAttribute(EagerlySplitUpon())){
       TNode left = n[0];
@@ -131,47 +131,20 @@ void TheoryArith::preRegisterTerm(TNode n) {
     setupVariable(n);
   }
 
-  //TODO is an atom
-  if(isRelationOperator(n.getKind())){
 
+  //TODO is an atom
+  if(isRelationOperator(k)){
     Assert(isNormalAtom(n));
-    Node normalForm(n);
-
-    if(normalForm.getKind() == NOT){
-      normalForm = pushInNegation(normalForm);
-    }
-    Kind k = normalForm.getKind();
-
-    if(k != kind::CONST_BOOLEAN){
-      Assert(isRelationOperator(k));
-      TNode left  = normalForm[0];
-      TNode right = normalForm[1];
-      if(left.getKind() == PLUS){
-        //We may need to introduce a slack variable.
-        Assert(left.getNumChildren() >= 2);
-        Assert(isBasicSum(left));
-        Node slack;
-        if(!left.getAttribute(Slack(), slack)){
-          //TODO
-          TypeNode real_type = NodeManager::currentNM()->realType();
-          slack = NodeManager::currentNM()->mkVar(real_type);
-
-          left.setAttribute(Slack(), slack);
-          makeBasic(slack);
-
 
 
-          Node slackEqLeft = NodeManager::currentNM()->mkNode(EQUAL,slack,left);
-          slackEqLeft.setAttribute(TheoryArithPropagated(), true);
-          //TODO this has to be wrong no? YES (dejan)
-          // d_out->lemma(slackEqLeft);
-
-          Debug("slack") << "slack " << slackEqLeft << endl;
-
-          d_tableau.addRow(slackEqLeft);
-
-          setupVariable(slack);
-        }
+    TNode left  = n[0];
+    TNode right = n[1];
+    if(left.getKind() == PLUS){
+      //We may need to introduce a slack variable.
+      Assert(left.getNumChildren() >= 2);
+      Assert(isBasicSum(left));
+      if(!left.hasAttribute(Slack())){
+        setupSlack(left);
       }
     }
   }
@@ -180,7 +153,23 @@ void TheoryArith::preRegisterTerm(TNode n) {
                              << n << ")" << endl;
 }
 
+void TheoryArith::setupSlack(TNode left){
+  //TODO
+  TypeNode real_type = NodeManager::currentNM()->realType();
+  Node slack = NodeManager::currentNM()->mkVar(real_type);
+
+  left.setAttribute(Slack(), slack);
+  makeBasic(slack);
+
+  Node slackEqLeft = NodeManager::currentNM()->mkNode(EQUAL,slack,left);
+  slackEqLeft.setAttribute(TheoryArithPropagated(), true);
+
+  Debug("slack") << "slack " << slackEqLeft << endl;
 
+  d_tableau.addRow(slackEqLeft);
+
+  setupVariable(slack);
+}
 
 
 void TheoryArith::checkBasicVariable(TNode basic){
@@ -491,31 +480,13 @@ TNode TheoryArith::selectSlackAbove(TNode x_i){ // beta(x_i) > u_i
 Node TheoryArith::updateInconsistentVars(){ //corresponds to Check() in dM06
   Debug("arith") << "updateInconsistentVars" << endl;
 
-  d_partialModel.turnOnUnsafeMode();
-
   while(true){
-    if(debugTagIsOn("paranoid:check_tableau")){
-      checkTableau();
-    }
+    if(debugTagIsOn("paranoid:check_tableau")){ checkTableau(); }
 
     TNode x_i = selectSmallestInconsistentVar();
     Debug("arith_update") << "selectSmallestInconsistentVar()=" << x_i << endl;
     if(x_i == Node::null()){
       Debug("arith_update") << "No inconsistent variables" << endl;
-
-      if(debugTagIsOn("paranoid:check_tableau")){
-        checkTableau();
-      }
-
-      d_partialModel.commitAssignmentChanges();
-      d_partialModel.turnOffUnsafeMode();
-
-      if(debugTagIsOn("paranoid:check_tableau")){
-        checkTableau();
-      }
-
-
-
       return Node::null(); //sat
     }
     DeltaRational beta_i = d_partialModel.getAssignment(x_i);
@@ -524,21 +495,6 @@ Node TheoryArith::updateInconsistentVars(){ //corresponds to Check() in dM06
       DeltaRational l_i = d_partialModel.getLowerBound(x_i);
       TNode x_j = selectSlackBelow(x_i);
       if(x_j == TNode::null() ){
-        Debug("arith_update") << "conflict below" << endl;
-
-        if(debugTagIsOn("paranoid:check_tableau")){
-          checkTableau();
-        }
-
-        d_partialModel.revertAssignmentChanges();
-        d_partialModel.turnOffUnsafeMode();
-        //d_partialModel.stopRecordingAssignments(true);
-        //d_partialModel.beginRecordingAssignments();
-
-        if(debugTagIsOn("paranoid:check_tableau")){
-          checkTableau();
-        }
-
         return generateConflictBelow(x_i); //unsat
       }
       pivotAndUpdate(x_i, x_j, l_i);
@@ -547,20 +503,6 @@ Node TheoryArith::updateInconsistentVars(){ //corresponds to Check() in dM06
       DeltaRational u_i = d_partialModel.getUpperBound(x_i);
       TNode x_j = selectSlackAbove(x_i);
       if(x_j == TNode::null() ){
-        Debug("arith_update") << "conflict above" << endl;
-
-        if(debugTagIsOn("paranoid:check_tableau")){
-          checkTableau();
-        }
-
-        d_partialModel.revertAssignmentChanges();
-        d_partialModel.turnOffUnsafeMode();
-        //d_partialModel.stopRecordingAssignments(true);
-        //d_partialModel.beginRecordingAssignments();
-
-        if(debugTagIsOn("paranoid:check_tableau")){
-          checkTableau();
-        }
         return generateConflictAbove(x_i); //unsat
       }
       pivotAndUpdate(x_i, x_j, u_i);
@@ -592,12 +534,14 @@ Node TheoryArith::generateConflictAbove(TNode conflictVar){
     if(a_ij < d_constants.d_ZERO){
       bound =  d_partialModel.getUpperConstraint(nonbasic);
       Debug("arith") << "below 0 " << nonbasic << " "
-                     << d_partialModel.getAssignment(nonbasic) << " " << bound << endl;
+                     << d_partialModel.getAssignment(nonbasic)
+                     << " " << bound << endl;
       nb << bound;
     }else{
       bound =  d_partialModel.getLowerConstraint(nonbasic);
       Debug("arith") << " above 0 " << nonbasic << " "
-                     << d_partialModel.getAssignment(nonbasic) << " " << bound << endl;
+                     << d_partialModel.getAssignment(nonbasic)
+                     << " " << bound << endl;
       nb << bound;
     }
   }
@@ -628,13 +572,15 @@ Node TheoryArith::generateConflictBelow(TNode conflictVar){
     if(a_ij < d_constants.d_ZERO){
       TNode bound = d_partialModel.getLowerConstraint(nonbasic);
       Debug("arith") << "Lower "<< nonbasic << " "
-                     << d_partialModel.getAssignment(nonbasic) << " "<< bound << endl;
+                     << d_partialModel.getAssignment(nonbasic) << " "
+                     << bound << endl;
 
       nb << bound;
     }else{
       TNode bound = d_partialModel.getUpperConstraint(nonbasic);
       Debug("arith") << "Upper "<< nonbasic << " "
-                     << d_partialModel.getAssignment(nonbasic) << " "<< bound << endl;
+                     << d_partialModel.getAssignment(nonbasic) << " "
+                     << bound << endl;
 
       nb << bound;
     }
@@ -655,37 +601,17 @@ Node TheoryArith::simulatePreprocessing(TNode n){
     }
   }else{
     Assert(isNormalAtom(n));
-    Node rewritten = n;
-    Kind k = rewritten.getKind();
-
-//  if(rewritten.getKind() == NOT){
-//       Node sub = simulatePreprocessing(rewritten[0]);
-//       if(sub.getKind() == NOT){
-//         return sub[0];
-//       }else{
-//         return NodeManager::currentNM()->mkNode(NOT,sub);
-//       }
-//     } else 
-    if(!isRelationOperator(k)){
-      if(rewritten.getKind() == CONST_BOOLEAN){
-        Warning() << "How did I get a const boolean here" << endl;
-        Warning() << "offending node has id " << n.getId() << endl;
-        Warning() << "offending node is "<< n << endl;
-        return rewritten;
-      }else{
-        Unreachable("Unexpected type!");
-      }
-    }else if(rewritten[0].getMetaKind() == metakind::VARIABLE){
-      return rewritten;
+    Kind k = n.getKind();
+
+    Assert(isRelationOperator(k));
+    if(n[0].getMetaKind() == metakind::VARIABLE){
+      return n;
     }else {
-      TNode left = rewritten[0];
-      TNode right = rewritten[1];
-      Node slack;
-      if(!left.getAttribute(Slack(), slack)){
-        Unreachable("Slack must be have been created!");
-      }else{
-        return NodeManager::currentNM()->mkNode(k,slack,right);
-      }
+      TNode left = n[0];
+      TNode right = n[1];
+      Assert(left.hasAttribute(Slack()));
+      Node slack = left.getAttribute(Slack());
+      return NodeManager::currentNM()->mkNode(k,slack,right);
     }
   }
 }
@@ -693,6 +619,7 @@ Node TheoryArith::simulatePreprocessing(TNode n){
 void TheoryArith::check(Effort level){
   Debug("arith") << "TheoryArith::check begun" << std::endl;
 
+
   bool conflictDuringAnAssert = false;
 
   while(!done()){
@@ -705,17 +632,14 @@ void TheoryArith::check(Effort level){
     d_preprocessed.push_back(assertion);
 
     switch(assertion.getKind()){
-    case CONST_BOOLEAN:
-      Warning() << "No bools should be reached dagnabbit" << endl;
-      break;
     case LEQ:
-      conflictDuringAnAssert = AssertUpper(assertion, original);
+      conflictDuringAnAssert |= AssertUpper(assertion, original);
       break;
     case GEQ:
-      conflictDuringAnAssert = AssertLower(assertion, original);
+      conflictDuringAnAssert |= AssertLower(assertion, original);
       break;
     case EQUAL:
-      conflictDuringAnAssert = AssertUpper(assertion, original);
+      conflictDuringAnAssert |= AssertUpper(assertion, original);
       conflictDuringAnAssert |= AssertLower(assertion, original);
       break;
     case NOT:
@@ -725,21 +649,18 @@ void TheoryArith::check(Effort level){
         case LEQ: //(not (LEQ x c)) <=> (GT x c)
           {
             Node pushedin = pushInNegation(assertion);
-            conflictDuringAnAssert = AssertLower(pushedin,original);
+            conflictDuringAnAssert |= AssertLower(pushedin,original);
             break;
           }
         case GEQ: //(not (GEQ x c) <=> (LT x c)
           {
             Node pushedin = pushInNegation(assertion);
-            conflictDuringAnAssert = AssertUpper(pushedin,original);
+            conflictDuringAnAssert |= AssertUpper(pushedin,original);
             break;
           }
         case EQUAL:
           d_diseq.push_back(assertion);
           break;
-        case CONST_BOOLEAN:
-          Warning() << "No bools should be reached dagnabbit" << endl;
-          break;
         default:
           Unhandled();
         }
@@ -750,10 +671,10 @@ void TheoryArith::check(Effort level){
     }
   }
   if(conflictDuringAnAssert){
-    //clear the queue;
-    while(!done()) {
-      get();
-    }
+    if(debugTagIsOn("paranoid:check_tableau")){ checkTableau(); }
+    d_partialModel.revertAssignmentChanges();
+    if(debugTagIsOn("paranoid:check_tableau")){ checkTableau(); }
+
     //return
     return;
   }
@@ -761,10 +682,24 @@ void TheoryArith::check(Effort level){
   if(fullEffort(level)){
     Node possibleConflict = updateInconsistentVars();
     if(possibleConflict != Node::null()){
+      if(debugTagIsOn("paranoid:check_tableau")){ checkTableau(); }
+
+      d_partialModel.revertAssignmentChanges();
+
+      if(debugTagIsOn("paranoid:check_tableau")){ checkTableau(); }
+
+      d_out->conflict(possibleConflict, true);
+
+
       Debug("arith_conflict") << "Found a conflict "
                               << possibleConflict << endl;
-      d_out->conflict(possibleConflict);
     }else{
+      if(debugTagIsOn("paranoid:check_tableau")){ checkTableau(); }
+
+      d_partialModel.commitAssignmentChanges();
+
+      if(debugTagIsOn("paranoid:check_tableau")){ checkTableau(); }
+
       Debug("arith_conflict") << "No conflict found" << endl;
     }
   }

diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index cdd73782e415391bc9243bfa8423c0582eedb4e5..e54f273e9e680e68de8cae7fc88d491eb9089e6a 100644 (file)
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -97,12 +97,16 @@ private:
   Node generateConflictBelow(TNode conflictVar);
 
   void setupVariable(TNode x);
+  void setupSlack(TNode left);
+
   DeltaRational computeRowValueUsingAssignment(TNode x);
   DeltaRational computeRowValueUsingSavedAssignment(TNode x);
   void checkTableau();
 
   void checkBasicVariable(TNode basic);
 
+
+
   //TODO get rid of this!
   Node simulatePreprocessing(TNode n);