Changed how assignments are saved during check. These are now backed by an attribute. There is now a priority queue for selecting the smallest inconsistent basic variable. normal.h has been removed. A large chunk of the registerTerm() stuff has been moved into preregister. The lazy splitting code is now been commented out so that it stops showing up in profiling.

6 files changed, 271 insertions, 234 deletions

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index 19980cd20..5c2a1e996 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -20,7 +20,6 @@
 
 #include "theory/arith/arith_rewriter.h"
 #include "theory/arith/arith_utilities.h"
-#include "theory/arith/normal.h"
 
 #include <vector>
 #include <set>
@@ -542,10 +541,6 @@ Kind multKind(Kind k, int sgn){
 Node ArithRewriter::rewrite(TNode n){
   Debug("arithrewriter") << "Trace rewrite:" << n << std::endl;
 
-  if(n.getAttribute(IsNormal())){
-    return n;
-  }
-
   Node res;
 
   if(isRelationOperator(n.getKind())){
@@ -554,11 +549,6 @@ Node ArithRewriter::rewrite(TNode n){
     res = rewriteTerm(n);
   }
 
-  if(n == res){
-    n.setAttribute(NormalForm(), Node::null());
-  }else{
-    n.setAttribute(NormalForm(), res);
-  }
   Debug("arithrewriter") << "Trace rewrite:" << n << "|->"<< res << std::endl;
 
   return res;
diff --git a/src/theory/arith/normal.h b/src/theory/arith/normal.h
deleted file mode 100644
index 12b2a5e71..000000000
--- a/src/theory/arith/normal.h
+++ /dev/null
@@ -1,48 +0,0 @@
-/*********************                                                        */
-/*! \file normal.h
- ** \verbatim
- ** Original author: taking
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-
-#ifndef __CVC4__THEORY__ARITH__NORMAL_H
-#define __CVC4__THEORY__ARITH__NORMAL_H
-
-namespace CVC4 {
-namespace theory {
-namespace arith {
-
-struct IsNormalAttrID;
-
-typedef expr::Attribute<IsNormalAttrID, bool> IsNormal;
-
-
-inline bool isNormalized(TNode x){
-  return x.getAttribute(IsNormal());
-}
-
-struct NormalFormAttrID;
-
-typedef expr::Attribute<IsNormalAttrID, Node> NormalForm;
-
-
-
-}; /* namespace arith */
-}; /* namespace theory */
-}; /* namespace CVC4 */
-
-
-#endif /* __CVC4__THEORY__ARITH__NORMAL_H */
diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp
index 2d65f0640..d4be75559 100644
--- a/src/theory/arith/partial_model.cpp
+++ b/src/theory/arith/partial_model.cpp
@@ -45,15 +45,21 @@ void ArithPartialModel::setLowerBound(TNode x, const DeltaRational& r){
 void ArithPartialModel::setAssignment(TNode x, const DeltaRational& r){
   Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
 
-  if(d_savingAssignments){
-    DeltaRational current = getAssignment(x);
-    d_history.push_back(make_pair(x,current));
-  }
-
   Assert(x.hasAttribute(partial_model::Assignment()));
 
-  DeltaRational* c = x.getAttribute(partial_model::Assignment());
-  *c = r;
+  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);
+    }
+  }
+
+  *curr = r;
   Debug("partial_model") << "pm: updating the assignment to" << x
                          << " now " << r <<endl;
 }
@@ -61,10 +67,12 @@ void ArithPartialModel::setAssignment(TNode x, const DeltaRational& r){
 void ArithPartialModel::initialize(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* c = new DeltaRational(r);
    x.setAttribute(partial_model::Assignment(), c);
+   x.setAttribute(partial_model::SafeAssignment(), NULL);
 
    Debug("partial_model") << "pm: constructing an assignment for " << x
                           << " initially " << (*c) <<endl;
@@ -89,8 +97,19 @@ DeltaRational ArithPartialModel::getLowerBound(TNode x) const{
   return DeltaRational((*i).second);
 }
 
+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;
+    }
+  }
+  return getAssignment(x);
+}
 
-DeltaRational ArithPartialModel::getAssignment(TNode x) const{
+const DeltaRational& ArithPartialModel::getAssignment(TNode x) const{
   Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
 
   DeltaRational* assign;
@@ -98,18 +117,6 @@ DeltaRational ArithPartialModel::getAssignment(TNode x) const{
   return *assign;
 }
 
-DeltaRational ArithPartialModel::getSavedAssignment(TNode x) const{
-  Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
-  if(d_savingAssignments){
-    for(HistoryStack::const_iterator i = d_history.begin(); i != d_history.end(); ++i){
-      pair<TNode, DeltaRational> curr = *i;
-      if(curr.first == x){
-        return DeltaRational(curr.second);
-      }
-    }
-  }
-  return getAssignment(x);
-}
 
 
 void ArithPartialModel::setLowerConstraint(TNode x, TNode constraint){
@@ -163,7 +170,7 @@ TNode ArithPartialModel::getUpperConstraint(TNode x){
 // }
 
 
-bool ArithPartialModel::belowLowerBound(TNode x, DeltaRational& c, bool strict){
+bool ArithPartialModel::belowLowerBound(TNode x, const DeltaRational& c, bool strict){
   CDDRationalMap::iterator i = d_LowerBoundMap.find(x);
   if(i == d_LowerBoundMap.end()){
     // l = -\intfy
@@ -180,7 +187,7 @@ bool ArithPartialModel::belowLowerBound(TNode x, DeltaRational& c, bool strict){
   }
 }
 
-bool ArithPartialModel::aboveUpperBound(TNode x, DeltaRational& c, bool strict){
+bool ArithPartialModel::aboveUpperBound(TNode x, const DeltaRational& c, bool strict){
   CDDRationalMap::iterator i = d_UpperBoundMap.find(x);
   if(i == d_UpperBoundMap.end()){
     // u = -\intfy
@@ -222,7 +229,7 @@ bool ArithPartialModel::strictlyAboveLowerBound(TNode x){
 }
 
 bool ArithPartialModel::assignmentIsConsistent(TNode x){
-  DeltaRational beta = getAssignment(x);
+  const DeltaRational& beta = getAssignment(x);
 
   bool above_li = !belowLowerBound(x,beta,true);
   bool below_ui = !aboveUpperBound(x,beta,true);
@@ -231,32 +238,50 @@ bool ArithPartialModel::assignmentIsConsistent(TNode x){
   return  above_li && below_ui;
 }
 
-void ArithPartialModel::beginRecordingAssignments(){
-  Assert(!d_savingAssignments);
+void ArithPartialModel::turnOnUnsafeMode(){
+  Assert(!d_unsafeMode);
   Assert(d_history.empty());
 
-  d_savingAssignments = true;
+  d_unsafeMode = true;
 }
 
+void ArithPartialModel::turnOffUnsafeMode(){
+  Assert(d_unsafeMode);
+  Assert(d_history.empty());
+
+  d_unsafeMode = false;
+}
 
-void ArithPartialModel::stopRecordingAssignments(bool revert){
-  Assert(d_savingAssignments);
+void ArithPartialModel::clearSafeAssignments(bool revert){
+  Assert(d_unsafeMode);
 
-  d_savingAssignments = false; //
+  for(HistoryList::iterator i = d_history.begin(); i != d_history.end(); ++i){
+    TNode x = *i;
 
-  if(revert){
-    while(!d_history.empty()){
-      pair<TNode, DeltaRational>& curr = d_history.back();
+    Assert(x.hasAttribute(partial_model::SafeAssignment()));
 
-      setAssignment(curr.first,curr.second);
+    DeltaRational* safeAssignment = x.getAttribute(partial_model::SafeAssignment());
 
-      d_history.pop_back();
+    if(revert){
+      Assert(x.hasAttribute(partial_model::Assignment()));
+
+      DeltaRational* assign = x.getAttribute(partial_model::Assignment());
+      *assign = *safeAssignment;
     }
-  }else{
-    d_history.clear();
+    x.setAttribute(partial_model::SafeAssignment(), NULL);
+    delete safeAssignment;
   }
 
+  d_history.clear();
+}
+
+void ArithPartialModel::revertAssignmentChanges(){
+  clearSafeAssignments(true);
+}
+void ArithPartialModel::commitAssignmentChanges(){
+  clearSafeAssignments(false);
 }
+
 void ArithPartialModel::printModel(TNode x){
 
   Debug("model") << "model" << x << ":"<< getAssignment(x) << " ";
diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h
index 36567e86e..d04d8dd8c 100644
--- a/src/theory/arith/partial_model.h
+++ b/src/theory/arith/partial_model.h
@@ -37,7 +37,9 @@ namespace partial_model {
 struct DeltaRationalCleanupStrategy{
   static void cleanup(DeltaRational* dq){
     Debug("arithgc") << "cleaning up  " << dq << "\n";
-    delete dq;
+    if(dq != NULL){
+      delete dq;
+    }
   }
 };
 
@@ -46,6 +48,12 @@ typedef expr::Attribute<AssignmentAttrID,
                         DeltaRational*,
                         DeltaRationalCleanupStrategy> Assignment;
 
+
+struct SafeAssignmentAttrID {};
+typedef expr::Attribute<SafeAssignmentAttrID,
+                        DeltaRational*,
+                        DeltaRationalCleanupStrategy> SafeAssignment;
+
 /**
  * This defines a context dependent delta rational map.
  * This is used to keep track of the current lower and upper bounds on
@@ -108,12 +116,11 @@ private:
   partial_model::CDDRationalMap d_LowerBoundMap;
   partial_model::CDDRationalMap d_UpperBoundMap;
 
-  typedef std::pair<TNode, DeltaRational> HistoryPair;
-  typedef std::deque< HistoryPair > HistoryStack;
 
-  HistoryStack d_history;
+  typedef std::vector<TNode> HistoryList;
+  HistoryList d_history;
 
-  bool d_savingAssignments;
+  bool d_unsafeMode;
 
 public:
 
@@ -121,7 +128,7 @@ public:
     d_LowerBoundMap(c),
     d_UpperBoundMap(c),
     d_history(),
-    d_savingAssignments(false)
+    d_unsafeMode(false)
   { }
 
   void setLowerConstraint(TNode x, TNode constraint);
@@ -130,11 +137,21 @@ public:
   TNode getUpperConstraint(TNode x);
 
 
-  void beginRecordingAssignments();
 
-  /* */
-  void stopRecordingAssignments(bool revert);
-  bool isRecording() { return d_savingAssignments;  }
+  void initialize(TNode x, const DeltaRational& r);
+
+  DeltaRational getSafeAssignment(TNode x) const;
+
+  bool isInUnsafeMode() { return d_unsafeMode;  }
+
+  void turnOnUnsafeMode();
+  void turnOffUnsafeMode();
+
+  void revertAssignmentChanges();
+  void commitAssignmentChanges();
+
+
+
 
   void setUpperBound(TNode x, const DeltaRational& r);
   void setLowerBound(TNode x, const DeltaRational& r);
@@ -143,20 +160,20 @@ public:
   /** Must know that the bound exists before calling this! */
   DeltaRational getUpperBound(TNode x) const;
   DeltaRational getLowerBound(TNode x) const;
-  DeltaRational getAssignment(TNode x) const;
+  const DeltaRational& getAssignment(TNode x) const;
 
 
   /**
    * x <= l
    * ? c < l
    */
-  bool belowLowerBound(TNode x, DeltaRational& c, bool strict);
+  bool belowLowerBound(TNode x, const DeltaRational& c, bool strict);
 
   /**
    * x <= u
    * ? c < u
    */
-  bool aboveUpperBound(TNode x, DeltaRational& c, bool strict);
+  bool aboveUpperBound(TNode x, const DeltaRational& c, bool strict);
 
   bool strictlyBelowUpperBound(TNode x);
   bool strictlyAboveLowerBound(TNode x);
@@ -164,10 +181,8 @@ public:
 
   void printModel(TNode x);
 
-  void initialize(TNode x, const DeltaRational& r);
-  
-  DeltaRational getSavedAssignment(TNode x) const;
-
+private:
+  void clearSafeAssignments(bool revert);
 };
 
 
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index e99a3e823..92781e0ba 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -30,7 +30,7 @@
 #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/normal.h"
 #include "theory/arith/slack.h"
 #include "theory/arith/basic.h"
 
@@ -63,7 +63,6 @@ TheoryArith::TheoryArith(context::Context* c, OutputChannel& out) :
   uint64_t ass_id = partial_model::Assignment::getId();
   Debug("arithsetup") << "Assignment: " << ass_id << std::endl;
 
-  d_partialModel.beginRecordingAssignments();
 }
 TheoryArith::~TheoryArith(){
   for(vector<Node>::iterator i=d_variables.begin(); i!= d_variables.end(); ++i){
@@ -72,6 +71,40 @@ TheoryArith::~TheoryArith(){
   }
 }
 
+bool isBasicSum(TNode n){
+  if(n.getKind() != kind::PLUS) return false;
+
+  for(TNode::const_iterator i=n.begin(); i!=n.end(); ++i){
+    TNode child = *i;
+    if(child.getKind() != MULT) return false;
+    if(child[0].getKind() != CONST_RATIONAL) return false;
+    for(unsigned j=1; j<child.getNumChildren(); ++j){
+      TNode var = child[j];
+      if(var.getMetaKind() != metakind::VARIABLE) return false;
+    }
+  }
+  return true;
+}
+
+bool isNormalAtom(TNode n){
+  
+  if(!(n.getKind() == LEQ|| n.getKind() == GEQ || n.getKind() == EQUAL)){
+    return false;
+  }
+  TNode left = n[0];
+  TNode right = n[1];
+  if(right.getKind() != CONST_RATIONAL){
+    return false;
+  }
+  if(left.getMetaKind() == metakind::VARIABLE){
+    return true;
+  }else if(isBasicSum(left)){
+    return true;
+  }else{
+    return false;
+  }
+
+}
 void TheoryArith::preRegisterTerm(TNode n) {
   Debug("arith_preregister") << "arith: begin TheoryArith::preRegisterTerm("
                              << n << ")" << endl;
@@ -98,31 +131,63 @@ void TheoryArith::preRegisterTerm(TNode n) {
     setupVariable(n);
   }
 
-  Debug("arith_preregister") << "arith: end TheoryArith::preRegisterTerm("
-                             << n << ")" << endl;
-}
+  //TODO is an atom
+  if(isRelationOperator(n.getKind())){
 
-bool isBasicSum(TNode n){
-  if(n.getKind() != kind::PLUS) return false;
+    Assert(isNormalAtom(n));
+    Node normalForm(n);
 
-  for(TNode::const_iterator i=n.begin(); i!=n.end(); ++i){
-    TNode child = *i;
-    if(child.getKind() != MULT) return false;
-    if(child[0].getKind() != CONST_RATIONAL) return false;
-    for(unsigned j=1; j<child.getNumChildren(); ++j){
-      TNode var = child[j];
-      if(var.getMetaKind() != metakind::VARIABLE) return false;
+    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);
+        }
+      }
     }
   }
-  return true;
+
+  Debug("arith_preregister") << "arith: end TheoryArith::preRegisterTerm("
+                             << n << ")" << endl;
 }
 
 
 
-void registerAtom(TNode rel){
-  //addBound(rel);
-  //Anything else?
 
+void TheoryArith::checkBasicVariable(TNode basic){
+  Assert(isBasic(basic));
+  if(!d_partialModel.assignmentIsConsistent(basic)){
+    d_possiblyInconsistent.push(basic);
+  }
 }
 
 /* Requirements:
@@ -153,6 +218,8 @@ void TheoryArith::setupVariable(TNode x){
       Debug("arith_setup") << "setup("<<x<< " " <<q<<")"<<std::endl;
     }
     d_partialModel.setAssignment(x,q);
+
+    checkBasicVariable(x);
   }
   Debug("arithgc") << "setupVariable("<<x<<")"<<std::endl;
 };
@@ -185,7 +252,7 @@ DeltaRational TheoryArith::computeRowValueUsingSavedAssignment(TNode x){
   for(std::set<TNode>::iterator i = row->begin(); i != row->end();++i){
     TNode nonbasic = *i;
     Rational& coeff = row->lookup(nonbasic);
-    DeltaRational assignment = d_partialModel.getSavedAssignment(nonbasic);
+    DeltaRational assignment = d_partialModel.getSafeAssignment(nonbasic);
     sum = sum + (assignment * coeff);
   }
   return sum;
@@ -208,56 +275,6 @@ void TheoryArith::registerTerm(TNode tn){
   if(tn.getKind() == kind::BUILTIN) return;
 
 
-  //TODO is an atom
-  if(isRelationOperator(tn.getKind())){
-
-    Node normalForm = (isNormalized(tn)) ? Node(tn) : rewrite(tn);
-    normalForm = (normalForm.getKind() == NOT) ? pushInNegation(normalForm):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);
-
-          Node rewritten = NodeManager::currentNM()->mkNode(k,slack,right);
-          registerAtom(rewritten);
-        }else{
-          Node rewritten = NodeManager::currentNM()->mkNode(k,slack,right);
-          registerAtom(rewritten);
-        }
-      }else{
-        Assert(left.getMetaKind() == metakind::VARIABLE);
-        Assert(right.getKind() == CONST_RATIONAL);
-        registerAtom(normalForm);
-      }
-    }
-  }
 }
 
 /* procedure AssertUpper( x_i <= c_i) */
@@ -288,6 +305,8 @@ bool TheoryArith::AssertUpper(TNode n, TNode original){
     if(d_partialModel.getAssignment(x_i) > c_i){
       update(x_i, c_i);
     }
+  }else{
+    checkBasicVariable(x_i);
   }
   d_partialModel.printModel(x_i);
   return false;
@@ -319,6 +338,8 @@ bool TheoryArith::AssertLower(TNode n, TNode original){
     if(d_partialModel.getAssignment(x_i) < c_i){
       update(x_i, c_i);
     }
+  }else{
+    checkBasicVariable(x_i);
   }
   //d_partialModel.printModel(x_i);
 
@@ -326,7 +347,7 @@ bool TheoryArith::AssertLower(TNode n, TNode original){
 }
 
 void TheoryArith::update(TNode x_i, DeltaRational& v){
-
+  Assert(!isBasic(x_i));
   DeltaRational assignment_x_i = d_partialModel.getAssignment(x_i);
 
   Debug("arith") <<"update " << x_i << ": "
@@ -345,6 +366,7 @@ void TheoryArith::update(TNode x_i, DeltaRational& v){
       DeltaRational assignment = d_partialModel.getAssignment(x_j);
       DeltaRational  nAssignment = assignment+(diff * a_ji);
       d_partialModel.setAssignment(x_j, nAssignment);
+      checkBasicVariable(x_j);
     }
   }
 
@@ -383,25 +405,45 @@ void TheoryArith::pivotAndUpdate(TNode x_i, TNode x_j, DeltaRational& v){
       Rational a_kj = row_k->lookup(x_j);
       DeltaRational nextAssignment = d_partialModel.getAssignment(x_k) + (theta * a_kj);
       d_partialModel.setAssignment(x_k, nextAssignment);
+      checkBasicVariable(x_k);
     }
   }
 
   d_tableau.pivot(x_i, x_j);
 
+  checkBasicVariable(x_j);
+
   if(debugTagIsOn("tableau")){
     d_tableau.printTableau();
   }
 }
 
 TNode TheoryArith::selectSmallestInconsistentVar(){
+  Debug("arith_update") << "selectSmallestInconsistentVar()" << endl;
+  Debug("arith_update") << "possiblyInconsistent.size()"
+                        << d_possiblyInconsistent.size() << endl;
+
+  while(!d_possiblyInconsistent.empty()){
+    TNode var = d_possiblyInconsistent.top();
+    Debug("arith_update") << "possiblyInconsistent var" << var << endl;
+    if(isBasic(var)){
+      if(!d_partialModel.assignmentIsConsistent(var)){
+        return var;
+      }
+    }
+    d_possiblyInconsistent.pop();
+  }
 
-  for(Tableau::VarSet::iterator basicIter = d_tableau.begin();
-      basicIter != d_tableau.end();
-      ++basicIter){
+  if(debugTagIsOn("paranoid:variables")){
+    for(Tableau::VarSet::iterator basicIter = d_tableau.begin();
+        basicIter != d_tableau.end();
+        ++basicIter){
 
-    TNode basic = *basicIter;
-    if(!d_partialModel.assignmentIsConsistent(basic)){
-      return basic;
+      TNode basic = *basicIter;
+      Assert(d_partialModel.assignmentIsConsistent(basic));
+      if(!d_partialModel.assignmentIsConsistent(basic)){
+        return basic;
+      }
     }
   }
 
@@ -449,6 +491,7 @@ 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")){
@@ -464,8 +507,8 @@ Node TheoryArith::updateInconsistentVars(){ //corresponds to Check() in dM06
         checkTableau();
       }
 
-      d_partialModel.stopRecordingAssignments(false);
-      d_partialModel.beginRecordingAssignments();
+      d_partialModel.commitAssignmentChanges();
+      d_partialModel.turnOffUnsafeMode();
 
       if(debugTagIsOn("paranoid:check_tableau")){
         checkTableau();
@@ -487,8 +530,10 @@ Node TheoryArith::updateInconsistentVars(){ //corresponds to Check() in dM06
           checkTableau();
         }
 
-        d_partialModel.stopRecordingAssignments(true);
-        d_partialModel.beginRecordingAssignments();
+        d_partialModel.revertAssignmentChanges();
+        d_partialModel.turnOffUnsafeMode();
+        //d_partialModel.stopRecordingAssignments(true);
+        //d_partialModel.beginRecordingAssignments();
 
         if(debugTagIsOn("paranoid:check_tableau")){
           checkTableau();
@@ -508,8 +553,10 @@ Node TheoryArith::updateInconsistentVars(){ //corresponds to Check() in dM06
           checkTableau();
         }
 
-        d_partialModel.stopRecordingAssignments(true);
-        d_partialModel.beginRecordingAssignments();
+        d_partialModel.revertAssignmentChanges();
+        d_partialModel.turnOffUnsafeMode();
+        //d_partialModel.stopRecordingAssignments(true);
+        //d_partialModel.beginRecordingAssignments();
 
         if(debugTagIsOn("paranoid:check_tableau")){
           checkTableau();
@@ -596,6 +643,7 @@ Node TheoryArith::generateConflictBelow(TNode conflictVar){
   return conflict;
 }
 
+
 //TODO get rid of this!
 Node TheoryArith::simulatePreprocessing(TNode n){
   if(n.getKind() == NOT){
@@ -606,17 +654,19 @@ Node TheoryArith::simulatePreprocessing(TNode n){
       return NodeManager::currentNM()->mkNode(NOT,sub);
     }
   }else{
-    Node rewritten = rewrite(n);
+    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() == 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;
@@ -719,37 +769,37 @@ void TheoryArith::check(Effort level){
     }
   }
 
-  if(fullEffort(level)){
-    bool enqueuedCaseSplit = false;
-    typedef context::CDList<Node>::const_iterator diseq_iterator;
-    for(diseq_iterator i = d_diseq.begin(); i!= d_diseq.end(); ++i){
-
-      Node assertion = *i;
-      Debug("arith") << "splitting"  << assertion << endl;
-      TNode eq = assertion[0];
-      TNode x_i = eq[0];
-      TNode c_i = eq[1];
-      DeltaRational constant =  c_i.getConst<Rational>();
-      Debug("arith") << "broken apart" << endl;
-      if(d_partialModel.getAssignment(x_i) == constant){
-        Debug("arith") << "here" << endl;
-        enqueuedCaseSplit = true;
-        Node lt = NodeManager::currentNM()->mkNode(LT,x_i,c_i);
-        Node gt = NodeManager::currentNM()->mkNode(GT,x_i,c_i);
-        Node caseSplit = NodeManager::currentNM()->mkNode(OR, eq, lt, gt);
-        //d_out->enqueueCaseSplits(caseSplit);
-        Debug("arith") << "finished" << caseSplit << endl;
-      }
-      Debug("arith") << "end of for loop" << endl;
-
-    }
-    Debug("arith") << "finished" << endl;
-
-    if(enqueuedCaseSplit){
-      //d_out->caseSplit();
-      //Warning() << "Outstanding case split in theory arith" << endl;
-    }
-  }
+  // if(fullEffort(level)){
+//     bool enqueuedCaseSplit = false;
+//     typedef context::CDList<Node>::const_iterator diseq_iterator;
+//     for(diseq_iterator i = d_diseq.begin(); i!= d_diseq.end(); ++i){
+
+//       Node assertion = *i;
+//       Debug("arith") << "splitting"  << assertion << endl;
+//       TNode eq = assertion[0];
+//       TNode x_i = eq[0];
+//       TNode c_i = eq[1];
+//       DeltaRational constant =  c_i.getConst<Rational>();
+//       Debug("arith") << "broken apart" << endl;
+//       if(d_partialModel.getAssignment(x_i) == constant){
+//         Debug("arith") << "here" << endl;
+//         enqueuedCaseSplit = true;
+//         Node lt = NodeManager::currentNM()->mkNode(LT,x_i,c_i);
+//         Node gt = NodeManager::currentNM()->mkNode(GT,x_i,c_i);
+//         Node caseSplit = NodeManager::currentNM()->mkNode(OR, eq, lt, gt);
+//         //d_out->enqueueCaseSplits(caseSplit);
+//         Debug("arith") << "finished" << caseSplit << endl;
+//       }
+//       Debug("arith") << "end of for loop" << endl;
+
+//     }
+//     Debug("arith") << "finished" << endl;
+
+//     if(enqueuedCaseSplit){
+//       //d_out->caseSplit();
+//       //Warning() << "Outstanding case split in theory arith" << endl;
+//     }
+//   }
 
   Debug("arith") << "TheoryArith::check end" << std::endl;
 
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index c6b555bf8..cdd73782e 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -32,6 +32,7 @@
 #include "theory/arith/partial_model.h"
 
 #include <vector>
+#include <queue>
 
 namespace CVC4 {
 namespace theory {
@@ -56,6 +57,8 @@ private:
   //This needs to come before d_partialModel and d_tableau in the file
 
 
+  std::priority_queue<Node> d_possiblyInconsistent;
+
   /* Chopping block ends */
   ArithConstants d_constants;
   ArithPartialModel d_partialModel;
@@ -98,6 +101,8 @@ private:
   DeltaRational computeRowValueUsingSavedAssignment(TNode x);
   void checkTableau();
 
+  void checkBasicVariable(TNode basic);
+
   //TODO get rid of this!
   Node simulatePreprocessing(TNode n);