diff options
author | Tim King <taking@cs.nyu.edu> | 2013-01-23 16:35:16 -0500 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2013-01-23 17:12:48 -0500 |
commit | 1435948e241d3134d44662b9476935fe635b4166 (patch) | |
tree | 21102cce34787e842d04e998a1ff3cdf4da25c81 /src/theory | |
parent | 9883548405f15ca8c18b7602092b186bc6934339 (diff) |
Adding miplibtrick option.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arith/arith_static_learner.cpp | 13 | ||||
-rw-r--r-- | src/theory/arith/arith_static_learner.h | 1 | ||||
-rw-r--r-- | src/theory/arith/options | 4 |
3 files changed, 16 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; } diff --git a/src/theory/arith/arith_static_learner.h b/src/theory/arith/arith_static_learner.h index 0de28c5ab..041ae6339 100644 --- a/src/theory/arith/arith_static_learner.h +++ b/src/theory/arith/arith_static_learner.h @@ -45,6 +45,7 @@ private: // The domain is an implicit list OR(x, OR(y, ..., FALSE )) // or FALSE CDNodeToNodeListMap d_miplibTrick; + void miplibTrickInsert(Node key, Node value); /** * Map from a node to it's minimum and maximum. diff --git a/src/theory/arith/options b/src/theory/arith/options index 38cf07251..ab377c8a1 100644 --- a/src/theory/arith/options +++ b/src/theory/arith/options @@ -51,4 +51,8 @@ option arithRewriteEq --enable-arith-rewrite-equalities/--disable-arith-rewrite- turns on the preprocessing rewrite turning equalities into a conjunction of inequalities /turns off the preprocessing rewrite turning equalities into a conjunction of inequalities +option arithMLTrick --enable-miplib-trick/--disable-miplib-trick bool :default false :read-write + turns on the preprocessing step of attempting to infer bounds on miplib problems +/turns off the preprocessing step of attempting to infer bounds on miplib problems + endmodule |