Adding a restart test strategy to integers.

diff --git a/src/theory/arith/options b/src/theory/arith/options
index efe5947666d1ef254c92a00a3d85ebaac7d9a1fb..129175eaff2380b64217ac685ad95298b6ce147c 100644 (file)
--- a/src/theory/arith/options
+++ b/src/theory/arith/options
@@ -62,4 +62,7 @@ option doCutAllBounded --enable-cut-all-bounded/--disable-cut-all-bounded bool :
  turns on the integer solving step of periodically cutting all integer variables that have both upper and lower bounds
 /turns off the integer solving step of periodically cutting all integer variables that have both upper and lower bounds
 
+option maxCutsInContext --maxCutsInContext unsigned :default 65535
+ maximum cuts in a given context before signalling a restart
+
 endmodule

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 52f2341293cb916da1678c505efe0e6726ddd371..d167b7a97c6d045656431bc6665d97c847d44d15 100644 (file)
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -89,6 +89,7 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputCha
   d_basicVarModelUpdateCallBack(d_simplex),
   d_DELTA_ZERO(0),
   d_fullCheckCounter(0),
+  d_cutsInContext(c,0),
   d_statistics()
 {
 }
@@ -1737,13 +1738,24 @@ void TheoryArith::check(Effort effortLevel){
   static const int CUT_ALL_BOUNDED_PERIOD = 10;
   if(!emmittedConflictOrSplit && fullEffort(effortLevel) &&
      d_fullCheckCounter % CUT_ALL_BOUNDED_PERIOD == 1){
-    vector<Node> lemmas = cutAllBounded();
-    //output the lemmas
-    for(vector<Node>::const_iterator i = lemmas.begin(); i != lemmas.end(); ++i){
-      d_out->lemma(*i);
-      ++(d_statistics.d_externalBranchAndBounds);
+
+    cout << options::maxCutsInContext() << " " << d_cutsInContext << endl;
+
+    if(options::maxCutsInContext() <= d_cutsInContext){
+      d_out->demandRestart();
+    }else{
+
+      cout << "cutting" << endl;
+
+      vector<Node> lemmas = cutAllBounded();
+      //output the lemmas
+      for(vector<Node>::const_iterator i = lemmas.begin(); i != lemmas.end(); ++i){
+        d_out->lemma(*i);
+        ++(d_statistics.d_externalBranchAndBounds);
+        d_cutsInContext = d_cutsInContext + 1;
+      }
+      emmittedConflictOrSplit = lemmas.size() > 0;
     }
-    emmittedConflictOrSplit = lemmas.size() > 0;
   }
 
   if(!emmittedConflictOrSplit && fullEffort(effortLevel)){
@@ -1769,15 +1781,30 @@ void TheoryArith::check(Effort effortLevel){
         emmittedConflictOrSplit = true;
         d_hasDoneWorkSinceCut = false;
         d_out->lemma(possibleLemma);
+
+        if(options::maxCutsInContext() <= d_cutsInContext){
+          d_out->demandRestart();
+        }else{
+          d_cutsInContext = d_cutsInContext + 1;
+        }
       }
     }
 
     if(!emmittedConflictOrSplit) {
       Node possibleLemma = roundRobinBranch();
       if(!possibleLemma.isNull()){
-        ++(d_statistics.d_externalBranchAndBounds);
-        emmittedConflictOrSplit = true;
-        d_out->lemma(possibleLemma);
+
+        if(options::maxCutsInContext() <= d_cutsInContext){
+          d_out->demandRestart();
+        }else{
+          d_cutsInContext = d_cutsInContext + 1;
+
+          cout << options::maxCutsInContext() << " " << d_cutsInContext << endl;
+
+          ++(d_statistics.d_externalBranchAndBounds);
+          emmittedConflictOrSplit = true;
+          d_out->lemma(possibleLemma);
+        }
       }
     }
   }//if !emmittedConflictOrSplit && fullEffort(effortLevel) && !hasIntegerModel()

diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 31f9bfcafead6367bee70e88db63003b250dd5e2..50061579a5276fde6cc2b0cfbc7e8964629860c1 100644 (file)
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -542,6 +542,8 @@ private:
   std::vector<Node> cutAllBounded() const;
   Node branchIntegerVariable(ArithVar x) const;
 
+  context::CDO<unsigned> d_cutsInContext;
+
   /** These fields are designed to be accessible to TheoryArith methods. */
   class Statistics {
   public: