From 354ef7c75f886a315b985324c76a658efb1da11f Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Mon, 1 Apr 2013 11:26:57 -0400
Subject: Adding a restart test strategy to integers.

---
 src/theory/arith/options          |  3 +++
 src/theory/arith/theory_arith.cpp | 45 +++++++++++++++++++++++++++++++--------
 src/theory/arith/theory_arith.h   |  2 ++
 3 files changed, 41 insertions(+), 9 deletions(-)

(limited to 'src/theory/arith')

diff --git a/src/theory/arith/options b/src/theory/arith/options
index efe594766..129175eaf 100644
--- 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 52f234129..d167b7a97 100644
--- 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 31f9bfcaf..50061579a 100644
--- 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:
-- 
cgit v1.2.3