- The learned clauses from the miplib trick were being added twice. This was slowing down the search. (The effect can be seen in the difference between jobs 1765 and 1755). This happened during commit -r1480 when adding the ArithStaticLearner. This has been fixed.

1 files changed, 12 insertions, 5 deletions

diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp
index 6fb538fac..548651358 100644
--- a/src/theory/arith/arith_static_learner.cpp
+++ b/src/theory/arith/arith_static_learner.cpp
@@ -212,13 +212,19 @@ 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 ==
-  VarToNodeSetMap::iterator i = d_miplibTrick.begin();
-  VarToNodeSetMap::iterator endMipLibTrick = d_miplibTrick.end();
-  for(; i != endMipLibTrick; ++i){
-    TNode var = i->first;
-    const set<Node>& imps = i->second;
+  vector<TNode>::iterator keyIter = keys.begin();
+  vector<TNode>::iterator endKeys = keys.end();
+  for(; keyIter != endKeys; ++keyIter){
+    TNode var = *keyIter;
+    const set<Node>& imps = d_miplibTrick[var];
 
     Assert(!imps.empty());
     vector<Node> conditions;
@@ -253,6 +259,7 @@ void ArithStaticLearner::postProcess(NodeBuilder<>& learned){
     Result isTaut = PropositionalQuery::isTautology(possibleTaut);
     if(isTaut == Result(Result::VALID)){
       miplibTrick(var, values, learned);
+      d_miplibTrick.erase(var);
     }
   }
 }