diff options
Diffstat (limited to 'src/theory/arith/arith_static_learner.cpp')
-rw-r--r-- | src/theory/arith/arith_static_learner.cpp | 13 |
1 files changed, 11 insertions, 2 deletions
diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp index 9ae7cd1c2..4ee176cf1 100644 --- a/src/theory/arith/arith_static_learner.cpp +++ b/src/theory/arith/arith_static_learner.cpp @@ -19,6 +19,7 @@ #include "theory/arith/arith_utilities.h" #include "theory/arith/arith_static_learner.h" +#include "theory/arith/options.h" #include "util/propositional_query.h" @@ -61,6 +62,13 @@ ArithStaticLearner::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_avgNumMiplibtrickValues); } +void ArithStaticLearner::miplibTrickInsert(Node key, Node value){ + if(options::arithMLTrick()){ + d_miplibTrick.insert(key, value); + } +} + + void ArithStaticLearner::staticLearning(TNode n, NodeBuilder<>& learned){ vector<TNode> workList; @@ -138,7 +146,8 @@ void ArithStaticLearner::process(TNode n, NodeBuilder<>& learned, const TNodeSet TNode var = n[1][0]; Node current = (d_miplibTrick.find(var) == d_miplibTrick.end()) ? mkBoolNode(false) : d_miplibTrick[var]; - d_miplibTrick.insert(var, n.orNode(current)); + + miplibTrickInsert(var, n.orNode(current)); Debug("arith::miplib") << "insert " << var << " const " << n << endl; } } @@ -338,7 +347,7 @@ void ArithStaticLearner::postProcess(NodeBuilder<>& learned){ Result isTaut = PropositionalQuery::isTautology(possibleTaut); if(isTaut == Result(Result::VALID)){ miplibTrick(var, values, learned); - d_miplibTrick.insert(var, mkBoolNode(false)); + miplibTrickInsert(var, mkBoolNode(false)); } ++keyIter; } |