Merge theory registrar and theory proxy (#5758)

The motivation of this PR is to make TheoryProxy the single point of contact to TheoryEngine from PropEngine.

This merges the helper class TheoryRegistrar into TheoryProxy.

4 files changed, 25 insertions, 16 deletions

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 8ea3507f0..384734100 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -37,7 +37,6 @@
 #include "smt/smt_statistics_registry.h"
 #include "theory/output_channel.h"
 #include "theory/theory_engine.h"
-#include "theory/theory_registrar.h"
 #include "util/resource_manager.h"
 #include "util/result.h"
 
@@ -75,7 +74,6 @@ PropEngine::PropEngine(TheoryEngine* te,
       d_context(satContext),
       d_theoryProxy(nullptr),
       d_satSolver(nullptr),
-      d_registrar(nullptr),
       d_pnm(pnm),
       d_cnfStream(nullptr),
       d_pfCnfStream(nullptr),
@@ -91,17 +89,24 @@ PropEngine::PropEngine(TheoryEngine* te,
 
   d_satSolver = SatSolverFactory::createCDCLTMinisat(smtStatisticsRegistry());
 
-  d_registrar = new theory::TheoryRegistrar(d_theoryEngine);
-  d_cnfStream = new CVC4::prop::CnfStream(
-      d_satSolver, d_registrar, userContext, &d_outMgr, rm, FormulaLitPolicy::TRACK);
-
+  // CNF stream and theory proxy required pointers to each other, make the
+  // theory proxy first
   d_theoryProxy = new TheoryProxy(this,
                                   d_theoryEngine,
                                   d_decisionEngine.get(),
-                                  d_context,
+                                  satContext,
                                   userContext,
-                                  d_cnfStream,
                                   pnm);
+  d_cnfStream = new CnfStream(d_satSolver,
+                              d_theoryProxy,
+                              userContext,
+                              &d_outMgr,
+                              rm,
+                              FormulaLitPolicy::TRACK);
+
+  // connect theory proxy
+  d_theoryProxy->finishInit(d_cnfStream);
+  // connect SAT solver
   d_satSolver->initialize(d_context, d_theoryProxy, userContext, pnm);
 
   d_decisionEngine->setSatSolver(d_satSolver);
@@ -144,7 +149,6 @@ PropEngine::~PropEngine() {
   d_decisionEngine->shutdown();
   d_decisionEngine.reset(nullptr);
   delete d_cnfStream;
-  delete d_registrar;
   delete d_satSolver;
   delete d_theoryProxy;
 }
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index ac2b35ad6..453c1c2af 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -298,9 +298,6 @@ class PropEngine
   /** List of all of the assertions that need to be made */
   std::vector<Node> d_assertionList;
 
-  /** Theory registrar; kept around for destructor cleanup */
-  theory::TheoryRegistrar* d_registrar;
-
   /** A pointer to the proof node maneger to be used by this engine. */
   ProofNodeManager* d_pnm;
 
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 35602b8b3..8e54064e1 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -35,10 +35,9 @@ TheoryProxy::TheoryProxy(PropEngine* propEngine,
                          DecisionEngine* decisionEngine,
                          context::Context* context,
                          context::UserContext* userContext,
-                         CnfStream* cnfStream,
                          ProofNodeManager* pnm)
     : d_propEngine(propEngine),
-      d_cnfStream(cnfStream),
+      d_cnfStream(nullptr),
       d_decisionEngine(decisionEngine),
       d_theoryEngine(theoryEngine),
       d_queue(context),
@@ -50,6 +49,8 @@ TheoryProxy::~TheoryProxy() {
   /* nothing to do for now */
 }
 
+void TheoryProxy::finishInit(CnfStream* cnfStream) { d_cnfStream = cnfStream; }
+
 void TheoryProxy::variableNotify(SatVariable var) {
   d_theoryEngine->preRegister(getNode(SatLiteral(var)));
 }
@@ -189,5 +190,7 @@ theory::TrustNode TheoryProxy::preprocess(
   return pnode;
 }
 
+void TheoryProxy::preRegister(Node n) { d_theoryEngine->preRegister(n); }
+
 }/* CVC4::prop namespace */
 }/* CVC4 namespace */
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index 4d460434d..85cdff00d 100644
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -29,6 +29,7 @@
 #include "context/cdhashmap.h"
 #include "context/cdqueue.h"
 #include "expr/node.h"
+#include "prop/registrar.h"
 #include "prop/sat_solver.h"
 #include "theory/theory.h"
 #include "theory/theory_preprocessor.h"
@@ -49,7 +50,7 @@ class CnfStream;
 /**
  * The proxy class that allows the SatSolver to communicate with the theories
  */
-class TheoryProxy
+class TheoryProxy : public Registrar
 {
  public:
   TheoryProxy(PropEngine* propEngine,
@@ -57,11 +58,13 @@ class TheoryProxy
               DecisionEngine* decisionEngine,
               context::Context* context,
               context::UserContext* userContext,
-              CnfStream* cnfStream,
               ProofNodeManager* pnm);
 
   ~TheoryProxy();
 
+  /** Finish initialize */
+  void finishInit(CnfStream* cnfStream);
+
   void theoryCheck(theory::Theory::Effort effort);
 
   void explainPropagation(SatLiteral l, SatClause& explanation);
@@ -111,6 +114,8 @@ class TheoryProxy
                                std::vector<theory::TrustNode>& newLemmas,
                                std::vector<Node>& newSkolems,
                                bool doTheoryPreprocess);
+  /** Preregister term */
+  void preRegister(Node n) override;
 
  private:
   /** The prop engine we are using. */