From 1435948e241d3134d44662b9476935fe635b4166 Mon Sep 17 00:00:00 2001 From: Tim King Date: Wed, 23 Jan 2013 16:35:16 -0500 Subject: [PATCH] Adding miplibtrick option. --- src/theory/arith/arith_static_learner.cpp | 13 +++++++++++-- src/theory/arith/arith_static_learner.h | 1 + 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 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 -- 2.30.2