Remove old miplibtrick from arith static learner

diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp
index 4ee176cf14248e00d6ab06af0b3d469de48b5cb3..124fa8e2aa7f157b94524a48d5bcda1557a25e91 100644 (file)
--- a/src/theory/arith/arith_static_learner.cpp
+++ b/src/theory/arith/arith_static_learner.cpp
@@ -21,8 +21,6 @@
 #include "theory/arith/arith_static_learner.h"
 #include "theory/arith/options.h"
 
-#include "util/propositional_query.h"
-
 #include "expr/expr.h"
 #include "expr/convenience_node_builders.h"
 
@@ -37,7 +35,6 @@ namespace arith {
 
 
 ArithStaticLearner::ArithStaticLearner(context::Context* userContext) :
-  d_miplibTrick(userContext),
   d_minMap(userContext),
   d_maxMap(userContext),
   d_statistics()
@@ -45,30 +42,17 @@ ArithStaticLearner::ArithStaticLearner(context::Context* userContext) :
 
 ArithStaticLearner::Statistics::Statistics():
   d_iteMinMaxApplications("theory::arith::iteMinMaxApplications", 0),
-  d_iteConstantApplications("theory::arith::iteConstantApplications", 0),
-  d_miplibtrickApplications("theory::arith::miplibtrickApplications", 0),
-  d_avgNumMiplibtrickValues("theory::arith::avgNumMiplibtrickValues")
+  d_iteConstantApplications("theory::arith::iteConstantApplications", 0)
 {
   StatisticsRegistry::registerStat(&d_iteMinMaxApplications);
   StatisticsRegistry::registerStat(&d_iteConstantApplications);
-  StatisticsRegistry::registerStat(&d_miplibtrickApplications);
-  StatisticsRegistry::registerStat(&d_avgNumMiplibtrickValues);
 }
 
 ArithStaticLearner::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_iteMinMaxApplications);
   StatisticsRegistry::unregisterStat(&d_iteConstantApplications);
-  StatisticsRegistry::unregisterStat(&d_miplibtrickApplications);
-  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;
@@ -111,8 +95,6 @@ void ArithStaticLearner::staticLearning(TNode n, NodeBuilder<>& learned){
     process(n,learned, defTrue);
 
   }
-
-  postProcess(learned);
 }
 
 
@@ -134,24 +116,6 @@ void ArithStaticLearner::process(TNode n, NodeBuilder<>& learned, const TNodeSet
       iteConstant(n, learned);
     }
     break;
-  case IMPLIES:
-    // == 3-FINITE VALUE SET : Collect information ==
-    if(n[1].getKind() == EQUAL &&
-       n[1][0].isVar() &&
-       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];
-        Node current = (d_miplibTrick.find(var)  == d_miplibTrick.end()) ?
-          mkBoolNode(false) : d_miplibTrick[var];
-
-        miplibTrickInsert(var, n.orNode(current));
-        Debug("arith::miplib") << "insert " << var  << " const " << n << endl;
-      }
-    }
-    break;
   case CONST_RATIONAL:
     // Mark constants as minmax
     d_minMap.insert(n, n.getConst<Rational>());
@@ -300,99 +264,6 @@ std::set<Node> listToSet(TNode l){
   return ret;
 }
 
-void ArithStaticLearner::postProcess(NodeBuilder<>& learned){
-  // == 3-FINITE VALUE SET ==
-  CDNodeToNodeListMap::const_iterator keyIter = d_miplibTrick.begin();
-  CDNodeToNodeListMap::const_iterator endKeys = d_miplibTrick.end();
-  while(keyIter != endKeys) {
-    TNode var = (*keyIter).first;
-    Node list = (*keyIter).second;
-    const set<Node> imps = listToSet(list);
-
-    if(imps.empty()){
-      ++keyIter;
-      continue;
-    }
-
-    Assert(!imps.empty());
-    vector<Node> conditions;
-    set<Rational> values;
-    set<Node>::const_iterator j=imps.begin(), impsEnd=imps.end();
-    for(; j != impsEnd; ++j){
-      TNode imp = *j;
-      Assert(imp.getKind() == IMPLIES);
-      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]);
-      values.insert(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)){
-      miplibTrick(var, values, learned);
-      miplibTrickInsert(var, mkBoolNode(false));
-    }
-    ++keyIter;
-  }
-}
-
-
-void ArithStaticLearner::miplibTrick(TNode var, set<Rational>& values, NodeBuilder<>& learned){
-
-  Debug("arith::miplib") << var << " found a tautology!"<< endl;
-
-  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;
-  }
-}
-
 void ArithStaticLearner::addBound(TNode n) {
 
   CDNodeToMinMaxMap::const_iterator minFind = d_minMap.find(n[0]);

diff --git a/src/theory/arith/arith_static_learner.h b/src/theory/arith/arith_static_learner.h
index 041ae63399b8ece0861db9f0d038ab0f62d84d21..48ee6a3bbd1388365b6411175741215d28ba4112 100644 (file)
--- a/src/theory/arith/arith_static_learner.h
+++ b/src/theory/arith/arith_static_learner.h
@@ -37,16 +37,6 @@ namespace arith {
 class ArithStaticLearner {
 private:
 
-  /* Maps a variable, x, to the set of defTrue nodes of the form
-   *  (=> _ (= x c))
-   * where c is a constant.
-   */
-  typedef context::CDTrailHashMap<Node, Node, NodeHashFunction> CDNodeToNodeListMap;
-  // 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.
    */
@@ -63,23 +53,15 @@ public:
 private:
   void process(TNode n, NodeBuilder<>& learned, const TNodeSet& defTrue);
 
-  void postProcess(NodeBuilder<>& learned);
-
   void iteMinMax(TNode n, NodeBuilder<>& learned);
   void iteConstant(TNode n, NodeBuilder<>& learned);
 
-  void miplibTrick(TNode var, std::set<Rational>& values, NodeBuilder<>& learned);
-
-
   /** These fields are designed to be accessible to ArithStaticLearner methods. */
   class Statistics {
   public:
     IntStat d_iteMinMaxApplications;
     IntStat d_iteConstantApplications;
 
-    IntStat d_miplibtrickApplications;
-    AverageStat d_avgNumMiplibtrickValues;
-
     Statistics();
     ~Statistics();
   };