Merging a squash of the branch timothy-king/CVC4/glpknecfix c95bf7d4f1 into master. See the CAV14 submission for an explanation of the changes to the integer solver's behavior. If compiled against the our custom extension of glpk, https://github.com/timothy-king/glpk-cut-log, this should have substantial differences in behavior. This should have moderate performance differences for linear real and integer arithmetic even if these features are disabled.

1 files changed, 8 insertions, 42 deletions

diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp
index 8f6f75295..3854188e0 100644
--- a/src/theory/arith/arith_static_learner.cpp
+++ b/src/theory/arith/arith_static_learner.cpp
@@ -21,6 +21,8 @@
 #include "theory/arith/arith_static_learner.h"
 #include "theory/arith/options.h"
 
+#include "theory/arith/normal_form.h"
+
 #include "expr/expr.h"
 #include "expr/convenience_node_builders.h"
 
@@ -38,7 +40,11 @@ ArithStaticLearner::ArithStaticLearner(context::Context* userContext) :
   d_minMap(userContext),
   d_maxMap(userContext),
   d_statistics()
-{}
+{
+}
+
+ArithStaticLearner::~ArithStaticLearner(){
+}
 
 ArithStaticLearner::Statistics::Statistics():
   d_iteMinMaxApplications("theory::arith::iteMinMaxApplications", 0),
@@ -98,9 +104,6 @@ void ArithStaticLearner::staticLearning(TNode n, NodeBuilder<>& learned){
 }
 
 
-
-
-
 void ArithStaticLearner::process(TNode n, NodeBuilder<>& learned, const TNodeSet& defTrue){
   Debug("arith::static") << "===================== looking at " << n << endl;
 
@@ -116,49 +119,12 @@ void ArithStaticLearner::process(TNode n, NodeBuilder<>& learned, const TNodeSet
       iteConstant(n, learned);
     }
     break;
+
   case CONST_RATIONAL:
     // Mark constants as minmax
     d_minMap.insert(n, n.getConst<Rational>());
     d_maxMap.insert(n, n.getConst<Rational>());
     break;
-  case OR: {
-    // Look for things like "x = 0 OR x = 1" (that are defTrue) and
-    // turn them into a pseudoboolean.  We catch "x >= 0
-    if(defTrue.find(n) == defTrue.end() ||
-       n.getNumChildren() != 2 ||
-       n[0].getKind() != EQUAL ||
-       n[1].getKind() != EQUAL) {
-      break;
-    }
-    Node var, c1, c2;
-    if(n[0][0].isVar() &&
-       n[0][1].isConst()) {
-      var = n[0][0];
-      c1 = n[0][1];
-    } else if(n[0][1].isVar() &&
-              n[0][0].isConst()) {
-      var = n[0][1];
-      c1 = n[0][0];
-    } else {
-      break;
-    }
-    if(!var.getType().isInteger() ||
-       !c1.getType().isReal()) {
-      break;
-    }
-    if(var == n[1][0]) {
-      c2 = n[1][1];
-    } else if(var == n[1][1]) {
-      c2 = n[1][0];
-    } else {
-      break;
-    }
-    if(!c2.getType().isReal()) {
-      break;
-    }
-
-    break;
-  }
   default: // Do nothing
     break;
   }