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.

6 files changed, 45 insertions, 13 deletions

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<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 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<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 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<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 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<SkolemDefManager> d_skdm;
+  SkolemDefManager* d_skdm;
 }; /* class TheoryProxy */
 
 }  // namespace prop