diff options
author | Tim King <taking@cs.nyu.edu> | 2013-04-01 11:26:57 -0400 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2013-04-01 19:43:06 -0400 |
commit | 354ef7c75f886a315b985324c76a658efb1da11f (patch) | |
tree | 81ece6ba8b15d2596bb0836fd99cc410911a0912 /src/theory/arith | |
parent | 3740d285d939b85af47804871abbf545ddda01af (diff) |
Adding a restart test strategy to integers.
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/options | 3 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 45 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.h | 2 |
3 files changed, 41 insertions, 9 deletions
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: |