summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/CMakeLists.txt1
-rw-r--r--src/prop/prop_engine.cpp22
-rw-r--r--src/prop/prop_engine.h3
-rw-r--r--src/prop/theory_proxy.cpp7
-rw-r--r--src/prop/theory_proxy.h9
-rw-r--r--src/theory/bv/bitblast/bitblaster.h3
-rw-r--r--src/theory/theory_registrar.h47
-rw-r--r--test/unit/prop/cnf_stream_white.h6
-rw-r--r--test/unit/theory/theory_bv_white.h1
9 files changed, 31 insertions, 68 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 7e294443c..15d39f06a 100644
--- 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 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. */
diff --git a/src/theory/bv/bitblast/bitblaster.h b/src/theory/bv/bitblast/bitblaster.h
index fd99621d4..d71fae8d0 100644
--- 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
index bc88b93f4..000000000
--- 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 495097a79..5200d81d8 100644
--- 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 f568dc779..0cfe722a6 100644
--- 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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback