From ecff741b43b7c5493a7e1ef801cbe7ff68f8ff54 Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Wed, 16 Mar 2011 15:36:45 +0000
Subject: [PATCH] - Turns on the miplibTrick.  This detects during the static
 learning phase a set of nodes that are asserted to the theory of the form (=>
 p_i (= x c_i)). If (or p_1 p_2 ...) is a tautology, then x \in {c_1, c_2,
 ...}. (This tautology check currently requires CUDD to be installed.)  Right
 now all this does is assert x \leq max{c_i} and x \geq min{c_i}. (Compare
 jobs 1728 to 1626 for how this affects the miplib examples.)

---
 src/theory/arith/theory_arith.cpp | 47 ++++++++-----------------------
 1 file changed, 12 insertions(+), 35 deletions(-)

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index b75140bc7..09bb48c8a 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -129,14 +129,6 @@ TheoryArith::Statistics::~Statistics(){
 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;
@@ -249,11 +241,9 @@ void TheoryArith::staticLearning(TNode n, NodeBuilder<>& learned) {
 
         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>()));
+          miplibTrick.insert(make_pair(var, set<TNode>()));
         }
-        //[MGD] commented out following line as per TAK's instructions
-        //miplibTrick[var].insert(n);
+        miplibTrick[var].insert(n);
         Debug("arith::miplib") << "insert " << var  << " const " << n << endl;
       }
     }
@@ -301,9 +291,15 @@ void TheoryArith::staticLearning(TNode n, NodeBuilder<>& learned) {
     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());
+      vector<Rational>::iterator minIter, maxIter;
+      minIter = std::min_element(valueCollection.begin(), valueCollection.end());
+      maxIter = std::max_element(valueCollection.begin(), valueCollection.end());
+
+      Assert(minIter != valueCollection.end());
+      Assert(maxIter != valueCollection.end());
+
+      const Rational& min = *minIter;
+      const Rational& max = *maxIter;
 
       Debug("arith::miplib") << "min: " << min << endl;
       Debug("arith::miplib") << "max: " << max << endl;
@@ -311,31 +307,12 @@ void TheoryArith::staticLearning(TNode n, NodeBuilder<>& learned) {
       Assert(min <= max);
 
       ++(d_statistics.d_miplibtrickApplications);
-      (d_statistics.d_avgNumMiplibtrickValues).addEntry(values.size());
+      (d_statistics.d_avgNumMiplibtrickValues).addEntry(valueCollection.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;
-      }
     }
   }
 }
-- 
2.30.2