Improved garbage collection for TheoryArith. The merges all of the code over from branches/arithmetic/converge except for the new code for simplex.

1 files changed, 110 insertions, 58 deletions

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index d2814348a..f036e20fd 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -62,6 +62,8 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputCha
   d_unknownsInARow(0),
   d_hasDoneWorkSinceCut(false),
   d_learner(u),
+  d_numberOfVariables(0),
+  d_pool(),
   d_setupLiteralCallback(this),
   d_assertionsThatDoNotMatchTheirLiterals(c),
   d_nextIntegerCheckVar(0),
@@ -79,6 +81,7 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputCha
   d_tableauResetPeriod(10),
   d_conflicts(c),
   d_raiseConflict(d_conflicts),
+  d_tempVarMalloc(*this),
   d_congruenceManager(c, d_constraintDatabase, d_setupLiteralCallback, d_arithvarNodeMap, d_raiseConflict),
   d_simplex(d_linEq, d_raiseConflict),
   d_constraintDatabase(c, u, d_arithvarNodeMap, d_congruenceManager, d_raiseConflict),
@@ -822,8 +825,9 @@ void TheoryArith::setupVariable(const Variable& x){
   Assert(!isSetup(n));
 
   ++(d_statistics.d_statUserVariables);
-  ArithVar varN = requestArithVar(n,false);
-  setupInitialValue(varN);
+  requestArithVar(n,false);
+  //ArithVar varN = requestArithVar(n,false);
+  //setupInitialValue(varN);
 
   markSetup(n);
 
@@ -860,8 +864,9 @@ void TheoryArith::setupVariableList(const VarList& vl){
     d_nlIncomplete = true;
 
     ++(d_statistics.d_statUserVariables);
-    ArithVar av = requestArithVar(vlNode, false);
-    setupInitialValue(av);
+    requestArithVar(vlNode, false);
+    //ArithVar av = requestArithVar(vlNode, false);
+    //setupInitialValue(av);
 
     markSetup(vlNode);
   }
@@ -1054,7 +1059,7 @@ void TheoryArith::setupPolynomial(const Polynomial& poly) {
 
     ArithVar varSlack = requestArithVar(polyNode, true);
     d_tableau.addRow(varSlack, coefficients, variables);
-    setupInitialValue(varSlack);
+    setupBasicValue(varSlack);
 
     //Add differences to the difference manager
     Polynomial::iterator i = poly.begin(), end = poly.end();
@@ -1125,6 +1130,14 @@ void TheoryArith::preRegisterTerm(TNode n) {
   Debug("arith::preregister") << "end arith::preRegisterTerm("<< n <<")" << endl;
 }
 
+void TheoryArith::releaseArithVar(ArithVar v){
+  Assert(d_arithvarNodeMap.hasNode(v));
+  
+  d_constraintDatabase.removeVariable(v);
+  d_arithvarNodeMap.remove(v);
+
+  d_pool.push_back(v);
+}
 
 ArithVar TheoryArith::requestArithVar(TNode x, bool slack){
   //TODO : The VarList trick is good enough?
@@ -1135,32 +1148,73 @@ ArithVar TheoryArith::requestArithVar(TNode x, bool slack){
   Assert(!d_arithvarNodeMap.hasArithVar(x));
   Assert(x.getType().isReal());// real or integer
 
-  ArithVar varX = d_variables.size();
-  d_variables.push_back(Node(x));
-  Debug("integers") << "isInteger[[" << x << "]]: " << x.getType().isInteger() << endl;
+  // ArithVar varX = d_variables.size();
+  // d_variables.push_back(Node(x));
+
+  bool reclaim = !d_pool.empty();
+  ArithVar varX;
+
+  if(reclaim){
+    varX = d_pool.back();
+    d_pool.pop_back();
+
+    d_partialModel.setAssignment(varX, d_DELTA_ZERO, d_DELTA_ZERO);
+  }else{
+    varX = d_numberOfVariables;
+    ++d_numberOfVariables;
+
+    d_slackVars.push_back(true);
+    d_variableTypes.push_back(ATReal);
 
+    d_simplex.increaseMax();
+
+    d_tableau.increaseSize();
+    d_tableauSizeHasBeenModified = true;
+
+    d_partialModel.initialize(varX, d_DELTA_ZERO);
+  }
+
+  ArithType type;
   if(slack){
     //The type computation is not quite accurate for Rationals that are integral.
     //We'll use the isIntegral check from the polynomial package instead.
     Polynomial p = Polynomial::parsePolynomial(x);
-    d_variableTypes.push_back(p.isIntegral() ? ATInteger : ATReal);
+    type = p.isIntegral() ? ATInteger : ATReal;
   }else{
-    d_variableTypes.push_back(nodeToArithType(x));
+    type = nodeToArithType(x);
   }
+  d_variableTypes[varX] = type;
+  d_slackVars[varX] = slack;
 
-  d_slackVars.push_back(slack);
-
-  d_simplex.increaseMax();
+  d_constraintDatabase.addVariable(varX);
 
   d_arithvarNodeMap.setArithVar(x,varX);
 
-  d_tableau.increaseSize();
-  d_tableauSizeHasBeenModified = true;
+  // Debug("integers") << "isInteger[[" << x << "]]: " << x.getType().isInteger() << endl;
 
-  d_constraintDatabase.addVariable(varX);
+  // if(slack){
+  //   //The type computation is not quite accurate for Rationals that are integral.
+  //   //We'll use the isIntegral check from the polynomial package instead.
+  //   Polynomial p = Polynomial::parsePolynomial(x);
+  //   d_variableTypes.push_back(p.isIntegral() ? ATInteger : ATReal);
+  // }else{
+  //   d_variableTypes.push_back(nodeToArithType(x));
+  // }
+
+  // d_slackVars.push_back(slack);
+
+  // d_simplex.increaseMax();
+
+  // d_tableau.increaseSize();
+  // d_tableauSizeHasBeenModified = true;
+
+  // d_constraintDatabase.addVariable(varX);
 
   Debug("arith::arithvar") << x << " |-> " << varX << endl;
 
+  Assert(!d_partialModel.hasUpperBound(varX));
+  Assert(!d_partialModel.hasLowerBound(varX));
+
   return varX;
 }
 
@@ -1179,18 +1233,7 @@ void TheoryArith::asVectors(const Polynomial& p, std::vector<Rational>& coeffs,
     Assert(theoryOf(n) != THEORY_ARITH || d_arithvarNodeMap.hasArithVar(n));
 
     Assert(d_arithvarNodeMap.hasArithVar(n));
-    ArithVar av;
-    // The first if is likely dead is likely dead code:
-    // if (theoryOf(n) != THEORY_ARITH && !d_arithvarNodeMap.hasArithVar(n)) {
-    //   // The only way not to get it through pre-register is if it's a foreign term
-    //   ++(d_statistics.d_statUserVariables);
-    //   av = requestArithVar(n,false);
-    //   setupInitialValue(av);
-    // } else {
-    //   // Otherwise, we already have it's variable
-    //   av = d_arithvarNodeMap.asArithVar(n);
-    // }
-    av = d_arithvarNodeMap.asArithVar(n);
+    ArithVar av = d_arithvarNodeMap.asArithVar(n);
 
     coeffs.push_back(constant.getValue());
     variables.push_back(av);
@@ -1200,11 +1243,12 @@ void TheoryArith::asVectors(const Polynomial& p, std::vector<Rational>& coeffs,
 /* Requirements:
  * For basic variables the row must have been added to the tableau.
  */
-void TheoryArith::setupInitialValue(ArithVar x){
+void TheoryArith::setupBasicValue(ArithVar x){
+  Assert(d_tableau.isBasic(x));
 
-  if(!d_tableau.isBasic(x)){
-    d_partialModel.initialize(x, d_DELTA_ZERO);
-  }else{
+  // if(!d_tableau.isBasic(x)){
+  //   d_partialModel.setAssignment(x, d_DELTA_ZERO, d_DELTA_ZERO);
+  // }else{
     //If the variable is basic, assertions may have already happened and updates
     //may have occured before setting this variable up.
 
@@ -1212,9 +1256,11 @@ void TheoryArith::setupInitialValue(ArithVar x){
     //time instead of register
     DeltaRational safeAssignment = d_linEq.computeRowValue(x, true);
     DeltaRational assignment = d_linEq.computeRowValue(x, false);
-    d_partialModel.initialize(x,safeAssignment);
-    d_partialModel.setAssignment(x,assignment);
-  }
+    //d_partialModel.initialize(x,safeAssignment);
+    //d_partialModel.setAssignment(x,assignment);
+    d_partialModel.setAssignment(x,safeAssignment,assignment);
+
+    //  }
   Debug("arith") << "setupVariable("<<x<<")"<<std::endl;
 }
 
@@ -1254,8 +1300,8 @@ Node TheoryArith::dioCutting(){
   context::Context::ScopedPush speculativePush(getSatContext());
   //DO NOT TOUCH THE OUTPUTSTREAM
 
-  //TODO: Improve this
-  for(ArithVar v = 0, end = d_variables.size(); v != end; ++v){
+  for(var_iterator vi = var_begin(), vend = var_end(); vi != vend; ++vi){
+    ArithVar v = *vi;
     if(isInteger(v)){
       const DeltaRational& dr = d_partialModel.getAssignment(v);
       if(d_partialModel.equalsUpperBound(v, dr) || d_partialModel.equalsLowerBound(v, dr)){
@@ -1485,7 +1531,8 @@ bool TheoryArith::assertionCases(Constraint constraint){
  * If this returns true, all integer variables have an integer assignment.
  */
 bool TheoryArith::hasIntegerModel(){
-  if(d_variables.size() > 0){
+  //if(d_variables.size() > 0){
+  if(getNumberOfVariables()){
     const ArithVar rrEnd = d_nextIntegerCheckVar;
     do {
       //Do not include slack variables
@@ -1495,7 +1542,7 @@ bool TheoryArith::hasIntegerModel(){
           return false;
         }
       }
-    } while((d_nextIntegerCheckVar = (1 + d_nextIntegerCheckVar == d_variables.size() ? 0 : 1 + d_nextIntegerCheckVar)) != rrEnd);
+    } while((d_nextIntegerCheckVar = (1 + d_nextIntegerCheckVar == getNumberOfVariables() ? 0 : 1 + d_nextIntegerCheckVar)) != rrEnd);
   }
   return true;
 }
@@ -1576,6 +1623,7 @@ void TheoryArith::check(Effort effortLevel){
   Assert(d_conflicts.empty());
 
   d_qflraStatus = d_simplex.findModel(fullEffort(effortLevel));
+
   switch(d_qflraStatus){
   case Result::SAT:
     if(newFacts){
@@ -1822,7 +1870,8 @@ bool TheoryArith::splitDisequalities(){
  */
 void TheoryArith::debugPrintAssertions() {
   Debug("arith::print_assertions") << "Assertions:" << endl;
-  for (ArithVar i = 0; i < d_variables.size(); ++ i) {
+  for (var_iterator vi = var_begin(), vend = var_end(); vi != vend; ++vi){
+    ArithVar i = *vi;
     if (d_partialModel.hasLowerBound(i)) {
       Constraint lConstr = d_partialModel.getLowerBoundConstraint(i);
       Debug("arith::print_assertions") << lConstr << endl;
@@ -1842,13 +1891,15 @@ void TheoryArith::debugPrintAssertions() {
 
 void TheoryArith::debugPrintModel(){
   Debug("arith::print_model") << "Model:" << endl;
-
-  for (ArithVar i = 0; i < d_variables.size(); ++ i) {
-    Debug("arith::print_model") << d_variables[i] << " : " <<
-      d_partialModel.getAssignment(i);
-    if(d_tableau.isBasic(i))
-      Debug("arith::print_model") << " (basic)";
-    Debug("arith::print_model") << endl;
+  for (var_iterator vi = var_begin(), vend = var_end(); vi != vend; ++vi){
+    ArithVar i = *vi;
+    if(d_arithvarNodeMap.hasNode(i)){
+      Debug("arith::print_model") << d_arithvarNodeMap.asNode(i) << " : " <<
+        d_partialModel.getAssignment(i);
+      if(d_tableau.isBasic(i))
+        Debug("arith::print_model") << " (basic)";
+      Debug("arith::print_model") << endl;
+    }
   }
 }
 
@@ -2057,7 +2108,8 @@ Rational TheoryArith::deltaValueForTotalOrder() const{
     relevantDeltaValues.insert(val);
   }
 
-  for(ArithVar v = 0; v < d_variables.size(); ++v){
+  for(var_iterator vi = var_begin(), vend = var_end(); vi != vend; ++vi){
+    ArithVar v = *vi;
     const DeltaRational& value = d_partialModel.getAssignment(v);
     relevantDeltaValues.insert(value);
     if( d_partialModel.hasLowerBound(v)){
@@ -2108,7 +2160,8 @@ void TheoryArith::collectModelInfo( TheoryModel* m, bool fullModel ){
   // TODO:
   // This is not very good for user push/pop....
   // Revisit when implementing push/pop
-  for(ArithVar v = 0; v < d_variables.size(); ++v){
+  for(var_iterator vi = var_begin(), vend = var_end(); vi != vend; ++vi){
+    ArithVar v = *vi;
     if(!isSlackVariable(v)){
       Node term = d_arithvarNodeMap.asNode(v);
 
@@ -2187,13 +2240,13 @@ void TheoryArith::notifyRestart(){
 }
 
 bool TheoryArith::entireStateIsConsistent(const string& s){
-  typedef std::vector<Node>::const_iterator VarIter;
   bool result = true;
-  for(VarIter i = d_variables.begin(), end = d_variables.end(); i != end; ++i){
-    ArithVar var = d_arithvarNodeMap.asArithVar(*i);
+  for(var_iterator vi = var_begin(), vend = var_end(); vi != vend; ++vi){
+    ArithVar var = *vi;
+    //ArithVar var = d_arithvarNodeMap.asArithVar(*i);
     if(!d_partialModel.assignmentIsConsistent(var)){
       d_partialModel.printModel(var);
-      Warning() << s << ":" << "Assignment is not consistent for " << var << *i;
+      Warning() << s << ":" << "Assignment is not consistent for " << var << d_arithvarNodeMap.asNode(var);
       if(d_tableau.isBasic(var)){
         Warning() << " (basic)";
       }
@@ -2205,15 +2258,14 @@ bool TheoryArith::entireStateIsConsistent(const string& s){
 }
 
 bool TheoryArith::unenqueuedVariablesAreConsistent(){
-  typedef std::vector<Node>::const_iterator VarIter;
   bool result = true;
-  for(VarIter i = d_variables.begin(), end = d_variables.end(); i != end; ++i){
-    ArithVar var = d_arithvarNodeMap.asArithVar(*i);
+  for(var_iterator vi = var_begin(), vend = var_end(); vi != vend; ++vi){
+    ArithVar var = *vi;
     if(!d_partialModel.assignmentIsConsistent(var)){
       if(!d_simplex.debugIsInCollectionQueue(var)){
 
         d_partialModel.printModel(var);
-        Warning() << "Unenqueued var is not consistent for " << var << *i;
+        Warning() << "Unenqueued var is not consistent for " << var <<  d_arithvarNodeMap.asNode(var);
         if(d_tableau.isBasic(var)){
           Warning() << " (basic)";
         }
@@ -2221,7 +2273,7 @@ bool TheoryArith::unenqueuedVariablesAreConsistent(){
         result = false;
       } else if(Debug.isOn("arith::consistency::initial")){
         d_partialModel.printModel(var);
-        Warning() << "Initial var is not consistent for " << var << *i;
+        Warning() << "Initial var is not consistent for " << var <<  d_arithvarNodeMap.asNode(var);
         if(d_tableau.isBasic(var)){
           Warning() << " (basic)";
         }