1 files changed, 46 insertions, 2 deletions

diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index 392d04f6c..cf3aeafee 100644
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -371,6 +371,10 @@ void ConstraintValue::setAssertedToTheTheory(TNode witness) {
   d_database->pushAssertionOrderWatch(this, witness);
 }
 
+// bool ConstraintValue::isPsuedoConstraint() const {
+//   return d_proof == d_database->d_psuedoConstraintProof;
+// }
+
 bool ConstraintValue::isSelfExplaining() const {
   return d_proof == d_database->d_selfExplainingProof;
 }
@@ -481,6 +485,9 @@ ConstraintDatabase::ConstraintDatabase(context::Context* satContext, context::Co
 
   d_equalityEngineProof = d_proofs.size();
   d_proofs.push_back(NullConstraint);
+
+  // d_psuedoConstraintProof = d_proofs.size();
+  // d_proofs.push_back(NullConstraint);
 }
 
 Constraint ConstraintDatabase::getConstraint(ArithVar v, ConstraintType t, const DeltaRational& r){
@@ -566,8 +573,32 @@ ConstraintDatabase::Statistics::~Statistics(){
 }
 
 void ConstraintDatabase::addVariable(ArithVar v){
-  Assert(v == d_varDatabases.size());
-  d_varDatabases.push_back(new PerVariableDatabase(v));
+  if(d_reclaimable.isMember(v)){
+    SortedConstraintMap& scm = getVariableSCM(v);
+
+    std::vector<Constraint> constraintList;
+
+    for(SortedConstraintMapIterator i = scm.begin(), end = scm.end(); i != end; ++i){
+      (i->second).push_into(constraintList);
+    }
+    while(!constraintList.empty()){
+      Constraint c = constraintList.back();
+      constraintList.pop_back();
+      Assert(c->safeToGarbageCollect());
+      delete c;
+    }
+    Assert(scm.empty());
+
+    d_reclaimable.remove(v);
+  }else{
+    Assert(v == d_varDatabases.size());
+    d_varDatabases.push_back(new PerVariableDatabase(v));
+  }
+}
+
+void ConstraintDatabase::removeVariable(ArithVar v){
+  Assert(!d_reclaimable.isMember(v));
+  d_reclaimable.add(v);
 }
 
 bool ConstraintValue::safeToGarbageCollect() const{
@@ -802,6 +833,13 @@ void ConstraintValue::impliedBy(const std::vector<Constraint>& b){
   }
 }
 
+// void ConstraintValue::setPsuedoConstraint(){
+//   Assert(truthIsUnknown());
+//   Assert(!hasLiteral());
+
+//   d_database->pushProofWatch(this, d_database->d_psuedoConstraintProof);
+// }
+
 void ConstraintValue::setEqualityEngineProof(){
   Assert(truthIsUnknown());
   Assert(hasLiteral());
@@ -818,6 +856,7 @@ void ConstraintValue::markAsTrue(){
 void ConstraintValue::markAsTrue(Constraint imp){
   Assert(truthIsUnknown());
   Assert(imp->hasProof());
+  //Assert(!imp->isPsuedoConstraint());
 
   d_database->d_proofs.push_back(NullConstraint);
   d_database->d_proofs.push_back(imp);
@@ -829,6 +868,8 @@ void ConstraintValue::markAsTrue(Constraint impA, Constraint impB){
   Assert(truthIsUnknown());
   Assert(impA->hasProof());
   Assert(impB->hasProof());
+  //Assert(!impA->isPsuedoConstraint());
+  //Assert(!impB->isPsuedoConstraint());
 
   d_database->d_proofs.push_back(NullConstraint);
   d_database->d_proofs.push_back(impA);
@@ -845,6 +886,7 @@ void ConstraintValue::markAsTrue(const vector<Constraint>& a){
   for(vector<Constraint>::const_iterator i = a.begin(), end = a.end(); i != end; ++i){
     Constraint c_i = *i;
     Assert(c_i->hasProof());
+    //Assert(!c_i->isPsuedoConstraint());
     d_database->d_proofs.push_back(c_i);
   }
 
@@ -861,6 +903,7 @@ SortedConstraintMap& ConstraintValue::constraintSet() const{
 bool ConstraintValue::proofIsEmpty() const{
   Assert(hasProof());
   bool result = d_database->d_proofs[d_proof] == NullConstraint;
+  //Assert((!result) || isSelfExplaining() || hasEqualityEngineProof() || isPsuedoConstraint());
   Assert((!result) || isSelfExplaining() || hasEqualityEngineProof());
   return result;
 }
@@ -869,6 +912,7 @@ void ConstraintValue::explainBefore(NodeBuilder<>& nb, AssertionOrder order) con
   Assert(hasProof());
   Assert(!isSelfExplaining() || assertedToTheTheory());
 
+
   if(assertedBefore(order)){
     nb << getWitness();
   }else if(hasEqualityEngineProof()){