Adding miplibtrick option.

diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp
index 9ae7cd1c2664e97fdbc76b19ebab22740d2d9ece..4ee176cf14248e00d6ab06af0b3d469de48b5cb3 100644 (file)
--- 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 0de28c5ab9a55f0ee4260599468c340384015cfa..041ae63399b8ece0861db9f0d038ab0f62d84d21 100644 (file)
--- 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 38cf072516524f5baeea07ac642dba3c7ae012b5..ab377c8a1dc0fb78e6f281042ecc248b62799db2 100644 (file)
--- 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