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.

1 files changed, 9 insertions, 2 deletions

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;