apply arithmetic static learner's miplibtrick in a consistent order (for easier replication of experiment)

2 files changed, 40 insertions, 11 deletions

diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp
index 548651358..315c6ce94 100644
--- a/src/theory/arith/arith_static_learner.cpp
+++ b/src/theory/arith/arith_static_learner.cpp
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file arith_rewriter.cpp
+/*! \file arith_static_learner.cpp
  ** \verbatim
  ** Original author: taking
  ** Major contributors: dejan
@@ -36,6 +36,7 @@ using namespace CVC4::theory::arith;
 
 ArithStaticLearner::ArithStaticLearner():
   d_miplibTrick(),
+  d_miplibTrickKeys(),
   d_statistics()
 {}
 
@@ -106,6 +107,7 @@ void ArithStaticLearner::staticLearning(TNode n, NodeBuilder<>& learned){
 
 void ArithStaticLearner::clear(){
   d_miplibTrick.clear();
+  d_miplibTrickKeys.clear();
 }
 
 
@@ -136,6 +138,7 @@ void ArithStaticLearner::process(TNode n, NodeBuilder<>& learned, const TNodeSet
         TNode var = n[1][0];
         if(d_miplibTrick.find(var)  == d_miplibTrick.end()){
           d_miplibTrick.insert(make_pair(var, set<Node>()));
+          d_miplibTrickKeys.push_back(var);
         }
         d_miplibTrick[var].insert(n);
         Debug("arith::miplib") << "insert " << var  << " const " << n << endl;
@@ -212,17 +215,10 @@ void ArithStaticLearner::iteConstant(TNode n, NodeBuilder<>& learned){
 
 
 void ArithStaticLearner::postProcess(NodeBuilder<>& learned){
-  vector<TNode> keys;
-  VarToNodeSetMap::iterator mipIter = d_miplibTrick.begin();
-  VarToNodeSetMap::iterator endMipLibTrick = d_miplibTrick.end();
-  for(; mipIter != endMipLibTrick; ++mipIter){
-    keys.push_back(mipIter->first);
-  }
-
   // == 3-FINITE VALUE SET ==
-  vector<TNode>::iterator keyIter = keys.begin();
-  vector<TNode>::iterator endKeys = keys.end();
-  for(; keyIter != endKeys; ++keyIter){
+  list<TNode>::iterator keyIter = d_miplibTrickKeys.begin();
+  list<TNode>::iterator endKeys = d_miplibTrickKeys.end();
+  while(keyIter != endKeys) {
     TNode var = *keyIter;
     const set<Node>& imps = d_miplibTrick[var];
 
@@ -260,6 +256,18 @@ void ArithStaticLearner::postProcess(NodeBuilder<>& learned){
     if(isTaut == Result(Result::VALID)){
       miplibTrick(var, values, learned);
       d_miplibTrick.erase(var);
+      // also have to erase from keys list
+      if(keyIter == endKeys) {
+        // last element is special: exit loop
+        d_miplibTrickKeys.erase(keyIter);
+        break;
+      } else {
+        // non-last element: make sure iterator is incremented before erase
+        list<TNode>::iterator eraseIter = keyIter++;
+        d_miplibTrickKeys.erase(eraseIter);
+      }
+    } else {
+      ++keyIter;
     }
   }
 }
diff --git a/src/theory/arith/arith_static_learner.h b/src/theory/arith/arith_static_learner.h
index 02274318f..f2405cd5c 100644
--- a/src/theory/arith/arith_static_learner.h
+++ b/src/theory/arith/arith_static_learner.h
@@ -1,3 +1,22 @@
+/*********************                                                        */
+/*! \file arith_static_learner.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, 2011  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
+ **/
+
 #include "cvc4_private.h"
 
 #ifndef __CVC4__THEORY__ARITH__ARITH_STATIC_LEARNER_H
@@ -7,6 +26,7 @@
 #include "util/stats.h"
 #include "theory/arith/arith_utilities.h"
 #include <set>
+#include <list>
 
 namespace CVC4 {
 namespace theory {
@@ -22,6 +42,7 @@ private:
    */
   typedef __gnu_cxx::hash_map<Node, std::set<Node>, NodeHashFunction> VarToNodeSetMap;
   VarToNodeSetMap d_miplibTrick;
+  std::list<TNode> d_miplibTrickKeys;
 
 public:
   ArithStaticLearner();