From: Andrew Reynolds Date: Thu, 19 Sep 2019 14:44:04 +0000 (-0500) Subject: Support context-(in)dependent decision strategies. (#3281) X-Git-Tag: cvc5-1.0.0~3938 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7988675ce9666b6f2214b583d42b9fa8be52ae60;p=cvc5.git Support context-(in)dependent decision strategies. (#3281) --- diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 9f06950bd..003bb0d68 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -112,7 +112,8 @@ TheoryArrays::TheoryArrays(context::Context* c, d_arrayMerges(c), d_inCheckModel(false), d_proofReconstruction(&d_equalityEngine), - d_dstrat(new TheoryArraysDecisionStrategy(this)) + d_dstrat(new TheoryArraysDecisionStrategy(this)), + d_dstratInit(false) { smtStatisticsRegistry()->registerStat(&d_numRow); smtStatisticsRegistry()->registerStat(&d_numExt); @@ -1252,9 +1253,15 @@ bool TheoryArrays::collectModelInfo(TheoryModel* m) void TheoryArrays::presolve() { Trace("arrays")<<"Presolving \n"; - // add the decision strategy - getDecisionManager()->registerStrategy(DecisionManager::STRAT_ARRAYS, - d_dstrat.get()); + if (!d_dstratInit) + { + d_dstratInit = true; + // add the decision strategy, which is user-context-independent + getDecisionManager()->registerStrategy( + DecisionManager::STRAT_ARRAYS, + d_dstrat.get(), + DecisionManager::STRAT_SCOPE_CTX_INDEPENDENT); + } } diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index be80a081d..3d6d0692e 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -474,6 +474,8 @@ class TheoryArrays : public Theory { }; /** an instance of the above decision strategy */ std::unique_ptr d_dstrat; + /** Have we registered the above strategy? (context-independent) */ + bool d_dstratInit; /** get the next decision request * * If the "arrays-eager-index" option is enabled, then whenever a diff --git a/src/theory/decision_manager.cpp b/src/theory/decision_manager.cpp index 3eda45b00..a2aee5d40 100644 --- a/src/theory/decision_manager.cpp +++ b/src/theory/decision_manager.cpp @@ -22,27 +22,68 @@ using namespace CVC4::kind; namespace CVC4 { namespace theory { -DecisionManager::DecisionManager(context::Context* satContext) {} +DecisionManager::DecisionManager(context::Context* userContext) + : d_strategyCacheC(userContext) +{ +} -void DecisionManager::reset() +void DecisionManager::presolve() { - Trace("dec-manager") << "DecisionManager: reset." << std::endl; + Trace("dec-manager") << "DecisionManager: presolve." << std::endl; + // remove the strategies that are not in this user context + std::unordered_set active; + for (DecisionStrategyList::const_iterator i = d_strategyCacheC.begin(); + i != d_strategyCacheC.end(); + ++i) + { + active.insert(*i); + } + active.insert(d_strategyCache.begin(), d_strategyCache.end()); + std::map > tmp = d_reg_strategy; d_reg_strategy.clear(); + for (std::pair >& rs : tmp) + { + for (DecisionStrategy* ds : rs.second) + { + if (active.find(ds) != active.end()) + { + // if its active, we keep it + d_reg_strategy[rs.first].push_back(ds); + } + } + } } -void DecisionManager::registerStrategy(StrategyId id, DecisionStrategy* ds) +void DecisionManager::registerStrategy(StrategyId id, + DecisionStrategy* ds, + StrategyScope sscope) { Trace("dec-manager") << "DecisionManager: Register strategy : " << ds->identify() << ", id = " << id << std::endl; ds->initialize(); d_reg_strategy[id].push_back(ds); + if (sscope == STRAT_SCOPE_USER_CTX_DEPENDENT) + { + // store it in the user-context-dependent list + d_strategyCacheC.push_back(ds); + } + else if (sscope == STRAT_SCOPE_CTX_INDEPENDENT) + { + // it is context independent + d_strategyCache.insert(ds); + } + else + { + // it is local to this call, we don't cache it + Assert(sscope == STRAT_SCOPE_LOCAL_SOLVE); + } } Node DecisionManager::getNextDecisionRequest() { Trace("dec-manager-debug") << "DecisionManager: Get next decision..." << std::endl; - for (const std::pair >& rs : + for (const std::pair >& rs : d_reg_strategy) { for (unsigned i = 0, size = rs.second.size(); i < size; i++) diff --git a/src/theory/decision_manager.h b/src/theory/decision_manager.h index 6825c1cf4..da040a7f7 100644 --- a/src/theory/decision_manager.h +++ b/src/theory/decision_manager.h @@ -19,6 +19,7 @@ #define CVC4__THEORY__DECISION_MANAGER__H #include +#include "context/cdlist.h" #include "theory/decision_strategy.h" namespace CVC4 { @@ -46,6 +47,8 @@ namespace theory { */ class DecisionManager { + typedef context::CDList DecisionStrategyList; + public: enum StrategyId { @@ -83,21 +86,42 @@ class DecisionManager STRAT_LAST }; - DecisionManager(context::Context* satContext); + /** The scope of a strategy, used in registerStrategy below */ + enum StrategyScope + { + // The strategy is user-context dependent, that is, it is cleared when + // the user context is popped. + STRAT_SCOPE_USER_CTX_DEPENDENT, + // The strategy is local to a check-sat call, that is, it is cleared on + // a call to presolve. + STRAT_SCOPE_LOCAL_SOLVE, + // The strategy is context-independent. + STRAT_SCOPE_CTX_INDEPENDENT, + }; + DecisionManager(context::Context* userContext); ~DecisionManager() {} - /** reset the strategy + /** presolve * - * This clears all decision strategies that are registered to this manager. + * This clears all decision strategies that are registered to this manager + * that no longer exist in the current user context. * We require that each satisfiability check beyond the first calls this - * function exactly once. Currently, it is called during - * TheoryEngine::postSolve. + * function exactly once. It is called during TheoryEngine::presolve. */ - void reset(); + void presolve(); /** * Registers the strategy ds with this manager. The id specifies when the - * strategy should be run. + * strategy should be run. The argument sscope indicates the scope of the + * strategy, i.e. how long it persists. + * + * Typically, strategies that are user-context-dependent are those that are + * in response to an assertion (e.g. a strategy that decides that a sygus + * conjecture is feasible). An example of a strategy that is context + * independent is the combined cardinality decision strategy for finite model + * finding for UF, which is not specific to any formula/type. */ - void registerStrategy(StrategyId id, DecisionStrategy* ds); + void registerStrategy(StrategyId id, + DecisionStrategy* ds, + StrategyScope sscope = STRAT_SCOPE_USER_CTX_DEPENDENT); /** Get the next decision request * * If this method returns a non-null node n, then n is a literal corresponding @@ -111,6 +135,10 @@ class DecisionManager private: /** Map containing all strategies registered to this manager */ std::map > d_reg_strategy; + /** Set of decision strategies in this user context */ + DecisionStrategyList d_strategyCacheC; + /** Set of decision strategies that are context independent */ + std::unordered_set d_strategyCache; }; } // namespace theory diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 65f06c008..0f9a78516 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -570,8 +570,12 @@ void TheoryStrings::presolve() { inputVars.push_back(*itr); } d_sslds->initialize(inputVars); + // This strategy is local to a check-sat call, since we refresh the strategy + // on every call to presolve. getDecisionManager()->registerStrategy( - DecisionManager::STRAT_STRINGS_SUM_LENGTHS, d_sslds.get()); + DecisionManager::STRAT_STRINGS_SUM_LENGTHS, + d_sslds.get(), + DecisionManager::STRAT_SCOPE_LOCAL_SOLVE); } } diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 8348c24d5..5d185ad9d 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -274,7 +274,7 @@ TheoryEngine::TheoryEngine(context::Context* context, d_masterEqualityEngine(nullptr), d_masterEENotify(*this), d_quantEngine(nullptr), - d_decManager(new DecisionManager(context)), + d_decManager(new DecisionManager(userContext)), d_curr_model(nullptr), d_aloc_curr_model(false), d_curr_model_builder(nullptr), @@ -910,6 +910,10 @@ bool TheoryEngine::presolve() { // Reset the interrupt flag d_interrupted = false; + // Reset the decision manager. This clears its decision strategies that are + // no longer valid in this user context. + d_decManager->presolve(); + try { // Definition of the statement that is to be run by every theory #ifdef CVC4_FOR_EACH_THEORY_STATEMENT @@ -933,9 +937,6 @@ bool TheoryEngine::presolve() { }/* TheoryEngine::presolve() */ void TheoryEngine::postsolve() { - // Reset the decision manager. This clears its decision strategies, which are - // user-context-dependent. - d_decManager->reset(); // no longer in SAT mode d_inSatMode = false; // Reset the interrupt flag diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp index 94e5f67c1..87696ef5f 100644 --- a/src/theory/uf/cardinality_extension.cpp +++ b/src/theory/uf/cardinality_extension.cpp @@ -504,6 +504,8 @@ void SortModel::initialize( OutputChannel* out ){ if (d_c_dec_strat.get() != nullptr && !d_initialized) { d_initialized = true; + // Strategy is user-context-dependent, since it is in sync with + // user-context-dependent flag d_initialized. d_thss->getTheory()->getDecisionManager()->registerStrategy( DecisionManager::STRAT_UF_CARD, d_c_dec_strat.get()); } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index c456ed2e8..a97670446 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1820,6 +1820,7 @@ set(regress_2_tests regress2/strings/norn-dis-0707-3.smt2 regress2/strings/range-perf.smt2 regress2/strings/repl-repl.smt2 + regress2/strings/repl-repl-i-no-push.smt2 regress2/strings/replaceall-diffrange.smt2 regress2/strings/replaceall-len-c.smt2 regress2/strings/small-1.smt2 diff --git a/test/regress/regress2/strings/repl-repl-i-no-push.smt2 b/test/regress/regress2/strings/repl-repl-i-no-push.smt2 new file mode 100644 index 000000000..0076af392 --- /dev/null +++ b/test/regress/regress2/strings/repl-repl-i-no-push.smt2 @@ -0,0 +1,26 @@ +; COMMAND-LINE: --strings-exp --strings-fmf --incremental +; EXPECT: sat +; EXPECT: unsat +; EXPECT: sat +; EXPECT: sat +(set-logic SLIA) +(declare-const x String) +(declare-const y String) +(declare-const z String) + +(assert (not (= (str.replace (str.replace x "B" x) x "AB") (str.replace (str.replace x "B" "AB") x "AB")))) +(check-sat) + +(push 1) +(assert (not (= (str.replace (str.replace x "B" x) x "A") (str.replace (str.replace x "B" "A") x "A")))) +(check-sat) +(pop 1) + +(push 1) +(assert (not (= (str.replace (str.replace x z x) x y) (str.replace (str.replace x z y) x y)))) +(check-sat) +(pop 1) + +(assert (not (= (str.replace (str.replace x z x) x y) (str.replace (str.replace x z y) x y)))) +(assert (<= (str.len y) (str.len z))) +(check-sat)