From e33683b83dfe9b24ff2bce5da0c7ff8c25fbfc44 Mon Sep 17 00:00:00 2001 From: Tim King Date: Fri, 18 Mar 2011 22:22:28 +0000 Subject: [PATCH] - 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. --- src/theory/arith/arith_static_learner.cpp | 17 ++++++++++++----- 1 file 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 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& imps = i->second; + vector::iterator keyIter = keys.begin(); + vector::iterator endKeys = keys.end(); + for(; keyIter != endKeys; ++keyIter){ + TNode var = *keyIter; + const set& imps = d_miplibTrick[var]; Assert(!imps.empty()); vector 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); } } } -- 2.30.2