1 files changed, 135 insertions, 0 deletions

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 456fdb746..b75140bc7 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -27,6 +27,8 @@
 #include "util/rational.h"
 #include "util/integer.h"
 
+#include "theory/rewriter.h"
+
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/delta_rational.h"
 #include "theory/arith/partial_model.h"
@@ -79,6 +81,8 @@ TheoryArith::Statistics::Statistics():
   d_staticLearningTimer("theory::arith::staticLearningTimer"),
   d_permanentlyRemovedVariables("theory::arith::permanentlyRemovedVariables", 0),
   d_presolveTime("theory::arith::presolveTime"),
+  d_miplibtrickApplications("theory::arith::miplibtrickApplications", 0),
+  d_avgNumMiplibtrickValues("theory::arith::avgNumMiplibtrickValues"),
   d_initialTableauDensity("theory::arith::initialTableauDensity", 0.0),
   d_avgTableauDensityAtRestart("theory::arith::avgTableauDensityAtRestarts"),
   d_tableauResets("theory::arith::tableauResets", 0),
@@ -93,6 +97,9 @@ TheoryArith::Statistics::Statistics():
   StatisticsRegistry::registerStat(&d_permanentlyRemovedVariables);
   StatisticsRegistry::registerStat(&d_presolveTime);
 
+  StatisticsRegistry::registerStat(&d_miplibtrickApplications);
+  StatisticsRegistry::registerStat(&d_avgNumMiplibtrickValues);
+
   StatisticsRegistry::registerStat(&d_initialTableauDensity);
   StatisticsRegistry::registerStat(&d_avgTableauDensityAtRestart);
   StatisticsRegistry::registerStat(&d_tableauResets);
@@ -109,19 +116,43 @@ TheoryArith::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_permanentlyRemovedVariables);
   StatisticsRegistry::unregisterStat(&d_presolveTime);
 
+  StatisticsRegistry::unregisterStat(&d_miplibtrickApplications);
+  StatisticsRegistry::unregisterStat(&d_avgNumMiplibtrickValues);
+
   StatisticsRegistry::unregisterStat(&d_initialTableauDensity);
   StatisticsRegistry::unregisterStat(&d_avgTableauDensityAtRestart);
   StatisticsRegistry::unregisterStat(&d_tableauResets);
   StatisticsRegistry::unregisterStat(&d_restartTimer);
 }
 
+#include "util/propositional_query.h"
 void TheoryArith::staticLearning(TNode n, NodeBuilder<>& learned) {
   TimerStat::CodeTimer codeTimer(d_statistics.d_staticLearningTimer);
 
+  /*
+  if(Debug.isOn("prop::static")){
+    Debug("prop::static") << n << "is "
+                          << prop::PropositionalQuery::isSatisfiable(n)
+                          << endl;
+  }
+  */
+
   vector<TNode> workList;
   workList.push_back(n);
   __gnu_cxx::hash_set<TNode, TNodeHashFunction> processed;
 
+  //Contains an underapproximation of nodes that must hold.
+  __gnu_cxx::hash_set<TNode, TNodeHashFunction> defTrue;
+
+  /* Maps a variable, x, to the set of defTrue nodes of the form
+   *  (=> _ (= x c))
+   * where c is a constant.
+   */
+  typedef __gnu_cxx::hash_map<TNode, set<TNode>, TNodeHashFunction> VarToNodeSetMap;
+  VarToNodeSetMap miplibTrick;
+
+  defTrue.insert(n);
+
   while(!workList.empty()) {
     n = workList.back();
 
@@ -133,6 +164,11 @@ void TheoryArith::staticLearning(TNode n, NodeBuilder<>& learned) {
         unprocessedChildren = true;
       }
     }
+    if(n.getKind() == AND && defTrue.find(n) != defTrue.end() ){
+      for(TNode::iterator i = n.begin(), iend = n.end(); i != iend; ++i) {
+        defTrue.insert(*i);
+      }
+    }
 
     if(unprocessedChildren) {
       continue;
@@ -202,6 +238,105 @@ void TheoryArith::staticLearning(TNode n, NodeBuilder<>& learned) {
       Debug("arith::mins") << n << " is a constant sandwich"  << nGeqMin << nLeqMax << endl;
       learned << nGeqMin << nLeqMax;
     }
+    // == 3-FINITE VALUE SET : Collect information ==
+    if(n.getKind() == IMPLIES &&
+       n[1].getKind() == EQUAL &&
+       n[1][0].getMetaKind() == metakind::VARIABLE &&
+       defTrue.find(n) != defTrue.end()){
+      Node eqTo = n[1][1];
+      Node rewriteEqTo = Rewriter::rewrite(eqTo);
+      if(rewriteEqTo.getKind() == CONST_RATIONAL){
+
+        TNode var = n[1][0];
+        if(miplibTrick.find(var)  == miplibTrick.end()){
+          //[MGD] commented out following line as per TAK's instructions
+          //miplibTrick.insert(make_pair(var, set<TNode>()));
+        }
+        //[MGD] commented out following line as per TAK's instructions
+        //miplibTrick[var].insert(n);
+        Debug("arith::miplib") << "insert " << var  << " const " << n << endl;
+      }
+    }
+  }
+
+  // == 3-FINITE VALUE SET ==
+  VarToNodeSetMap::iterator i = miplibTrick.begin(), endMipLibTrick = miplibTrick.end();
+  for(; i != endMipLibTrick; ++i){
+    TNode var = i->first;
+    const set<TNode>& imps = i->second;
+
+    Assert(!imps.empty());
+    vector<Node> conditions;
+    vector<Rational> valueCollection;
+    set<TNode>::const_iterator j=imps.begin(), impsEnd=imps.end();
+    for(; j != impsEnd; ++j){
+      TNode imp = *j;
+      Assert(imp.getKind() == IMPLIES);
+      Assert(defTrue.find(imp) != defTrue.end());
+      Assert(imp[1].getKind() == EQUAL);
+
+
+      Node eqTo = imp[1][1];
+      Node rewriteEqTo = Rewriter::rewrite(eqTo);
+      Assert(rewriteEqTo.getKind() == CONST_RATIONAL);
+
+      conditions.push_back(imp[0]);
+      valueCollection.push_back(rewriteEqTo.getConst<Rational>());
+    }
+
+    Node possibleTaut = Node::null();
+    if(conditions.size() == 1){
+      possibleTaut = conditions.front();
+    }else{
+      NodeBuilder<> orBuilder(OR);
+      orBuilder.append(conditions);
+      possibleTaut = orBuilder;
+    }
+
+
+    Debug("arith::miplib") << "var: " << var << endl;
+    Debug("arith::miplib") << "possibleTaut: " << possibleTaut << endl;
+
+    Result isTaut = PropositionalQuery::isTautology(possibleTaut);
+    if(isTaut == Result(Result::VALID)){
+      Debug("arith::miplib") << var << " found a tautology!"<< endl;
+
+      set<Rational> values(valueCollection.begin(), valueCollection.end());
+      const Rational& min = *(values.begin());
+      const Rational& max = *(values.rbegin());
+
+      Debug("arith::miplib") << "min: " << min << endl;
+      Debug("arith::miplib") << "max: " << max << endl;
+
+      Assert(min <= max);
+
+      ++(d_statistics.d_miplibtrickApplications);
+      (d_statistics.d_avgNumMiplibtrickValues).addEntry(values.size());
+
+      Node nGeqMin = NodeBuilder<2>(GEQ) << var << mkRationalNode(min);
+      Node nLeqMax = NodeBuilder<2>(LEQ) << var << mkRationalNode(max);
+      Debug("arith::miplib") << nGeqMin << nLeqMax << endl;
+      learned << nGeqMin << nLeqMax;
+      set<Rational>::iterator valuesIter = values.begin();
+      set<Rational>::iterator valuesEnd = values.end();
+      set<Rational>::iterator valuesPrev = valuesIter;
+      ++valuesIter;
+      for(; valuesIter != valuesEnd; valuesPrev = valuesIter, ++valuesIter){
+        const Rational& prev = *valuesPrev;
+        const Rational& curr = *valuesIter;
+        Assert(prev < curr);
+
+        //The interval (last,curr) can be excluded:
+        //(not (and (> var prev) (< var curr))
+        //<=> (or (not (> var prev)) (not (< var curr)))
+        //<=> (or (<= var prev) (>= var curr))
+        Node leqPrev = NodeBuilder<2>(LEQ) << var << mkRationalNode(prev);
+        Node geqCurr = NodeBuilder<2>(GEQ) << var << mkRationalNode(curr);
+        Node excludedMiddle =  NodeBuilder<2>(OR) << leqPrev << geqCurr;
+        Debug("arith::miplib") << excludedMiddle << endl;
+        learned << excludedMiddle;
+      }
+    }
   }
 }