From 7295b8da3f77d0121ab0215a7f309dab90b02854 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 22 Apr 2021 14:12:23 -0500 Subject: [PATCH] Reorganizing use of skolem definition manager in prop engine (#6415) Towards setting up the proper callbacks into the new justification heuristic. Moves ownership of skolem definition manager from TheoryProxy to PropEngine. --- src/decision/decision_engine.cpp | 2 ++ src/decision/decision_engine.h | 2 ++ src/decision/decision_strategy.h | 4 ++-- src/decision/justification_heuristic.cpp | 2 +- src/decision/justification_heuristic.h | 2 +- src/prop/prop_engine.cpp | 2 ++ src/prop/prop_engine.h | 11 +++++++++-- src/prop/skolem_def_manager.cpp | 19 +++++++++++++++---- src/prop/skolem_def_manager.h | 9 ++++++++- src/prop/theory_proxy.cpp | 6 ++++-- src/prop/theory_proxy.h | 11 +++++++---- 11 files changed, 53 insertions(+), 17 deletions(-) diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp index 12e148500..d55d2077f 100644 --- a/src/decision/decision_engine.cpp +++ b/src/decision/decision_engine.cpp @@ -24,6 +24,7 @@ using namespace std; namespace cvc5 { +namespace decision { DecisionEngine::DecisionEngine(context::Context* sc, context::UserContext* uc, @@ -100,4 +101,5 @@ void DecisionEngine::addSkolemDefinition(TNode lem, TNode skolem) } } +} } // namespace cvc5 diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h index 0a1d63d99..c10fe2bb9 100644 --- a/src/decision/decision_engine.h +++ b/src/decision/decision_engine.h @@ -31,6 +31,7 @@ using namespace cvc5::prop; using namespace cvc5::decision; namespace cvc5 { +namespace decision { class DecisionEngine { @@ -159,6 +160,7 @@ class DecisionEngine { std::unique_ptr d_enabledITEStrategy; };/* DecisionEngine class */ +} } // namespace cvc5 #endif /* CVC5__DECISION__DECISION_ENGINE_H */ diff --git a/src/decision/decision_strategy.h b/src/decision/decision_strategy.h index 9f3b4be91..0376b00cc 100644 --- a/src/decision/decision_strategy.h +++ b/src/decision/decision_strategy.h @@ -26,13 +26,13 @@ namespace cvc5 { -class DecisionEngine; - namespace context { class Context; } // namespace context namespace decision { + +class DecisionEngine; class DecisionStrategy { protected: diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp index 42e4cb7b0..ecc0ae68c 100644 --- a/src/decision/justification_heuristic.cpp +++ b/src/decision/justification_heuristic.cpp @@ -32,7 +32,7 @@ namespace cvc5 { namespace decision { -JustificationHeuristic::JustificationHeuristic(cvc5::DecisionEngine* de, +JustificationHeuristic::JustificationHeuristic(DecisionEngine* de, context::UserContext* uc, context::Context* c) : ITEDecisionStrategy(de, c), diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h index a7c82646d..45f297bb9 100644 --- a/src/decision/justification_heuristic.h +++ b/src/decision/justification_heuristic.h @@ -117,7 +117,7 @@ class JustificationHeuristic : public ITEDecisionStrategy { }; public: - JustificationHeuristic(cvc5::DecisionEngine* de, + JustificationHeuristic(DecisionEngine* de, context::UserContext* uc, context::Context* c); diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 646da84b2..c4d929d35 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -73,6 +73,7 @@ PropEngine::PropEngine(TheoryEngine* te, : d_inCheckSat(false), d_theoryEngine(te), d_context(satContext), + d_skdm(new SkolemDefManager(satContext, userContext)), d_theoryProxy(nullptr), d_satSolver(nullptr), d_pnm(pnm), @@ -95,6 +96,7 @@ PropEngine::PropEngine(TheoryEngine* te, d_theoryProxy = new TheoryProxy(this, d_theoryEngine, d_decisionEngine.get(), + d_skdm.get(), satContext, userContext, pnm); diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index cae02eba2..a0496a525 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -22,6 +22,7 @@ #include "context/cdlist.h" #include "expr/node.h" +#include "prop/skolem_def_manager.h" #include "theory/output_channel.h" #include "theory/trust_node.h" #include "util/result.h" @@ -29,11 +30,14 @@ namespace cvc5 { class ResourceManager; -class DecisionEngine; class OutputManager; class ProofNodeManager; class TheoryEngine; +namespace decision { +class DecisionEngine; +} + namespace prop { class CnfStream; @@ -331,11 +335,14 @@ class PropEngine TheoryEngine* d_theoryEngine; /** The decision engine we will be using */ - std::unique_ptr d_decisionEngine; + std::unique_ptr d_decisionEngine; /** The context */ context::Context* d_context; + /** The skolem definition manager */ + std::unique_ptr d_skdm; + /** SAT solver's proxy back to theories; kept around for dtor cleanup */ TheoryProxy* d_theoryProxy; diff --git a/src/prop/skolem_def_manager.cpp b/src/prop/skolem_def_manager.cpp index 9b4011557..873a748ae 100644 --- a/src/prop/skolem_def_manager.cpp +++ b/src/prop/skolem_def_manager.cpp @@ -44,12 +44,13 @@ void SkolemDefManager::notifySkolemDefinition(TNode skolem, Node def) TNode SkolemDefManager::getDefinitionForSkolem(TNode skolem) const { NodeNodeMap::const_iterator it = d_skDefs.find(skolem); - AlwaysAssert(it != d_skDefs.end()) << "No skolem def for " << skolem; + Assert(it != d_skDefs.end()) << "No skolem def for " << skolem; return it->second; } void SkolemDefManager::notifyAsserted(TNode literal, - std::vector& activatedSkolems) + std::vector& activatedSkolems, + bool useDefs) { std::unordered_set skolems; getSkolems(literal, skolems); @@ -61,8 +62,18 @@ void SkolemDefManager::notifyAsserted(TNode literal, continue; } d_skActive.insert(k); - // add to the activated list - activatedSkolems.push_back(k); + if (useDefs) + { + // add its definition to the activated list + NodeNodeMap::const_iterator it = d_skDefs.find(k); + Assert(it != d_skDefs.end()); + activatedSkolems.push_back(it->second); + } + else + { + // add to the activated list + activatedSkolems.push_back(k); + } } } diff --git a/src/prop/skolem_def_manager.h b/src/prop/skolem_def_manager.h index 9ddde3fb2..475f40c85 100644 --- a/src/prop/skolem_def_manager.h +++ b/src/prop/skolem_def_manager.h @@ -64,8 +64,15 @@ class SkolemDefManager * Notify that the given literal has been asserted. This method adds skolems * that become "active" as a result of asserting this literal. A skolem * is active in the SAT context if it appears in an asserted literal. + * + * @param literal The literal that became asserted + * @param activatedSkolems The list to add skolems to + * @param useDefs If this flag is true, we add the skolem definition for + * skolems to activatedSkolems instead of the skolem itself. */ - void notifyAsserted(TNode literal, std::vector& activatedSkolems); + void notifyAsserted(TNode literal, + std::vector& activatedSkolems, + bool useDefs = false); /** * Get the set of skolems maintained by this class that occur in node n, diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index 98a76ae1a..43f91f732 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -24,6 +24,7 @@ #include "proof/cnf_proof.h" #include "prop/cnf_stream.h" #include "prop/prop_engine.h" +#include "prop/skolem_def_manager.h" #include "smt/smt_statistics_registry.h" #include "theory/rewriter.h" #include "theory/theory_engine.h" @@ -34,7 +35,8 @@ namespace prop { TheoryProxy::TheoryProxy(PropEngine* propEngine, TheoryEngine* theoryEngine, - DecisionEngine* decisionEngine, + decision::DecisionEngine* decisionEngine, + SkolemDefManager* skdm, context::Context* context, context::UserContext* userContext, ProofNodeManager* pnm) @@ -44,7 +46,7 @@ TheoryProxy::TheoryProxy(PropEngine* propEngine, d_theoryEngine(theoryEngine), d_queue(context), d_tpp(*theoryEngine, userContext, pnm), - d_skdm(new SkolemDefManager(context, userContext)) + d_skdm(skdm) { } diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index 5ba9ea50f..bc834d205 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -28,7 +28,6 @@ #include "expr/node.h" #include "prop/registrar.h" #include "prop/sat_solver_types.h" -#include "prop/skolem_def_manager.h" #include "theory/theory.h" #include "theory/theory_preprocessor.h" #include "theory/trust_node.h" @@ -36,13 +35,16 @@ namespace cvc5 { +namespace decision { class DecisionEngine; +} class TheoryEngine; namespace prop { class PropEngine; class CnfStream; +class SkolemDefManager; /** * The proxy class that allows the SatSolver to communicate with the theories @@ -52,7 +54,8 @@ class TheoryProxy : public Registrar public: TheoryProxy(PropEngine* propEngine, TheoryEngine* theoryEngine, - DecisionEngine* decisionEngine, + decision::DecisionEngine* decisionEngine, + SkolemDefManager* skdm, context::Context* context, context::UserContext* userContext, ProofNodeManager* pnm); @@ -140,7 +143,7 @@ class TheoryProxy : public Registrar CnfStream* d_cnfStream; /** The decision engine we are using. */ - DecisionEngine* d_decisionEngine; + decision::DecisionEngine* d_decisionEngine; /** The theory engine we are using. */ TheoryEngine* d_theoryEngine; @@ -158,7 +161,7 @@ class TheoryProxy : public Registrar theory::TheoryPreprocessor d_tpp; /** The skolem definition manager */ - std::unique_ptr d_skdm; + SkolemDefManager* d_skdm; }; /* class TheoryProxy */ } // namespace prop -- 2.30.2