From: Andrew Reynolds Date: Thu, 4 Oct 2018 17:21:16 +0000 (-0500) Subject: Clean remaining references to getNextDecisionRequest and simplify (#2500) X-Git-Tag: cvc5-1.0.0~4460 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7b76222cacbdb906dca1543b53e0f113dc1e1826;p=cvc5.git Clean remaining references to getNextDecisionRequest and simplify (#2500) --- diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index a04c12903..3313a684f 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -40,7 +40,6 @@ # notifyRestart the theory supports notifyRestart() # presolve the theory supports presolve() # postsolve the theory supports postsolve() -# getNextDecisionRequest the theory supports getNextDecisionRequest() # # In the case of the "theory-supports-function" properties, you # need to declare these for your theory or the functions will not diff --git a/src/theory/decision_manager.cpp b/src/theory/decision_manager.cpp index 3cc67fe6d..5c43e6159 100644 --- a/src/theory/decision_manager.cpp +++ b/src/theory/decision_manager.cpp @@ -38,7 +38,7 @@ void DecisionManager::registerStrategy(StrategyId id, DecisionStrategy* ds) d_reg_strategy[id].push_back(ds); } -Node DecisionManager::getNextDecisionRequest(unsigned& priority) +Node DecisionManager::getNextDecisionRequest() { Trace("dec-manager-debug") << "DecisionManager: Get next decision..." << std::endl; @@ -51,10 +51,6 @@ Node DecisionManager::getNextDecisionRequest(unsigned& priority) Node lit = ds->getNextDecisionRequest(); if (!lit.isNull()) { - StrategyId sid = rs.first; - priority = sid < STRAT_LAST_M_SOUND - ? 0 - : (sid < STRAT_LAST_FM_COMPLETE ? 1 : 2); Trace("dec-manager") << "DecisionManager: -> literal " << lit << " decided by strategy " << ds->identify() << std::endl; diff --git a/src/theory/decision_manager.h b/src/theory/decision_manager.h index 7ac27a531..fbc0e2cd6 100644 --- a/src/theory/decision_manager.h +++ b/src/theory/decision_manager.h @@ -105,11 +105,8 @@ class DecisionManager * returns null, then no decisions are required by a decision strategy * registered to this class. In the latter case, the SAT solver will choose * a decision based on its given heuristic. - * - * The argument priority has the same role as in - * Theory::getNextDecisionRequest. */ - Node getNextDecisionRequest(unsigned& priorty); + Node getNextDecisionRequest(); private: /** Map containing all strategies registered to this manager */ diff --git a/src/theory/mktheorytraits b/src/theory/mktheorytraits index 15166fc1f..456a4b0ea 100755 --- a/src/theory/mktheorytraits +++ b/src/theory/mktheorytraits @@ -53,7 +53,6 @@ theory_has_ppStaticLearn="false" theory_has_notifyRestart="false" theory_has_presolve="false" theory_has_postsolve="false" -theory_has_getNextDecisionRequest="false" theory_stable_infinite="false" theory_finite="false" @@ -177,14 +176,13 @@ struct TheoryTraits<${theory_id}> { static const bool hasNotifyRestart = ${theory_has_notifyRestart}; static const bool hasPresolve = ${theory_has_presolve}; static const bool hasPostsolve = ${theory_has_postsolve}; - static const bool hasGetNextDecisionRequest = ${theory_has_getNextDecisionRequest}; };/* struct TheoryTraits<${theory_id}> */ " # warnings about theory content and properties dir="$(dirname "$kf")/../../" if [ -e "$dir/$theory_header" ]; then - for function in check propagate ppStaticLearn notifyRestart presolve postsolve getNextDecisionRequest; do + for function in check propagate ppStaticLearn notifyRestart presolve postsolve; do if eval "\$theory_has_$function"; then grep '\<'"$function"' *\((\|;\)' "$dir/$theory_header" | grep -vq '^ */\(/\|\*\)' || echo "$kf: warning: $theory_class has property \"$function\" in its kinds file but doesn't appear to declare the function" >&2 @@ -203,7 +201,6 @@ struct TheoryTraits<${theory_id}> { theory_has_notifyRestart="false" theory_has_presolve="false" theory_has_postsolve="false" - theory_has_getNextDecisionRequest="false" theory_stable_infinite="false" theory_finite="false" @@ -286,7 +283,6 @@ function properties { ppStaticLearn) theory_has_ppStaticLearn="true";; presolve) theory_has_presolve="true";; postsolve) theory_has_postsolve="true";; - getNextDecisionRequest) theory_has_getNextDecisionRequest="true";; notifyRestart) theory_has_notifyRestart="true";; *) echo "$kf:$lineno: error: unknown theory property \"$property\"" >&2; exit 1;; esac diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index de4a013cd..7fb2d26c6 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -6,7 +6,7 @@ theory THEORY_STRINGS ::CVC4::theory::strings::TheoryStrings "theory/strings/theory_strings.h" -properties check parametric propagate getNextDecisionRequest presolve +properties check parametric propagate presolve rewriter ::CVC4::theory::strings::TheoryStringsRewriter "theory/strings/theory_strings_rewriter.h" diff --git a/src/theory/theory.h b/src/theory/theory.h index 534f091bf..8a0c87c9e 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -532,16 +532,6 @@ public: virtual bool collectModelInfo(TheoryModel* m) { return true; } /** if theories want to do something with model after building, do it here */ virtual void postProcessModel( TheoryModel* m ){ } - /** - * Return a decision request, if the theory has one, or the NULL node - * otherwise. - * If returning non-null node, should set priority to - * 0 if decision is necessary for model-soundness, - * 1 if decision is necessary for completeness, - * >1 otherwise. - */ - virtual Node getNextDecisionRequest( unsigned& priority ) { return Node(); } - /** * Statically learn from assertion "in," which has been asserted * true at the top level. The theory should only add (via diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index b9c3ccc4e..54ac272cc 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -767,28 +767,9 @@ void TheoryEngine::propagate(Theory::Effort effort) { } } -Node TheoryEngine::getNextDecisionRequest() { - unsigned min_priority = 0; - Node dec = d_decManager->getNextDecisionRequest(min_priority); - - // Definition of the statement that is to be run by every theory -#ifdef CVC4_FOR_EACH_THEORY_STATEMENT -#undef CVC4_FOR_EACH_THEORY_STATEMENT -#endif -#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ - if (theory::TheoryTraits::hasGetNextDecisionRequest && d_logicInfo.isTheoryEnabled(THEORY)) { \ - unsigned priority; \ - Node n = theoryOf(THEORY)->getNextDecisionRequest( priority ); \ - if(! n.isNull() && ( dec.isNull() || prioritygetNextDecisionRequest(); } bool TheoryEngine::properConflict(TNode conflict) const { diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index b5ac208d7..09f986686 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -702,6 +702,12 @@ public: } } + /** + * Returns the next decision request, or null if none exist. The next + * decision request is a literal that this theory engine prefers the SAT + * solver to make as its next decision. Decision requests are managed by + * the decision manager d_decManager. + */ Node getNextDecisionRequest(); bool properConflict(TNode conflict) const;