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.

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 7e294443c2fbd7150c33c3fd3862d0cdb8e25804..15d39f06ad4eb3762f5c0c30a77715fe8c33e2da 100644 (file)
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -954,7 +954,6 @@ libcvc4_add_sources(
   theory/theory_proof_step_buffer.h
   theory/theory_rewriter.cpp
   theory/theory_rewriter.h
-  theory/theory_registrar.h
   theory/theory_state.cpp
   theory/theory_state.h
   theory/theory_test_utils.h

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 8ea3507f093a04fe0fa3b4eaaa59934e5ede96ea..384734100a7b1bfd744228e42284ac6fb48f6d19 100644 (file)
--- 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 ac2b35ad67a6da6f81ef8b763c7db6f7aef070e8..453c1c2af83febdd1183374d8963215176693927 100644 (file)
--- 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 35602b8b3ab721fc7bb14d7066af7e7ba292f9aa..8e54064e1a57bfc273553bb18ee601db805d269a 100644 (file)
--- 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 4d460434dfe4f7cb2ef97d921fa40bb08876ec1f..85cdff00d11f34cd1e83dcb22f374b461794d1c8 100644 (file)
--- 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. */

diff --git a/src/theory/bv/bitblast/bitblaster.h b/src/theory/bv/bitblast/bitblaster.h
index fd99621d44c7c3c76c65a98e2dea0433d806f83a..d71fae8d00a2e3f4a16898dc116a0f9c59d5efed 100644 (file)
--- a/src/theory/bv/bitblast/bitblaster.h
+++ b/src/theory/bv/bitblast/bitblaster.h
@@ -25,11 +25,12 @@
 
 #include "expr/node.h"
 #include "prop/bv_sat_solver_notify.h"
+#include "prop/cnf_stream.h"
+#include "prop/registrar.h"
 #include "prop/sat_solver.h"
 #include "prop/sat_solver_types.h"
 #include "smt/smt_engine_scope.h"
 #include "theory/bv/bitblast/bitblast_strategies_template.h"
-#include "theory/theory_registrar.h"
 #include "theory/valuation.h"
 #include "util/resource_manager.h"
 

diff --git a/src/theory/theory_registrar.h b/src/theory/theory_registrar.h
deleted file mode 100644 (file)
index bc88b93..0000000
--- a/src/theory/theory_registrar.h
+++ /dev/null
@@ -1,47 +0,0 @@
-/*********************                                                        */
-/*! \file theory_registrar.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Mathias Preiner, Tim King, Liana Hadarean
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Class to encapsulate preregistration duties
- **
- ** Class to encapsulate preregistration duties.  This class permits the
- ** CNF stream implementation to reach into the theory engine to
- ** preregister only those terms with an associated SAT literal (at the
- ** point when they get the SAT literal), without having to refer to the
- ** TheoryEngine class directly.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef CVC4__THEORY__THEORY_REGISTRAR_H
-#define CVC4__THEORY__THEORY_REGISTRAR_H
-
-#include "prop/registrar.h"
-#include "theory/theory_engine.h"
-
-namespace CVC4 {
-namespace theory {
-
-class TheoryRegistrar : public prop::Registrar {
-private:
-  TheoryEngine* d_theoryEngine;
-
-public:
-
-  TheoryRegistrar(TheoryEngine* te) : d_theoryEngine(te) { }
-
-  void preRegister(Node n) override { d_theoryEngine->preRegister(n); }
-
-};/* class TheoryRegistrar */
-
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* CVC4__THEORY__THEORY_REGISTRAR_H */

diff --git a/test/unit/prop/cnf_stream_white.h b/test/unit/prop/cnf_stream_white.h
index 495097a790a76a914316d0f2aa5bf34038400a3f..5200d81d816ba5c1123688a6512da65d97b74ddf 100644 (file)
--- a/test/unit/prop/cnf_stream_white.h
+++ b/test/unit/prop/cnf_stream_white.h
@@ -24,6 +24,7 @@
 #include "expr/node_manager.h"
 #include "prop/cnf_stream.h"
 #include "prop/prop_engine.h"
+#include "prop/registrar.h"
 #include "prop/theory_proxy.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
@@ -32,7 +33,6 @@
 #include "theory/builtin/theory_builtin.h"
 #include "theory/theory.h"
 #include "theory/theory_engine.h"
-#include "theory/theory_registrar.h"
 
 using namespace CVC4;
 using namespace CVC4::context;
@@ -119,7 +119,7 @@ class CnfStreamWhite : public CxxTest::TestSuite {
   Context* d_cnfContext;
 
   /** The registrar used by the CnfStream. */
-  theory::TheoryRegistrar* d_cnfRegistrar;
+  prop::NullRegistrar* d_cnfRegistrar;
 
   /** The node manager */
   NodeManager* d_nodeManager;
@@ -144,7 +144,7 @@ class CnfStreamWhite : public CxxTest::TestSuite {
 
     d_satSolver = new FakeSatSolver();
     d_cnfContext = new context::Context();
-    d_cnfRegistrar = new theory::TheoryRegistrar(d_theoryEngine);
+    d_cnfRegistrar = new prop::NullRegistrar;
     ResourceManager* rm = d_smt->getResourceManager();
     d_cnfStream = new CVC4::prop::CnfStream(d_satSolver,
                                             d_cnfRegistrar,

diff --git a/test/unit/theory/theory_bv_white.h b/test/unit/theory/theory_bv_white.h
index f568dc779eb86f5f92050f0b09f1d8f1443e89e5..0cfe722a61dc355c7cad93653e94cd04c22c6f7d 100644 (file)
--- a/test/unit/theory/theory_bv_white.h
+++ b/test/unit/theory/theory_bv_white.h
@@ -27,6 +27,7 @@
 #include "theory/bv/bitblast/eager_bitblaster.h"
 #include "theory/bv/bv_solver_lazy.h"
 #include "theory/theory.h"
+#include "theory/theory_engine.h"
 #include "theory/theory_test_utils.h"
 
 using namespace CVC4;