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.

diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp
index 12e14850064af3aa0c12990800815415bfc10699..d55d2077f8de05681da0ffd4a09a20121aef9247 100644 (file)
--- 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 0a1d63d99dd4c09bf086640609a9b137c986ab68..c10fe2bb90a429f321a62cae994bdf31a58d2011 100644 (file)
--- 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<ITEDecisionStrategy> 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 9f3b4be914d1c7b0fa4b8f722d4541369baaf054..0376b00cc0260d41441bd3bcc58e72071a6a4f01 100644 (file)
--- 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 42e4cb7b00240bec77f3f123e1ea9cd297daef47..ecc0ae68c0732ff9e7476f4fdc9ac6f9005f427f 100644 (file)
--- 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 a7c82646dfbedfc7d238ac17d62052957f4b5b7b..45f297bb94ca32eb79a89bc1f6746d5f8c9a4c9c 100644 (file)
--- 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 646da84b2e7fd1e59022146fa65d88771dd22a34..c4d929d357829b67c5839d2b0fcf5f4c1b95dff0 100644 (file)
--- 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 cae02eba245fb09d4b83057f2e4b95a96b2a1be2..a0496a525be622f38b3eb38e76e8e06e194bb52a 100644 (file)
--- 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<DecisionEngine> d_decisionEngine;
+  std::unique_ptr<decision::DecisionEngine> d_decisionEngine;
 
   /** The context */
   context::Context* d_context;
 
+  /** The skolem definition manager */
+  std::unique_ptr<SkolemDefManager> 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 9b401155778a7bd4c4b3ae4f101d0d1ffe7c7d23..873a748aeec8be0e029844eb7a60b65b344af445 100644 (file)
--- 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<TNode>& activatedSkolems)
+                                      std::vector<TNode>& activatedSkolems,
+                                      bool useDefs)
 {
   std::unordered_set<Node, NodeHashFunction> 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 9ddde3fb2d8c3c38bca960566e1ed1e2b4161c47..475f40c8591fc0530af94e9a29322c3317104705 100644 (file)
--- 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<TNode>& activatedSkolems);
+  void notifyAsserted(TNode literal,
+                      std::vector<TNode>& 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 98a76ae1a438034330b6d24431eabff7bd5569cb..43f91f73289adfe57bef2879cb6e1e018922ff1f 100644 (file)
--- 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 5ba9ea50fdc02973f9d01a485c88aed837225906..bc834d20521f03fff9b979ec546b2c676fee9fd9 100644 (file)
--- 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<SkolemDefManager> d_skdm;
+  SkolemDefManager* d_skdm;
 }; /* class TheoryProxy */
 
 }  // namespace prop