From b4aaa40ca834958130a8ee5a922ac45c6de84ce1 Mon Sep 17 00:00:00 2001 From: Liana Hadarean Date: Thu, 28 May 2015 15:03:10 +0100 Subject: [PATCH] added options for controlling resource step-count for various solving stages --- src/decision/decision_engine.h | 2 +- src/parser/parser.cpp | 5 +-- src/prop/bvminisat/bvminisat.h | 8 ++--- src/prop/bvminisat/core/Solver.cc | 5 +-- src/prop/bvminisat/core/Solver.h | 12 +++---- src/prop/cnf_stream.cpp | 2 +- src/prop/minisat/core/Solver.cc | 13 ++++---- src/prop/minisat/core/Solver.h | 2 +- src/prop/prop_engine.cpp | 4 +-- src/prop/prop_engine.h | 2 +- src/prop/sat_solver.h | 4 +-- src/prop/theory_proxy.cpp | 6 ++-- src/prop/theory_proxy.h | 2 +- src/smt/options | 38 +++++++++++++++++++++++ src/smt/smt_engine.cpp | 30 +++++++++--------- src/theory/arith/theory_arith.cpp | 2 ++ src/theory/arrays/theory_arrays.cpp | 6 +++- src/theory/bv/bitblaster_template.h | 10 +++--- src/theory/bv/bv_eager_solver.cpp | 2 +- src/theory/bv/bv_subtheory_bitblast.cpp | 2 +- src/theory/bv/bv_subtheory_core.cpp | 3 +- src/theory/bv/bv_subtheory_inequality.cpp | 3 +- src/theory/bv/eager_bitblaster.cpp | 2 +- src/theory/bv/lazy_bitblaster.cpp | 10 +++--- src/theory/bv/theory_bv.cpp | 4 +-- src/theory/bv/theory_bv.h | 2 +- src/theory/output_channel.h | 4 +-- src/theory/quantifiers_engine.cpp | 2 +- src/theory/rewriter.cpp | 2 +- src/theory/theory_engine.cpp | 4 +-- src/theory/theory_engine.h | 10 +++--- src/theory/theory_test_utils.h | 2 +- src/theory/uf/theory_uf.cpp | 3 +- src/util/resource_manager.cpp | 6 ++-- src/util/resource_manager.h | 2 +- 35 files changed, 133 insertions(+), 83 deletions(-) diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h index 61900e59d..ffcf2db63 100644 --- a/src/decision/decision_engine.h +++ b/src/decision/decision_engine.h @@ -118,7 +118,7 @@ public: /** Gets the next decision based on strategies that are enabled */ SatLiteral getNext(bool &stopSearch) { - NodeManager::currentResourceManager()->spendResource(); + NodeManager::currentResourceManager()->spendResource(options::decisionStep()); Assert(d_cnfStream != NULL, "Forgot to set cnfStream for decision engine?"); Assert(d_satSolver != NULL, diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 10a729420..d17d5d141 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -31,6 +31,7 @@ #include "util/output.h" #include "util/resource_manager.h" #include "options/options.h" +#include "smt/options.h" using namespace std; using namespace CVC4::kind; @@ -499,14 +500,14 @@ Command* Parser::nextCommand() throw(ParserException, UnsafeInterruptException) dynamic_cast(cmd) == NULL) { // don't count set-option commands as to not get stuck in an infinite // loop of resourcing out - d_resourceManager->spendResource(); + d_resourceManager->spendResource(d_exprManager->getOptions()[options::parseStep]); } return cmd; } Expr Parser::nextExpression() throw(ParserException, UnsafeInterruptException) { Debug("parser") << "nextExpression()" << std::endl; - d_resourceManager->spendResource(); + d_resourceManager->spendResource(d_exprManager->getOptions()[options::parseStep]); Expr result; if(!done()) { try { diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h index 6246e6885..2c9662655 100644 --- a/src/prop/bvminisat/bvminisat.h +++ b/src/prop/bvminisat/bvminisat.h @@ -46,11 +46,11 @@ private: d_notify->notify(satClause); } - void spendResource() { - d_notify->spendResource(); + void spendResource(uint64_t ammount) { + d_notify->spendResource(ammount); } - void safePoint() { - d_notify->safePoint(); + void safePoint(uint64_t ammount) { + d_notify->safePoint(ammount); } }; diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc index b6238460b..1267561fb 100644 --- a/src/prop/bvminisat/core/Solver.cc +++ b/src/prop/bvminisat/core/Solver.cc @@ -29,6 +29,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "util/utility.h" #include "util/exception.h" #include "theory/bv/options.h" +#include "smt/options.h" #include "theory/interrupted.h" using namespace BVMinisat; @@ -871,7 +872,7 @@ lbool Solver::search(int nof_conflicts, UIP uip) // NO CONFLICT bool isWithinBudget; try { - isWithinBudget = withinBudget(); + isWithinBudget = withinBudget(CVC4::options::bvSatConflictStep()); } catch (const CVC4::theory::Interrupted& e) { // do some clean-up and rethrow @@ -1021,7 +1022,7 @@ lbool Solver::solve_() while (status == l_Undef){ double rest_base = luby_restart ? luby(restart_inc, curr_restarts) : pow(restart_inc, curr_restarts); status = search(rest_base * restart_first); - if (!withinBudget()) break; + if (!withinBudget(CVC4::options::bvSatConflictStep())) break; curr_restarts++; } diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h index 3fcf34185..7d2a978b9 100644 --- a/src/prop/bvminisat/core/Solver.h +++ b/src/prop/bvminisat/core/Solver.h @@ -52,8 +52,8 @@ public: */ virtual void notify(vec& learnt) = 0; - virtual void spendResource() = 0; - virtual void safePoint() = 0; + virtual void spendResource(uint64_t ammount) = 0; + virtual void safePoint(uint64_t ammount) = 0; }; //================================================================================================= @@ -324,7 +324,7 @@ protected: CRef reason (Var x) const; int level (Var x) const; double progressEstimate () const; // DELETE THIS ?? IT'S NOT VERY USEFUL ... - bool withinBudget () const; + bool withinBudget (uint64_t ammount) const; // Static helpers: // @@ -412,10 +412,10 @@ inline void Solver::setPropBudget(int64_t x){ propagation_budget = propagati inline void Solver::interrupt(){ asynch_interrupt = true; } inline void Solver::clearInterrupt(){ asynch_interrupt = false; } inline void Solver::budgetOff(){ conflict_budget = propagation_budget = -1; } -inline bool Solver::withinBudget() const { +inline bool Solver::withinBudget(uint64_t ammount) const { Assert (notify); - notify->spendResource(); - notify->safePoint(); + notify->spendResource(ammount); + notify->safePoint(0); return !asynch_interrupt && (conflict_budget < 0 || conflicts < (uint64_t)conflict_budget) && diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index c8d86c73d..f03cc9944 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -679,7 +679,7 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool negated, ProofRule proo Debug("cnf") << "convertAndAssert(" << node << ", negated = " << (negated ? "true" : "false") << ")" << endl; if (d_convertAndAssertCounter % ResourceManager::getFrequencyCount() == 0) { - NodeManager::currentResourceManager()->spendResource(); + NodeManager::currentResourceManager()->spendResource(options::cnfStep()); d_convertAndAssertCounter = 0; } ++d_convertAndAssertCounter; diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 56316ca0b..2c94401fb 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -1205,7 +1205,8 @@ lbool Solver::search(int nof_conflicts) check_type = CHECK_WITH_THEORY; } - if (nof_conflicts >= 0 && conflictC >= nof_conflicts || !withinBudget()) { + if (nof_conflicts >= 0 && conflictC >= nof_conflicts || + !withinBudget(options::satConflictStep())) { // Reached bound on number of conflicts: progress_estimate = progressEstimate(); cancelUntil(0); @@ -1343,11 +1344,11 @@ lbool Solver::solve_() while (status == l_Undef){ double rest_base = luby_restart ? luby(restart_inc, curr_restarts) : pow(restart_inc, curr_restarts); status = search(rest_base * restart_first); - if (!withinBudget()) break; + if (!withinBudget(options::satConflictStep())) break; // FIXME add restart option? curr_restarts++; } - if(!withinBudget()) + if(!withinBudget(options::satConflictStep())) status = l_Undef; if (verbosity >= 1) @@ -1599,7 +1600,7 @@ CRef Solver::updateLemmas() { Debug("minisat::lemmas") << "Solver::updateLemmas() begin" << std::endl; // Avoid adding lemmas indefinitely without resource-out - proxy->spendResource(); + proxy->spendResource(options::lemmaStep()); CRef conflict = CRef_Undef; @@ -1717,11 +1718,11 @@ CRef Solver::updateLemmas() { return conflict; } -inline bool Solver::withinBudget() const { +inline bool Solver::withinBudget(uint64_t ammount) const { Assert (proxy); // spendResource sets async_interrupt or throws UnsafeInterruptException // depending on whether hard-limit is enabled - proxy->spendResource(); + proxy->spendResource(ammount); bool within_budget = !asynch_interrupt && (conflict_budget < 0 || conflicts < (uint64_t)conflict_budget) && diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index 9243a2b35..1508e3e35 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -424,7 +424,7 @@ protected: int trail_index (Var x) const; // Index in the trail double progressEstimate () const; // DELETE THIS ?? IT'S NOT VERY USEFUL ... public: - bool withinBudget () const; + bool withinBudget (uint64_t amount) const; protected: // Static helpers: diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index c7dae533e..e6d965f8f 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -281,8 +281,8 @@ void PropEngine::interrupt() throw(ModalException) { Debug("prop") << "interrupt()" << endl; } -void PropEngine::spendResource() throw (UnsafeInterruptException) { - d_resourceManager->spendResource(); +void PropEngine::spendResource(uint64_t ammount) throw (UnsafeInterruptException) { + d_resourceManager->spendResource(ammount); } bool PropEngine::properExplanation(TNode node, TNode expl) const { diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 2750319e6..17ac394c3 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -228,7 +228,7 @@ public: * Informs the ResourceManager that a resource has been spent. If out of * resources, can throw an UnsafeInterruptException exception. */ - void spendResource() throw (UnsafeInterruptException); + void spendResource(uint64_t ammount) throw (UnsafeInterruptException); /** * For debugging. Return true if "expl" is a well-formed diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h index 8effa8189..79758a425 100644 --- a/src/prop/sat_solver.h +++ b/src/prop/sat_solver.h @@ -97,8 +97,8 @@ public: * Notify about a learnt clause. */ virtual void notify(SatClause& clause) = 0; - virtual void spendResource() = 0; - virtual void safePoint() = 0; + virtual void spendResource(uint64_t ammount) = 0; + virtual void safePoint(uint64_t ammount) = 0; };/* class BVSatSolverInterface::Notify */ diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index 59e87dd33..5b80b7596 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -103,7 +103,7 @@ TNode TheoryProxy::getNode(SatLiteral lit) { } void TheoryProxy::notifyRestart() { - d_propEngine->spendResource(); + d_propEngine->spendResource(options::restartStep()); d_theoryEngine->notifyRestart(); static uint32_t lemmaCount = 0; @@ -179,8 +179,8 @@ void TheoryProxy::logDecision(SatLiteral lit) { #endif /* CVC4_REPLAY */ } -void TheoryProxy::spendResource() { - d_theoryEngine->spendResource(); +void TheoryProxy::spendResource(uint64_t ammount) { + d_theoryEngine->spendResource(ammount); } bool TheoryProxy::isDecisionRelevant(SatVariable var) { diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index 3565aa501..d978edefd 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -111,7 +111,7 @@ public: void logDecision(SatLiteral lit); - void spendResource(); + void spendResource(uint64_t ammount); bool isDecisionEngineDone(); diff --git a/src/smt/options b/src/smt/options index b23d73943..dbee33f5a 100644 --- a/src/smt/options +++ b/src/smt/options @@ -104,6 +104,44 @@ common-option hardLimit hard-limit --hard-limit bool :default false common-option cpuTime cpu-time --cpu-time bool :default false measures CPU time if set to true and wall time if false (default false) +# Resource spending options for SPARK +expert-option rewriteStep rewrite-step --rewrite-step uint64_t :default 1 + ammount of resources spent for each rewrite step + +expert-option theoryCheckStep theory-check-step --theory-check-step uint64_t :default 1 + ammount of resources spent for each theory check call + +expert-option decisionStep decision-step --decision-step uint64_t :default 1 + ammount of getNext decision calls in the decision engine + +expert-option bitblastStep bitblast-step --bitblast-step uint64_t :default 1 + ammount of resources spent for each bitblast step + +expert-option parseStep parse-step --parse-step uint64_t :default 1 + ammount of resources spent for each command/expression parsing + +expert-option lemmaStep lemma-step --lemma-step uint64_t :default 1 + ammount of resources spent when adding lemmas + +expert-option restartStep restart-step --restart-step uint64_t :default 1 + ammount of resources spent for each theory restart + +expert-option cnfStep cnf-step --cnf-step uint64_t :default 1 + ammount of resources spent for each call to cnf conversion + +expert-option preprocessStep preprocess-step --preprocess-step uint64_t :default 1 + ammount of resources spent for each preprocessing step in SmtEngine + +expert-option quantifierStep quantifier-step --quantifier-step uint64_t :default 1 + ammount of resources spent for quantifier instantiations + +expert-option satConflictStep sat-conflict-step --sat-conflict-step uint64_t :default 1 + ammount of resources spent for each sat conflict (main sat solver) + +expert-option bvSatConflictStep bv-sat-conflict-step --bv-sat-conflict-step uint64_t :default 1 + ammount of resources spent for each sat conflict (bitvectors) + + expert-option rewriteApplyToConst rewrite-apply-to-const --rewrite-apply-to-const bool :default false eliminate function applications, rewriting e.g. f(5) to a new symbol f_5 diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index bc594a47e..c7c0bc71a 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -492,8 +492,8 @@ public: } ResourceManager* getResourceManager() { return d_resourceManager; } - void spendResource() throw(UnsafeInterruptException) { - d_resourceManager->spendResource(); + void spendResource(uint64_t ammount) throw(UnsafeInterruptException) { + d_resourceManager->spendResource(ammount); } void nmNotifyNewSort(TypeNode tn, uint32_t flags) { @@ -1776,7 +1776,7 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_mapd_staticLearningTime); @@ -1957,7 +1957,7 @@ static void dumpAssertions(const char* key, const AssertionPipeline& assertionLi // returns false if it learns a conflict bool SmtEnginePrivate::nonClausalSimplify() { - spendResource(); + spendResource(options::preprocessStep()); d_smt.finalOptionsAreSet(); if(options::unsatCores()) { @@ -2286,7 +2286,7 @@ void SmtEnginePrivate::bvAbstraction() { void SmtEnginePrivate::bvToBool() { Trace("bv-to-bool") << "SmtEnginePrivate::bvToBool()" << endl; - spendResource(); + spendResource(options::preprocessStep()); std::vector new_assertions; d_smt.d_theoryEngine->ppBvToBool(d_assertions.ref(), new_assertions); for (unsigned i = 0; i < d_assertions.size(); ++ i) { @@ -2297,13 +2297,13 @@ void SmtEnginePrivate::bvToBool() { bool SmtEnginePrivate::simpITE() { TimerStat::CodeTimer simpITETimer(d_smt.d_stats->d_simpITETime); - spendResource(); + spendResource(options::preprocessStep()); Trace("simplify") << "SmtEnginePrivate::simpITE()" << endl; unsigned numAssertionOnEntry = d_assertions.size(); for (unsigned i = 0; i < d_assertions.size(); ++i) { - spendResource(); + spendResource(options::preprocessStep()); Node result = d_smt.d_theoryEngine->ppSimpITE(d_assertions[i]); d_assertions.replace(i, result); if(result.isConst() && !result.getConst()){ @@ -2350,7 +2350,7 @@ void SmtEnginePrivate::compressBeforeRealAssertions(size_t before){ void SmtEnginePrivate::unconstrainedSimp() { TimerStat::CodeTimer unconstrainedSimpTimer(d_smt.d_stats->d_unconstrainedSimpTime); - spendResource(); + spendResource(options::preprocessStep()); Trace("simplify") << "SmtEnginePrivate::unconstrainedSimp()" << endl; d_smt.d_theoryEngine->ppUnconstrainedSimp(d_assertions.ref()); } @@ -2799,7 +2799,7 @@ void SmtEnginePrivate::doMiplibTrick() { // returns false if simplification led to "false" bool SmtEnginePrivate::simplifyAssertions() throw(TypeCheckingException, LogicException, UnsafeInterruptException) { - spendResource(); + spendResource(options::preprocessStep()); Assert(d_smt.d_pendingPops == 0); try { ScopeCounter depth(d_simplifyAssertionsDepth); @@ -3042,7 +3042,7 @@ bool SmtEnginePrivate::checkForBadSkolems(TNode n, TNode skolem, hash_mapd_rewriteBooleanTermsTime); - spendResource(); + spendResource(options::preprocessStep()); if(d_booleanTermConverter == NULL) { // This needs to be initialized _after_ the whole SMT framework is in place, subscribed @@ -3077,7 +3077,7 @@ Node SmtEnginePrivate::rewriteBooleanTerms(TNode n) { void SmtEnginePrivate::processAssertions() { TimerStat::CodeTimer paTimer(d_smt.d_stats->d_processAssertionsTime); - spendResource(); + spendResource(options::preprocessStep()); Assert(d_smt.d_fullyInited); Assert(d_smt.d_pendingPops == 0); @@ -3199,7 +3199,7 @@ void SmtEnginePrivate::processAssertions() { << "applying substitutions" << endl; for (unsigned i = 0; i < d_assertions.size(); ++ i) { Trace("simplify") << "applying to " << d_assertions[i] << endl; - spendResource(); + spendResource(options::preprocessStep()); d_assertions.replace(i, Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertions[i]))); Trace("simplify") << " got " << d_assertions[i] << endl; } @@ -3759,7 +3759,7 @@ Expr SmtEngine::simplify(const Expr& ex) throw(TypeCheckingException, LogicExcep } Expr SmtEngine::expandDefinitions(const Expr& ex) throw(TypeCheckingException, LogicException, UnsafeInterruptException) { - d_private->spendResource(); + d_private->spendResource(options::preprocessStep()); Assert(ex.getExprManager() == d_exprManager); SmtScope smts(this); diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 7b5b40c8b..565c69514 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -18,6 +18,7 @@ #include "theory/arith/theory_arith.h" #include "theory/arith/theory_arith_private.h" #include "theory/arith/infer_bounds.h" +#include "smt/options.h" using namespace std; using namespace CVC4::kind; @@ -70,6 +71,7 @@ void TheoryArith::ppStaticLearn(TNode n, NodeBuilder<>& learned) { } void TheoryArith::check(Effort effortLevel){ + getOutputChannel().spendResource(options::theoryCheckStep()); d_internal->check(effortLevel); } 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) { diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h index d4d7bc04c..4d953b03c 100644 --- a/src/theory/bv/bitblaster_template.h +++ b/src/theory/bv/bitblaster_template.h @@ -135,8 +135,8 @@ class TLazyBitblaster : public TBitblaster { {} bool notify(prop::SatLiteral lit); void notify(prop::SatClause& clause); - void spendResource(); - void safePoint(); + void spendResource(uint64_t ammount); + void safePoint(uint64_t ammount); }; TheoryBV *d_bv; @@ -240,10 +240,10 @@ public: MinisatEmptyNotify() {} bool notify(prop::SatLiteral lit) { return true; } void notify(prop::SatClause& clause) { } - void spendResource() { - NodeManager::currentResourceManager()->spendResource(); + void spendResource(uint64_t ammount) { + NodeManager::currentResourceManager()->spendResource(ammount); } - void safePoint() {} + void safePoint(uint64_t ammount) {} }; diff --git a/src/theory/bv/bv_eager_solver.cpp b/src/theory/bv/bv_eager_solver.cpp index 57a635c20..0c087ddb9 100644 --- a/src/theory/bv/bv_eager_solver.cpp +++ b/src/theory/bv/bv_eager_solver.cpp @@ -67,7 +67,7 @@ bool EagerBitblastSolver::isInitialized() { } void EagerBitblastSolver::assertFormula(TNode formula) { - d_bv->spendResource(); + d_bv->spendResource(1); Assert (isInitialized()); Debug("bitvector-eager") << "EagerBitblastSolver::assertFormula "<< formula <<"\n"; d_assertionSet.insert(formula); diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp index c86572ead..7e3ed46c8 100644 --- a/src/theory/bv/bv_subtheory_bitblast.cpp +++ b/src/theory/bv/bv_subtheory_bitblast.cpp @@ -152,7 +152,7 @@ bool BitblastSolver::check(Theory::Effort e) { // We need to ensure we are fully propagated, so propagate now if (d_useSatPropagation) { - d_bv->spendResource(); + d_bv->spendResource(1); bool ok = d_bitblaster->propagate(); if (!ok) { std::vector conflictAtoms; diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp index 9481b9894..13c31463b 100644 --- a/src/theory/bv/bv_subtheory_core.cpp +++ b/src/theory/bv/bv_subtheory_core.cpp @@ -21,6 +21,7 @@ #include "theory/bv/slicer.h" #include "theory/theory_model.h" #include "theory/bv/options.h" +#include "smt/options.h" using namespace std; using namespace CVC4; @@ -167,7 +168,7 @@ bool CoreSolver::decomposeFact(TNode fact) { bool CoreSolver::check(Theory::Effort e) { Trace("bitvector::core") << "CoreSolver::check \n"; - d_bv->spendResource(); + d_bv->spendResource(options::theoryCheckStep()); d_checkCalled = true; Assert (!d_bv->inConflict()); diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp index 660551fe2..55dcbb03a 100644 --- a/src/theory/bv/bv_subtheory_inequality.cpp +++ b/src/theory/bv/bv_subtheory_inequality.cpp @@ -18,6 +18,7 @@ #include "theory/bv/theory_bv.h" #include "theory/bv/theory_bv_utils.h" #include "theory/theory_model.h" +#include "smt/options.h" using namespace std; using namespace CVC4; @@ -29,7 +30,7 @@ using namespace CVC4::theory::bv::utils; bool InequalitySolver::check(Theory::Effort e) { Debug("bv-subtheory-inequality") << "InequalitySolveR::check("<< e <<")\n"; ++(d_statistics.d_numCallstoCheck); - d_bv->spendResource(); + d_bv->spendResource(options::theoryCheckStep()); bool ok = true; while (!done() && ok) { diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp index 065d5d5ef..eca9f12ab 100644 --- a/src/theory/bv/eager_bitblaster.cpp +++ b/src/theory/bv/eager_bitblaster.cpp @@ -103,7 +103,7 @@ void EagerBitblaster::bbTerm(TNode node, Bits& bits) { return; } - d_bv->spendResource(); + d_bv->spendResource(options::bitblastStep()); Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n"; d_termBBStrategies[node.getKind()] (node, bits, this); diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp index 080f23143..61472fd79 100644 --- a/src/theory/bv/lazy_bitblaster.cpp +++ b/src/theory/bv/lazy_bitblaster.cpp @@ -170,7 +170,7 @@ void TLazyBitblaster::bbTerm(TNode node, Bits& bits) { return; } - d_bv->spendResource(); + d_bv->spendResource(options::bitblastStep()); Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n"; ++d_statistics.d_numTerms; @@ -356,12 +356,12 @@ void TLazyBitblaster::MinisatNotify::notify(prop::SatClause& clause) { } } -void TLazyBitblaster::MinisatNotify::spendResource() { - d_bv->spendResource(); +void TLazyBitblaster::MinisatNotify::spendResource(uint64_t ammount) { + d_bv->spendResource(ammount); } -void TLazyBitblaster::MinisatNotify::safePoint() { - d_bv->d_out->safePoint(); +void TLazyBitblaster::MinisatNotify::safePoint(uint64_t ammount) { + d_bv->d_out->safePoint(ammount); } diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 9dcd5ac62..6f399cb7a 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -107,8 +107,8 @@ void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine* eq) { } } -void TheoryBV::spendResource() throw(UnsafeInterruptException) { - getOutputChannel().spendResource(); +void TheoryBV::spendResource(uint64_t ammount) throw(UnsafeInterruptException) { + getOutputChannel().spendResource(ammount); } TheoryBV::Statistics::Statistics(): diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 11d8cb895..3317d1b01 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -103,7 +103,7 @@ private: Statistics d_statistics; - void spendResource() throw(UnsafeInterruptException); + void spendResource(uint64_t ammount) throw(UnsafeInterruptException); /** * Return the uninterpreted function symbol corresponding to division-by-zero diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index bef39f536..f340c994c 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -86,7 +86,7 @@ public: * With safePoint(), the theory signals that it is at a safe point * and can be interrupted. */ - virtual void safePoint() throw(Interrupted, UnsafeInterruptException, AssertionException) { + virtual void safePoint(uint64_t ammount) throw(Interrupted, UnsafeInterruptException, AssertionException) { } /** @@ -213,7 +213,7 @@ public: * long-running operations, they cannot rely on resource() to break * out of infinite or intractable computations. */ - virtual void spendResource() throw(UnsafeInterruptException) {} + virtual void spendResource(uint64_t ammount) throw(UnsafeInterruptException) {} /** * Handle user attribute. diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index afc607470..2177ebc32 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -767,7 +767,7 @@ bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool mkRep, bool bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& terms, bool mkRep, bool modEq, bool modInst ) { // For resource-limiting (also does a time check). - getOutputChannel().safePoint(); + getOutputChannel().safePoint(options::quantifierStep()); Assert( terms.size()==f[0].getNumChildren() ); Trace("inst-add-debug") << "Add instantiation: "; diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index a940bcc3d..842df69c5 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -116,7 +116,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { if (hasSmtEngine && d_iterationCount % ResourceManager::getFrequencyCount() == 0) { - rm->spendResource(); + rm->spendResource(options::rewriteStep()); d_iterationCount = 0; } diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index bbeec5125..75dafb7f6 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1756,6 +1756,6 @@ std::pair TheoryEngine::entailmentCheck(theory::TheoryOfMode mode, T return th->entailmentCheck(lit, params, seffects); } -void TheoryEngine::spendResource() { - d_resourceManager->spendResource(); +void TheoryEngine::spendResource(uint64_t ammount) { + d_resourceManager->spendResource(ammount); } diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 8aedc65f0..bb4d4c16d 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -282,8 +282,8 @@ class TheoryEngine { { } - void safePoint() throw(theory::Interrupted, UnsafeInterruptException, AssertionException) { - spendResource(); + void safePoint(uint64_t ammount) throw(theory::Interrupted, UnsafeInterruptException, AssertionException) { + spendResource(ammount); if (d_engine->d_interrupted) { throw theory::Interrupted(); } @@ -347,8 +347,8 @@ class TheoryEngine { d_engine->setIncomplete(d_theory); } - void spendResource() throw(UnsafeInterruptException) { - d_engine->spendResource(); + void spendResource(uint64_t ammount) throw(UnsafeInterruptException) { + d_engine->spendResource(ammount); } void handleUserAttribute( const char* attr, theory::Theory* t ){ @@ -488,7 +488,7 @@ public: /** * "Spend" a resource during a search or preprocessing. */ - void spendResource(); + void spendResource(uint64_t ammount); /** * Adds a theory. Only one theory per TheoryId can be present, so if diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h index 46a717cc5..6fe92eb6e 100644 --- a/src/theory/theory_test_utils.h +++ b/src/theory/theory_test_utils.h @@ -69,7 +69,7 @@ public: ~TestOutputChannel() {} - void safePoint() throw(Interrupted, AssertionException) {} + void safePoint(uint64_t ammount) throw(Interrupted, AssertionException) {} void conflict(TNode n) throw(AssertionException, UnsafeInterruptException) { diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index b00fdd6ee..073399894 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -17,6 +17,7 @@ #include "theory/uf/theory_uf.h" #include "theory/uf/options.h" +#include "smt/options.h" #include "theory/quantifiers/options.h" #include "theory/uf/theory_uf_strong_solver.h" #include "theory/theory_model.h" @@ -92,7 +93,7 @@ void TheoryUF::check(Effort level) { if (done() && !fullEffort(level)) { return; } - + getOutputChannel().spendResource(options::theoryCheckStep()); TimerStat::CodeTimer checkTimer(d_checkTime); while (!done() && !d_conflict) diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp index 6d32120d9..37fea2c67 100644 --- a/src/util/resource_manager.cpp +++ b/src/util/resource_manager.cpp @@ -170,13 +170,13 @@ uint64_t ResourceManager::getTimeRemaining() const { return d_thisCallTimeBudget - time_passed; } -void ResourceManager::spendResource() throw (UnsafeInterruptException) { +void ResourceManager::spendResource(uint64_t ammount) throw (UnsafeInterruptException) { ++d_spendResourceCalls; - ++d_cumulativeResourceUsed; + d_cumulativeResourceUsed += ammount; if (!d_on) return; Debug("limit") << "ResourceManager::spendResource()" << std::endl; - ++d_thisCallResourceUsed; + d_thisCallResourceUsed += ammount; if(out()) { Trace("limit") << "ResourceManager::spendResource: interrupt!" << std::endl; Trace("limit") << " on call " << d_spendResourceCalls << std::endl; diff --git a/src/util/resource_manager.h b/src/util/resource_manager.h index d1ec0456a..9c2812f0f 100644 --- a/src/util/resource_manager.h +++ b/src/util/resource_manager.h @@ -128,7 +128,7 @@ public: return d_thisCallResourceBudget; } - void spendResource() throw(UnsafeInterruptException); + void spendResource(uint64_t ammount) throw(UnsafeInterruptException); void setHardLimit(bool value); void setResourceLimit(uint64_t units, bool cumulative = false); -- 2.30.2