From 8c04f1639607b34b56e3eaa8d3188b27e1454b41 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 11 Jan 2021 11:23:15 -0600 Subject: [PATCH] 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. --- src/CMakeLists.txt | 1 - src/prop/prop_engine.cpp | 22 ++++++++------ src/prop/prop_engine.h | 3 -- src/prop/theory_proxy.cpp | 7 +++-- src/prop/theory_proxy.h | 9 ++++-- src/theory/bv/bitblast/bitblaster.h | 3 +- src/theory/theory_registrar.h | 47 ----------------------------- test/unit/prop/cnf_stream_white.h | 6 ++-- test/unit/theory/theory_bv_white.h | 1 + 9 files changed, 31 insertions(+), 68 deletions(-) delete mode 100644 src/theory/theory_registrar.h 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 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& newLemmas, std::vector& 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; -- 2.30.2