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, 10 insertions, 8 deletions

diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index d79ddee31..ddf763b73 100755
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -46,11 +46,12 @@ void InstStrategySimplex::processResetInstantiationRound( Theory::Effort effort
   d_tableaux.clear();

   d_ceTableaux.clear();

   //search for instantiation rows in simplex tableaux

-  ArithVarToNodeMap avtnm = d_th->d_arithvarNodeMap.getArithVarToNodeMap();

-  for( ArithVarToNodeMap::iterator it = avtnm.begin(); it != avtnm.end(); ++it ){

-    ArithVar x = (*it).first;

+  ArithVarNodeMap& avnm = d_th->d_arithvarNodeMap;

+  ArithVarNodeMap::var_iterator vi, vend;

+  for(vi = avnm.var_begin(), vend = avnm.var_end(); vi != vend; ++vi ){

+    ArithVar x = *vi;

     if( d_th->d_partialModel.hasEitherBound( x ) ){

-      Node n = (*it).second;

+      Node n = avnm.asNode(x);

       Node f;

       NodeBuilder<> t(kind::PLUS);

       if( n.getKind()==PLUS ){

@@ -167,10 +168,11 @@ void InstStrategySimplex::addTermToRow( ArithVar x, Node n, Node& f, NodeBuilder
 }

 

 void InstStrategySimplex::debugPrint( const char* c ){

-  ArithVarToNodeMap avtnm = d_th->d_arithvarNodeMap.getArithVarToNodeMap();

-  for( ArithVarToNodeMap::iterator it = avtnm.begin(); it != avtnm.end(); ++it ){

-    ArithVar x = (*it).first;

-    Node n = (*it).second;

+  const ArithVarNodeMap& avnm = d_th->d_arithvarNodeMap;

+  ArithVarNodeMap::var_iterator vi, vend;

+  for(vi = avnm.var_begin(), vend = avnm.var_end(); vi != vend; ++vi ){

+    ArithVar x = *vi;

+    Node n = avnm.asNode(x);

     //if( ((TheoryArith*)getTheory())->d_partialModel.hasEitherBound( x ) ){

       Debug(c) << x << " : " << n << ", bounds = ";

       if( d_th->d_partialModel.hasLowerBound( x ) ){