From 5712bdcd06a9f9502c3b5487386e1277702e25f4 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 4 Oct 2021 13:32:20 -0500 Subject: [PATCH] Make decision engine use env (#7300) --- src/decision/decision_engine.cpp | 16 +++++--------- src/decision/decision_engine.h | 8 +++---- src/decision/decision_engine_old.cpp | 11 ++++------ src/decision/decision_engine_old.h | 4 +--- src/decision/decision_strategy.h | 28 ++++++++++-------------- src/decision/justification_heuristic.cpp | 26 ++++++++++------------ src/decision/justification_heuristic.h | 4 +--- src/decision/justification_strategy.cpp | 21 +++++++++--------- src/decision/justification_strategy.h | 5 +---- src/prop/prop_engine.cpp | 9 ++++---- src/smt/env.cpp | 4 ++-- src/smt/env_obj.cpp | 9 ++++++-- src/smt/env_obj.h | 9 +++++--- 13 files changed, 69 insertions(+), 85 deletions(-) diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp index 5b65951a6..3011ad6ec 100644 --- a/src/decision/decision_engine.cpp +++ b/src/decision/decision_engine.cpp @@ -17,16 +17,14 @@ #include "decision/decision_engine_old.h" #include "options/decision_options.h" #include "prop/sat_solver.h" +#include "smt/env.h" #include "util/resource_manager.h" namespace cvc5 { namespace decision { -DecisionEngine::DecisionEngine(context::Context* c, ResourceManager* rm) - : d_context(c), - d_resourceManager(rm), - d_cnfStream(nullptr), - d_satSolver(nullptr) +DecisionEngine::DecisionEngine(Env& env) + : EnvObj(env), d_cnfStream(nullptr), d_satSolver(nullptr) { } @@ -38,15 +36,11 @@ void DecisionEngine::finishInit(CDCLTSatSolverInterface* ss, CnfStream* cs) prop::SatLiteral DecisionEngine::getNext(bool& stopSearch) { - d_resourceManager->spendResource(Resource::DecisionStep); + resourceManager()->spendResource(Resource::DecisionStep); return getNextInternal(stopSearch); } -DecisionEngineEmpty::DecisionEngineEmpty(context::Context* sc, - ResourceManager* rm) - : DecisionEngine(sc, rm) -{ -} +DecisionEngineEmpty::DecisionEngineEmpty(Env& env) : DecisionEngine(env) {} bool DecisionEngineEmpty::isDone() { return false; } void DecisionEngineEmpty::addAssertion(TNode assertion) {} void DecisionEngineEmpty::addSkolemDefinition(TNode lem, TNode skolem) {} diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h index aa4c43e89..331d6eaca 100644 --- a/src/decision/decision_engine.h +++ b/src/decision/decision_engine.h @@ -22,16 +22,16 @@ #include "prop/cnf_stream.h" #include "prop/sat_solver.h" #include "prop/sat_solver_types.h" +#include "smt/env_obj.h" namespace cvc5 { namespace decision { -class DecisionEngine +class DecisionEngine : protected EnvObj { public: /** Constructor */ - DecisionEngine(context::Context* sc, - ResourceManager* rm); + DecisionEngine(Env& env); virtual ~DecisionEngine() {} /** Finish initialize */ @@ -86,7 +86,7 @@ class DecisionEngine class DecisionEngineEmpty : public DecisionEngine { public: - DecisionEngineEmpty(context::Context* sc, ResourceManager* rm); + DecisionEngineEmpty(Env& env); bool isDone() override; void addAssertion(TNode assertion) override; void addSkolemDefinition(TNode lem, TNode skolem) override; diff --git a/src/decision/decision_engine_old.cpp b/src/decision/decision_engine_old.cpp index 6bfba35ee..c61069cae 100644 --- a/src/decision/decision_engine_old.cpp +++ b/src/decision/decision_engine_old.cpp @@ -25,11 +25,9 @@ using namespace std; namespace cvc5 { -DecisionEngineOld::DecisionEngineOld(context::Context* sc, - context::UserContext* uc, - ResourceManager* rm) - : DecisionEngine(sc, rm), - d_result(sc, SAT_VALUE_UNKNOWN), +DecisionEngineOld::DecisionEngineOld(Env& env) + : DecisionEngine(env), + d_result(context(), SAT_VALUE_UNKNOWN), d_engineState(0), d_enabledITEStrategy(nullptr), d_decisionStopOnly(options::decisionMode() @@ -47,8 +45,7 @@ DecisionEngineOld::DecisionEngineOld(context::Context* sc, if (options::decisionMode() == options::DecisionMode::JUSTIFICATION) { - d_enabledITEStrategy.reset( - new decision::JustificationHeuristic(this, uc, sc)); + d_enabledITEStrategy.reset(new decision::JustificationHeuristic(env, this)); } } diff --git a/src/decision/decision_engine_old.h b/src/decision/decision_engine_old.h index 93f581143..f1a340ca0 100644 --- a/src/decision/decision_engine_old.h +++ b/src/decision/decision_engine_old.h @@ -39,9 +39,7 @@ class DecisionEngineOld : public decision::DecisionEngine // Necessary functions /** Constructor */ - DecisionEngineOld(context::Context* sc, - context::UserContext* uc, - ResourceManager* rm); + DecisionEngineOld(Env& env); /** Destructor, currently does nothing */ ~DecisionEngineOld() diff --git a/src/decision/decision_strategy.h b/src/decision/decision_strategy.h index 87c463c29..e8f7683fd 100644 --- a/src/decision/decision_strategy.h +++ b/src/decision/decision_strategy.h @@ -22,39 +22,35 @@ #include "expr/node.h" #include "prop/sat_solver_types.h" +#include "smt/env_obj.h" #include "smt/term_formula_removal.h" namespace cvc5 { class DecisionEngineOld; -namespace context { - class Context; - } // namespace context - namespace decision { - -class DecisionEngine; - -class DecisionStrategy { -protected: - DecisionEngineOld* d_decisionEngine; -public: - DecisionStrategy(DecisionEngineOld* de, context::Context* c) - : d_decisionEngine(de) - { +class DecisionStrategy : protected EnvObj +{ + public: + DecisionStrategy(Env& env, DecisionEngineOld* de) + : EnvObj(env), d_decisionEngine(de) + { } virtual ~DecisionStrategy() { } virtual prop::SatLiteral getNext(bool&) = 0; + + protected: + DecisionEngineOld* d_decisionEngine; };/* class DecisionStrategy */ class ITEDecisionStrategy : public DecisionStrategy { public: - ITEDecisionStrategy(DecisionEngineOld* de, context::Context* c) - : DecisionStrategy(de, c) + ITEDecisionStrategy(Env& env, DecisionEngineOld* de) + : DecisionStrategy(env, de) { } /** diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp index dcf8975bb..e04de9ce1 100644 --- a/src/decision/justification_heuristic.cpp +++ b/src/decision/justification_heuristic.cpp @@ -34,28 +34,26 @@ using namespace cvc5::prop; namespace cvc5 { namespace decision { -JustificationHeuristic::JustificationHeuristic(DecisionEngineOld* de, - context::UserContext* uc, - context::Context* c) - : ITEDecisionStrategy(de, c), - d_justified(c), - d_exploredThreshold(c), - d_prvsIndex(c, 0), - d_threshPrvsIndex(c, 0), +JustificationHeuristic::JustificationHeuristic(Env& env, DecisionEngineOld* de) + : ITEDecisionStrategy(env, de), + d_justified(context()), + d_exploredThreshold(context()), + d_prvsIndex(context(), 0), + d_threshPrvsIndex(context(), 0), d_helpfulness( smtStatisticsRegistry().registerInt("decision::jh::helpfulness")), d_giveup(smtStatisticsRegistry().registerInt("decision::jh::giveup")), d_timestat(smtStatisticsRegistry().registerTimer("decision::jh::time")), - d_assertions(uc), - d_skolemAssertions(uc), - d_skolemCache(uc), + d_assertions(userContext()), + d_skolemAssertions(userContext()), + d_skolemCache(userContext()), d_visited(), d_visitedComputeSkolems(), d_curDecision(), d_curThreshold(0), - d_childCache(uc), - d_weightCache(uc), - d_startIndexCache(c) + d_childCache(userContext()), + d_weightCache(userContext()), + d_startIndexCache(context()) { Trace("decision") << "Justification heuristic enabled" << std::endl; } diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h index 8c713ab06..303f1a63b 100644 --- a/src/decision/justification_heuristic.h +++ b/src/decision/justification_heuristic.h @@ -113,9 +113,7 @@ class JustificationHeuristic : public ITEDecisionStrategy { }; public: - JustificationHeuristic(DecisionEngineOld* de, - context::UserContext* uc, - context::Context* c); + JustificationHeuristic(Env& env, DecisionEngineOld* de); ~JustificationHeuristic(); diff --git a/src/decision/justification_strategy.cpp b/src/decision/justification_strategy.cpp index 56d96b32f..d9e6b43e9 100644 --- a/src/decision/justification_strategy.cpp +++ b/src/decision/justification_strategy.cpp @@ -23,20 +23,19 @@ using namespace cvc5::prop; namespace cvc5 { namespace decision { -JustificationStrategy::JustificationStrategy(context::Context* c, - context::UserContext* u, - prop::SkolemDefManager* skdm, - ResourceManager* rm) - : DecisionEngine(c, rm), +JustificationStrategy::JustificationStrategy(Env& env, + prop::SkolemDefManager* skdm) + : DecisionEngine(env), d_skdm(skdm), d_assertions( - u, - c, + userContext(), + context(), options::jhRlvOrder()), // assertions are user-context dependent - d_skolemAssertions(c, c), // skolem assertions are SAT-context dependent - d_justified(c), - d_stack(c), - d_lastDecisionLit(c), + d_skolemAssertions( + context(), context()), // skolem assertions are SAT-context dependent + d_justified(context()), + d_stack(context()), + d_lastDecisionLit(context()), d_currStatusDec(false), d_useRlvOrder(options::jhRlvOrder()), d_decisionStopOnly(options::decisionMode() diff --git a/src/decision/justification_strategy.h b/src/decision/justification_strategy.h index fc31805dd..26b456cf1 100644 --- a/src/decision/justification_strategy.h +++ b/src/decision/justification_strategy.h @@ -122,10 +122,7 @@ class JustificationStrategy : public DecisionEngine { public: /** Constructor */ - JustificationStrategy(context::Context* c, - context::UserContext* u, - prop::SkolemDefManager* skdm, - ResourceManager* rm); + JustificationStrategy(Env& env, prop::SkolemDefManager* skdm); /** Presolve, called at the beginning of each check-sat call */ void presolve() override; diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 9060c318c..34dff2ba8 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -79,7 +79,6 @@ PropEngine::PropEngine(TheoryEngine* te, Env& env) d_assumptions(d_env.getUserContext()) { Debug("prop") << "Constructing the PropEngine" << std::endl; - context::Context* satContext = d_env.getContext(); context::UserContext* userContext = d_env.getUserContext(); ProofNodeManager* pnm = d_env.getProofNodeManager(); ResourceManager* rm = d_env.getResourceManager(); @@ -88,17 +87,17 @@ PropEngine::PropEngine(TheoryEngine* te, Env& env) if (dmode == options::DecisionMode::JUSTIFICATION || dmode == options::DecisionMode::STOPONLY) { - d_decisionEngine.reset(new decision::JustificationStrategy( - satContext, userContext, d_skdm.get(), rm)); + d_decisionEngine.reset( + new decision::JustificationStrategy(env, d_skdm.get())); } else if (dmode == options::DecisionMode::JUSTIFICATION_OLD || dmode == options::DecisionMode::STOPONLY_OLD) { - d_decisionEngine.reset(new DecisionEngineOld(satContext, userContext, rm)); + d_decisionEngine.reset(new DecisionEngineOld(env)); } else { - d_decisionEngine.reset(new decision::DecisionEngineEmpty(satContext, rm)); + d_decisionEngine.reset(new decision::DecisionEngineEmpty(env)); } d_satSolver = SatSolverFactory::createCDCLTMinisat(smtStatisticsRegistry()); diff --git a/src/smt/env.cpp b/src/smt/env.cpp index 5c7836fb7..3267702fb 100644 --- a/src/smt/env.cpp +++ b/src/smt/env.cpp @@ -77,10 +77,10 @@ void Env::shutdown() d_resourceManager.reset(nullptr); } -context::UserContext* Env::getUserContext() { return d_userContext.get(); } - context::Context* Env::getContext() { return d_context.get(); } +context::UserContext* Env::getUserContext() { return d_userContext.get(); } + NodeManager* Env::getNodeManager() const { return d_nodeManager; } ProofNodeManager* Env::getProofNodeManager() { return d_proofNodeManager; } diff --git a/src/smt/env_obj.cpp b/src/smt/env_obj.cpp index b9aebbe83..926bf61ff 100644 --- a/src/smt/env_obj.cpp +++ b/src/smt/env_obj.cpp @@ -49,8 +49,6 @@ Node EnvObj::evaluate(TNode n, return d_env.evaluate(n, args, vals, visited, useRewriter); } -const LogicInfo& EnvObj::logicInfo() const { return d_env.getLogicInfo(); } - const Options& EnvObj::options() const { return d_env.getOptions(); } context::Context* EnvObj::context() const { return d_env.getContext(); } @@ -60,6 +58,13 @@ context::UserContext* EnvObj::userContext() const return d_env.getUserContext(); } +const LogicInfo& EnvObj::logicInfo() const { return d_env.getLogicInfo(); } + +ResourceManager* EnvObj::resourceManager() const +{ + return d_env.getResourceManager(); +} + StatisticsRegistry& EnvObj::statisticsRegistry() const { return d_env.getStatisticsRegistry(); diff --git a/src/smt/env_obj.h b/src/smt/env_obj.h index 75b97fda9..b240b4852 100644 --- a/src/smt/env_obj.h +++ b/src/smt/env_obj.h @@ -70,9 +70,6 @@ class EnvObj const std::unordered_map& visited, bool useRewriter = true) const; - /** Get the current logic information. */ - const LogicInfo& logicInfo() const; - /** Get the options object (const version only) via Env. */ const Options& options() const; @@ -82,6 +79,12 @@ class EnvObj /** Get a pointer to the UserContext via Env. */ context::UserContext* userContext() const; + /** Get the resource manager owned by this Env. */ + ResourceManager* resourceManager() const; + + /** Get the current logic information. */ + const LogicInfo& logicInfo() const; + /** Get the statistics registry via Env. */ StatisticsRegistry& statisticsRegistry() const; -- 2.30.2