diff options
author | Liana Hadarean <lianahady@gmail.com> | 2015-05-28 15:03:10 +0100 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2015-05-28 15:03:10 +0100 |
commit | b4aaa40ca834958130a8ee5a922ac45c6de84ce1 (patch) | |
tree | d0ce340446271c56909bcac8b1697ca18b7d5773 /src/theory/arrays | |
parent | 3df7ea65b701a9ab054179af7efb4be120d280f2 (diff) |
added options for controlling resource step-count for various solving stages
Diffstat (limited to 'src/theory/arrays')
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index c770fb7ae..8bdf38ca3 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -23,6 +23,7 @@ #include "expr/command.h" #include "theory/theory_model.h" #include "theory/arrays/options.h" +#include "smt/options.h" #include "smt/logic_exception.h" @@ -1031,6 +1032,9 @@ void TheoryArrays::check(Effort e) { if (done() && !fullEffort(e)) { return; } + + getOutputChannel().spendResource(options::theoryCheckStep()); + TimerStat::CodeTimer checkTimer(d_checkTime); while (!done() && !d_conflict) @@ -1209,7 +1213,7 @@ void TheoryArrays::checkModel(Effort e) int numrestarts = 0; while (true || numrestarts < 1 || fullEffort(e) || combination(e)) { ++numrestarts; - d_out->safePoint(); + d_out->safePoint(1); int level = getSatContext()->getLevel(); d_getModelValCache.clear(); for (constraintIdx = 0; constraintIdx < d_modelConstraints.size(); ++constraintIdx) { |