From 36bfe4c1802ddeb88517a399ddab9f79976ae10d Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 6 Oct 2021 11:45:13 -0500 Subject: [PATCH] Refactor skolem definitions notifications for the decision engine (#7310) These changes are taken from the SAT relevancy branch. This does not change the behavior of the current code, it breaks the dependency of decision engine on the skolem definition manager and makes the latter solely managed by TheoryProxy. This is in preparation for virtual clause deletion. --- src/decision/decision_engine.h | 11 +++++++--- src/decision/justification_strategy.cpp | 27 ++++++++++++------------- src/decision/justification_strategy.h | 23 ++++++++++----------- src/prop/prop_engine.cpp | 9 +++------ src/prop/theory_proxy.cpp | 22 +++++++++++++++++++- src/prop/theory_proxy.h | 9 +++++++++ 6 files changed, 65 insertions(+), 36 deletions(-) diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h index 331d6eaca..d0092ab1c 100644 --- a/src/decision/decision_engine.h +++ b/src/decision/decision_engine.h @@ -61,10 +61,15 @@ class DecisionEngine : protected EnvObj */ virtual void addSkolemDefinition(TNode lem, TNode skolem) = 0; /** - * Notify this class that the literal n has been asserted, possibly - * propagated by the SAT solver. + * Notify this class that the list of lemmas defs are now active in the + * current SAT context. */ - virtual void notifyAsserted(TNode n) {} + virtual void notifyActiveSkolemDefs(std::vector& defs) {} + /** + * Track active skolem defs, whether we need to call the above method + * when appropriate. + */ + virtual bool needsActiveSkolemDefs() const { return false; } protected: /** Get next internal, the engine-specific implementation of getNext */ diff --git a/src/decision/justification_strategy.cpp b/src/decision/justification_strategy.cpp index d9e6b43e9..e577e6912 100644 --- a/src/decision/justification_strategy.cpp +++ b/src/decision/justification_strategy.cpp @@ -23,10 +23,8 @@ using namespace cvc5::prop; namespace cvc5 { namespace decision { -JustificationStrategy::JustificationStrategy(Env& env, - prop::SkolemDefManager* skdm) +JustificationStrategy::JustificationStrategy(Env& env) : DecisionEngine(env), - d_skdm(skdm), d_assertions( userContext(), context(), @@ -500,19 +498,20 @@ void JustificationStrategy::addSkolemDefinition(TNode lem, TNode skolem) insertToAssertionList(toProcess, false); } } +bool JustificationStrategy::needsActiveSkolemDefs() const +{ + return d_jhSkRlvMode == options::JutificationSkolemRlvMode::ASSERT; +} -void JustificationStrategy::notifyAsserted(TNode n) +void JustificationStrategy::notifyActiveSkolemDefs(std::vector& defs) { - if (d_jhSkRlvMode == options::JutificationSkolemRlvMode::ASSERT) - { - // assertion processed makes all skolems in assertion active, - // which triggers their definitions to becoming relevant - std::vector defs; - d_skdm->notifyAsserted(n, defs, true); - insertToAssertionList(defs, true); - } - // NOTE: can update tracking triggers, pop stack to where a child implied - // that a node on the current stack is justified. + Assert(d_jhSkRlvMode == options::JutificationSkolemRlvMode::ASSERT); + // assertion processed makes all skolems in assertion active, + // which triggers their definitions to becoming relevant + insertToAssertionList(defs, true); + // NOTE: if we had a notifyAsserted callback, we could update tracking + // triggers, pop stack to where a child implied that a node on the current + // stack is justified. } void JustificationStrategy::insertToAssertionList(std::vector& toProcess, diff --git a/src/decision/justification_strategy.h b/src/decision/justification_strategy.h index 26b456cf1..366c26c22 100644 --- a/src/decision/justification_strategy.h +++ b/src/decision/justification_strategy.h @@ -32,11 +32,6 @@ #include "prop/sat_solver_types.h" namespace cvc5 { - -namespace prop { -class SkolemDefManager; -} - namespace decision { /** @@ -122,7 +117,7 @@ class JustificationStrategy : public DecisionEngine { public: /** Constructor */ - JustificationStrategy(Env& env, prop::SkolemDefManager* skdm); + JustificationStrategy(Env& env); /** Presolve, called at the beginning of each check-sat call */ void presolve() override; @@ -157,11 +152,17 @@ class JustificationStrategy : public DecisionEngine */ void addSkolemDefinition(TNode lem, TNode skolem) override; /** - * Notify this class that literal n has been asserted. This is triggered when - * n is sent to TheoryEngine. This activates skolem definitions for skolems - * k that occur in n. + * Notify this class that the list of lemmas defs are now active in the + * current SAT context. This is triggered when a literal lit is sent to + * TheoryEngine that contains skolems we have yet to see in the current SAT + * context, where defs are the skolem definitions for each such skolem. + */ + void notifyActiveSkolemDefs(std::vector& defs) override; + /** + * We need notification of active skolem definitions when our skolem + * relevance policy is JutificationSkolemRlvMode::ASSERT. */ - void notifyAsserted(TNode n) override; + bool needsActiveSkolemDefs() const override; private: /** @@ -221,8 +222,6 @@ class JustificationStrategy : public DecisionEngine static bool isTheoryLiteral(TNode n); /** Is n a theory atom? */ static bool isTheoryAtom(TNode n); - /** Pointer to the skolem definition manager */ - prop::SkolemDefManager* d_skdm; /** The assertions, which are user-context dependent. */ AssertionList d_assertions; /** The skolem assertions */ diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 34dff2ba8..a98ab02c7 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -87,8 +87,7 @@ PropEngine::PropEngine(TheoryEngine* te, Env& env) if (dmode == options::DecisionMode::JUSTIFICATION || dmode == options::DecisionMode::STOPONLY) { - d_decisionEngine.reset( - new decision::JustificationStrategy(env, d_skdm.get())); + d_decisionEngine.reset(new decision::JustificationStrategy(env)); } else if (dmode == options::DecisionMode::JUSTIFICATION_OLD || dmode == options::DecisionMode::STOPONLY_OLD) @@ -322,7 +321,6 @@ void PropEngine::assertLemmasInternal(TrustNode trn, Assert(ppSkolems.size() == ppLemmas.size()); for (size_t i = 0, lsize = ppLemmas.size(); i < lsize; ++i) { - Node lem = ppLemmas[i].getProven(); d_theoryProxy->notifyAssertion(ppLemmas[i].getProven(), ppSkolems[i]); } } @@ -383,9 +381,8 @@ Result PropEngine::checkSat() { ScopedBool scopedBool(d_inCheckSat); d_inCheckSat = true; - // TODO This currently ignores conflicts (a dangerous practice). - d_decisionEngine->presolve(); - d_theoryEngine->presolve(); + // Note this currently ignores conflicts (a dangerous practice). + d_theoryProxy->presolve(); if(options::preprocessOnly()) { return Result(Result::SAT_UNKNOWN, Result::REQUIRES_FULL_CHECK); diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index 5b283635d..a4690ff0a 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -41,6 +41,7 @@ TheoryProxy::TheoryProxy(PropEngine* propEngine, : d_propEngine(propEngine), d_cnfStream(nullptr), d_decisionEngine(decisionEngine), + d_dmNeedsActiveDefs(d_decisionEngine->needsActiveSkolemDefs()), d_theoryEngine(theoryEngine), d_queue(env.getContext()), d_tpp(env, *theoryEngine), @@ -55,6 +56,12 @@ TheoryProxy::~TheoryProxy() { void TheoryProxy::finishInit(CnfStream* cnfStream) { d_cnfStream = cnfStream; } +void TheoryProxy::presolve() +{ + d_decisionEngine->presolve(); + d_theoryEngine->presolve(); +} + void TheoryProxy::notifyAssertion(Node a, TNode skolem) { if (skolem.isNull()) @@ -76,8 +83,21 @@ void TheoryProxy::theoryCheck(theory::Theory::Effort effort) { while (!d_queue.empty()) { TNode assertion = d_queue.front(); d_queue.pop(); + // now, assert to theory engine d_theoryEngine->assertFact(assertion); - d_decisionEngine->notifyAsserted(assertion); + if (d_dmNeedsActiveDefs) + { + Assert(d_skdm != nullptr); + Trace("sat-rlv-assert") + << "Assert to theory engine: " << assertion << std::endl; + // Assertion makes all skolems in assertion active, + // which triggers their definitions to becoming active. + std::vector activeSkolemDefs; + d_skdm->notifyAsserted(assertion, activeSkolemDefs, true); + // notify the decision engine of the skolem definitions that have become + // active due to the assertion. + d_decisionEngine->notifyActiveSkolemDefs(activeSkolemDefs); + } } d_theoryEngine->check(effort); } diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index 0e54ff8c9..a196bd4d4 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -65,6 +65,9 @@ class TheoryProxy : public Registrar /** Finish initialize */ void finishInit(CnfStream* cnfStream); + /** Presolve, which calls presolve for the modules managed by this class */ + void presolve(); + /** Notify a lemma, possibly corresponding to a skolem definition */ void notifyAssertion(Node lem, TNode skolem = TNode::null()); @@ -145,6 +148,12 @@ class TheoryProxy : public Registrar /** The decision engine we are using. */ decision::DecisionEngine* d_decisionEngine; + /** + * Whether the decision engine needs notification of active skolem + * definitions, see DecisionEngine::needsActiveSkolemDefs. + */ + bool d_dmNeedsActiveDefs; + /** The theory engine we are using. */ TheoryEngine* d_theoryEngine; -- 2.30.2