From 19c382b8666492fa8818444c7f2ee907da3d9479 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 3 Aug 2021 20:15:43 -0500 Subject: [PATCH] Remove dependencies on smt engine in smt solver (#6965) This is work towards eliminating circular dependencies on SmtEngine. This simplifies several interfaces and makes it so that SmtSolver does not take a pointer to its parent SmtEngine. It is also work towards eliminating the output manager, which is now subsumed by Env. --- src/prop/cnf_stream.cpp | 12 +++--- src/prop/cnf_stream.h | 12 +++--- src/prop/prop_engine.cpp | 4 +- src/prop/prop_engine.h | 5 --- src/smt/smt_engine.cpp | 63 +++++++++++++---------------- src/smt/smt_solver.cpp | 16 +++----- src/smt/smt_solver.h | 5 +-- src/theory/theory_engine.cpp | 14 +++---- src/theory/theory_engine.h | 6 +-- test/unit/prop/cnf_stream_white.cpp | 2 +- 10 files changed, 54 insertions(+), 85 deletions(-) diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 4897f8e6a..e04651fc3 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -27,7 +27,7 @@ #include "prop/prop_engine.h" #include "prop/theory_proxy.h" #include "smt/dump.h" -#include "smt/smt_engine.h" +#include "smt/env.h" #include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" #include "theory/theory.h" @@ -39,12 +39,12 @@ namespace prop { CnfStream::CnfStream(SatSolver* satSolver, Registrar* registrar, context::Context* context, - OutputManager* outMgr, + Env* env, ResourceManager* rm, FormulaLitPolicy flpol, std::string name) : d_satSolver(satSolver), - d_outMgr(outMgr), + d_env(env), d_booleanVariables(context), d_notifyFormulas(context), d_nodeToLiteralMap(context), @@ -61,10 +61,10 @@ CnfStream::CnfStream(SatSolver* satSolver, bool CnfStream::assertClause(TNode node, SatClause& c) { Trace("cnf") << "Inserting into stream " << c << " node = " << node << "\n"; - if (Dump.isOn("clauses") && d_outMgr != nullptr) + if (Dump.isOn("clauses") && d_env != nullptr) { - const Printer& printer = d_outMgr->getPrinter(); - std::ostream& out = d_outMgr->getDumpOut(); + const Printer& printer = d_env->getPrinter(); + std::ostream& out = d_env->getDumpOut(); if (c.size() == 1) { printer.toStreamCmdAssert(out, getNode(c[0])); diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index aeed97380..664a2bf61 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -36,7 +36,7 @@ namespace cvc5 { -class OutputManager; +class Env; namespace prop { @@ -84,8 +84,8 @@ class CnfStream { * @param satSolver the sat solver to use. * @param registrar the entity that takes care of preregistration of Nodes. * @param context the context that the CNF should respect. - * @param outMgr Reference to the output manager of the smt engine. Assertions - * will not be dumped if outMgr == nullptr. + * @param env Reference to the environment of the smt engine. Assertions + * will not be dumped if env == nullptr. * @param rm the resource manager of the CNF stream * @param flpol policy for literals corresponding to formulas (those that are * not-theory literals). @@ -95,7 +95,7 @@ class CnfStream { CnfStream(SatSolver* satSolver, Registrar* registrar, context::Context* context, - OutputManager* outMgr, + Env* env, ResourceManager* rm, FormulaLitPolicy flpol = FormulaLitPolicy::INTERNAL, std::string name = ""); @@ -212,8 +212,8 @@ class CnfStream { /** The SAT solver we will be using */ SatSolver* d_satSolver; - /** Reference to the output manager of the smt engine */ - OutputManager* d_outMgr; + /** Pointer to the env of the smt engine */ + Env* d_env; /** Boolean variables that we translated */ context::CDList d_booleanVariables; diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 24b98577f..0308715e6 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -67,7 +67,6 @@ public: PropEngine::PropEngine(TheoryEngine* te, Env& env, - OutputManager& outMgr, ProofNodeManager* pnm) : d_inCheckSat(false), d_theoryEngine(te), @@ -80,7 +79,6 @@ PropEngine::PropEngine(TheoryEngine* te, d_pfCnfStream(nullptr), d_ppm(nullptr), d_interrupted(false), - d_outMgr(outMgr), d_assumptions(d_env.getUserContext()) { Debug("prop") << "Constructing the PropEngine" << std::endl; @@ -119,7 +117,7 @@ PropEngine::PropEngine(TheoryEngine* te, d_cnfStream = new CnfStream(d_satSolver, d_theoryProxy, userContext, - &d_outMgr, + &d_env, rm, FormulaLitPolicy::TRACK, "prop"); diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index e458ca5e5..4d06adfba 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -31,7 +31,6 @@ namespace cvc5 { class Env; class ResourceManager; -class OutputManager; class ProofNodeManager; class TheoryEngine; @@ -59,7 +58,6 @@ class PropEngine */ PropEngine(TheoryEngine* te, Env& env, - OutputManager& outMgr, ProofNodeManager* pnm); /** @@ -388,9 +386,6 @@ class PropEngine /** Whether we were just interrupted (or not) */ bool d_interrupted; - /** Reference to the output manager of the smt engine */ - OutputManager& d_outMgr; - /** * Stores assumptions added via assertInternal() if assumption-based unsat * cores are enabled. diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 774d8b192..55f3d1c5f 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -132,8 +132,7 @@ SmtEngine::SmtEngine(NodeManager* nm, Options* optr) d_pp.reset( new smt::Preprocessor(*this, *d_env.get(), *d_absValues.get(), *d_stats)); // make the SMT solver - d_smtSolver.reset( - new SmtSolver(*this, *d_env.get(), *d_state, *d_pp, *d_stats)); + d_smtSolver.reset(new SmtSolver(*d_env.get(), *d_state, *d_pp, *d_stats)); // make the SyGuS solver d_sygusSolver.reset( new SygusSolver(*d_smtSolver, *d_pp, getUserContext(), d_outMgr)); @@ -251,11 +250,11 @@ void SmtEngine::finishInit() LogicInfo everything; everything.lock(); getPrinter().toStreamCmdComment( - getOutputManager().getDumpOut(), + d_env->getDumpOut(), "cvc5 always dumps the most general, all-supported logic (below), as " "some internals might require the use of a logic more general than " "the input."); - getPrinter().toStreamCmdSetBenchmarkLogic(getOutputManager().getDumpOut(), + getPrinter().toStreamCmdSetBenchmarkLogic(d_env->getDumpOut(), everything.getLogicString()); } @@ -359,7 +358,7 @@ void SmtEngine::setLogic(const std::string& s) if (Dump.isOn("raw-benchmark")) { getPrinter().toStreamCmdSetBenchmarkLogic( - getOutputManager().getDumpOut(), getLogicInfo().getLogicString()); + d_env->getDumpOut(), getLogicInfo().getLogicString()); } } catch (IllegalArgumentException& e) @@ -431,13 +430,11 @@ void SmtEngine::setInfo(const std::string& key, const std::string& value) (value == "sat") ? Result::SAT : ((value == "unsat") ? Result::UNSAT : Result::SAT_UNKNOWN); - getPrinter().toStreamCmdSetBenchmarkStatus( - getOutputManager().getDumpOut(), status); + getPrinter().toStreamCmdSetBenchmarkStatus(d_env->getDumpOut(), status); } else { - getPrinter().toStreamCmdSetInfo( - getOutputManager().getDumpOut(), key, value); + getPrinter().toStreamCmdSetInfo(d_env->getDumpOut(), key, value); } } @@ -677,7 +674,7 @@ void SmtEngine::defineFunctionsRec( if (Dump.isOn("raw-benchmark")) { getPrinter().toStreamCmdDefineFunctionRec( - getOutputManager().getDumpOut(), funcs, formals, formulas); + d_env->getDumpOut(), funcs, formals, formulas); } NodeManager* nm = getNodeManager(); @@ -835,8 +832,7 @@ Result SmtEngine::checkSat(const Node& assumption) { if (Dump.isOn("benchmark")) { - getPrinter().toStreamCmdCheckSat(getOutputManager().getDumpOut(), - assumption); + getPrinter().toStreamCmdCheckSat(d_env->getDumpOut(), assumption); } std::vector assump; if (!assumption.isNull()) @@ -852,11 +848,11 @@ Result SmtEngine::checkSat(const std::vector& assumptions) { if (assumptions.empty()) { - getPrinter().toStreamCmdCheckSat(getOutputManager().getDumpOut()); + getPrinter().toStreamCmdCheckSat(d_env->getDumpOut()); } else { - getPrinter().toStreamCmdCheckSatAssuming(getOutputManager().getDumpOut(), + getPrinter().toStreamCmdCheckSatAssuming(d_env->getDumpOut(), assumptions); } } @@ -867,7 +863,7 @@ Result SmtEngine::checkEntailed(const Node& node) { if (Dump.isOn("benchmark")) { - getPrinter().toStreamCmdQuery(getOutputManager().getDumpOut(), node); + getPrinter().toStreamCmdQuery(d_env->getDumpOut(), node); } return checkSatInternal( node.isNull() ? std::vector() : std::vector{node}, @@ -975,8 +971,7 @@ std::vector SmtEngine::getUnsatAssumptions(void) finishInit(); if (Dump.isOn("benchmark")) { - getPrinter().toStreamCmdGetUnsatAssumptions( - getOutputManager().getDumpOut()); + getPrinter().toStreamCmdGetUnsatAssumptions(d_env->getDumpOut()); } UnsatCore core = getUnsatCoreInternal(); std::vector res; @@ -1001,7 +996,7 @@ Result SmtEngine::assertFormula(const Node& formula) if (Dump.isOn("raw-benchmark")) { - getPrinter().toStreamCmdAssert(getOutputManager().getDumpOut(), formula); + getPrinter().toStreamCmdAssert(d_env->getDumpOut(), formula); } // Substitute out any abstract values in ex @@ -1023,8 +1018,7 @@ void SmtEngine::declareSygusVar(Node var) d_sygusSolver->declareSygusVar(var); if (Dump.isOn("raw-benchmark")) { - getPrinter().toStreamCmdDeclareVar( - getOutputManager().getDumpOut(), var, var.getType()); + getPrinter().toStreamCmdDeclareVar(d_env->getDumpOut(), var, var.getType()); } // don't need to set that the conjecture is stale } @@ -1045,7 +1039,7 @@ void SmtEngine::declareSynthFun(Node func, if (Dump.isOn("raw-benchmark")) { getPrinter().toStreamCmdSynthFun( - getOutputManager().getDumpOut(), func, vars, isInv, sygusType); + d_env->getDumpOut(), func, vars, isInv, sygusType); } } void SmtEngine::declareSynthFun(Node func, @@ -1064,8 +1058,7 @@ void SmtEngine::assertSygusConstraint(Node constraint) d_sygusSolver->assertSygusConstraint(constraint); if (Dump.isOn("raw-benchmark")) { - getPrinter().toStreamCmdConstraint(getOutputManager().getDumpOut(), - constraint); + getPrinter().toStreamCmdConstraint(d_env->getDumpOut(), constraint); } } @@ -1080,7 +1073,7 @@ void SmtEngine::assertSygusInvConstraint(Node inv, if (Dump.isOn("raw-benchmark")) { getPrinter().toStreamCmdInvConstraint( - getOutputManager().getDumpOut(), inv, pre, trans, post); + d_env->getDumpOut(), inv, pre, trans, post); } } @@ -1200,7 +1193,7 @@ Model* SmtEngine::getModel() { if (Dump.isOn("benchmark")) { - getPrinter().toStreamCmdGetModel(getOutputManager().getDumpOut()); + getPrinter().toStreamCmdGetModel(d_env->getDumpOut()); } Model* m = getAvailableModel("get model"); @@ -1238,7 +1231,7 @@ Result SmtEngine::blockModel() if (Dump.isOn("benchmark")) { - getPrinter().toStreamCmdBlockModel(getOutputManager().getDumpOut()); + getPrinter().toStreamCmdBlockModel(d_env->getDumpOut()); } Model* m = getAvailableModel("block model"); @@ -1270,8 +1263,7 @@ Result SmtEngine::blockModelValues(const std::vector& exprs) if (Dump.isOn("benchmark")) { - getPrinter().toStreamCmdBlockModelValues(getOutputManager().getDumpOut(), - exprs); + getPrinter().toStreamCmdBlockModelValues(d_env->getDumpOut(), exprs); } Model* m = getAvailableModel("block model values"); @@ -1563,7 +1555,7 @@ UnsatCore SmtEngine::getUnsatCore() { finishInit(); if (Dump.isOn("benchmark")) { - getPrinter().toStreamCmdGetUnsatCore(getOutputManager().getDumpOut()); + getPrinter().toStreamCmdGetUnsatCore(d_env->getDumpOut()); } return getUnsatCoreInternal(); } @@ -1588,7 +1580,7 @@ std::string SmtEngine::getProof() finishInit(); if (Dump.isOn("benchmark")) { - getPrinter().toStreamCmdGetProof(getOutputManager().getDumpOut()); + getPrinter().toStreamCmdGetProof(d_env->getDumpOut()); } if (!d_env->getOptions().smt.produceProofs) { @@ -1789,7 +1781,7 @@ std::vector SmtEngine::getAssertions() d_state->doPendingPops(); if (Dump.isOn("benchmark")) { - getPrinter().toStreamCmdGetAssertions(getOutputManager().getDumpOut()); + getPrinter().toStreamCmdGetAssertions(d_env->getDumpOut()); } Trace("smt") << "SMT getAssertions()" << endl; if (!d_env->getOptions().smt.produceAssertions) @@ -1817,7 +1809,7 @@ void SmtEngine::push() Trace("smt") << "SMT push()" << endl; d_smtSolver->processAssertions(*d_asserts); if(Dump.isOn("benchmark")) { - getPrinter().toStreamCmdPush(getOutputManager().getDumpOut()); + getPrinter().toStreamCmdPush(d_env->getDumpOut()); } d_state->userPush(); } @@ -1828,7 +1820,7 @@ void SmtEngine::pop() { Trace("smt") << "SMT pop()" << endl; if (Dump.isOn("benchmark")) { - getPrinter().toStreamCmdPop(getOutputManager().getDumpOut()); + getPrinter().toStreamCmdPop(d_env->getDumpOut()); } d_state->userPop(); @@ -1861,7 +1853,7 @@ void SmtEngine::resetAssertions() Trace("smt") << "SMT resetAssertions()" << endl; if (Dump.isOn("benchmark")) { - getPrinter().toStreamCmdResetAssertions(getOutputManager().getDumpOut()); + getPrinter().toStreamCmdResetAssertions(d_env->getDumpOut()); } d_asserts->clearCurrent(); @@ -1949,8 +1941,7 @@ void SmtEngine::setOption(const std::string& key, const std::string& value) if (Dump.isOn("benchmark")) { - getPrinter().toStreamCmdSetOption( - getOutputManager().getDumpOut(), key, value); + getPrinter().toStreamCmdSetOption(d_env->getDumpOut(), key, value); } if (key == "command-verbosity") diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 6d3326603..503d9d1db 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -32,13 +32,11 @@ using namespace std; namespace cvc5 { namespace smt { -SmtSolver::SmtSolver(SmtEngine& smt, - Env& env, +SmtSolver::SmtSolver(Env& env, SmtEngineState& state, Preprocessor& pp, SmtEngineStatistics& stats) - : d_smt(smt), - d_env(env), + : d_env(env), d_state(state), d_pp(pp), d_stats(stats), @@ -56,7 +54,6 @@ void SmtSolver::finishInit(const LogicInfo& logicInfo) // engine later (it is non-essential there) d_theoryEngine.reset(new TheoryEngine( d_env, - d_smt.getOutputManager(), // Other than whether d_pm is set, theory engine proofs are conditioned on // the relationshup between proofs and unsat cores: the unsat cores are in // FULL_PROOF mode, no proofs are generated on theory engine. @@ -81,8 +78,7 @@ void SmtSolver::finishInit(const LogicInfo& logicInfo) * are unregistered by the obsolete PropEngine object before registered * again by the new PropEngine object */ d_propEngine.reset(nullptr); - d_propEngine.reset(new prop::PropEngine( - d_theoryEngine.get(), d_env, d_smt.getOutputManager(), d_pnm)); + d_propEngine.reset(new prop::PropEngine(d_theoryEngine.get(), d_env, d_pnm)); Trace("smt-debug") << "Setting up theory engine..." << std::endl; d_theoryEngine->setPropEngine(getPropEngine()); @@ -98,8 +94,7 @@ void SmtSolver::resetAssertions() * statistics are unregistered by the obsolete PropEngine object before * registered again by the new PropEngine object */ d_propEngine.reset(nullptr); - d_propEngine.reset(new prop::PropEngine( - d_theoryEngine.get(), d_env, d_smt.getOutputManager(), d_pnm)); + d_propEngine.reset(new prop::PropEngine(d_theoryEngine.get(), d_env, d_pnm)); d_theoryEngine->setPropEngine(getPropEngine()); // Notice that we do not reset TheoryEngine, nor does it require calling // finishInit again. In particular, TheoryEngine::finishInit does not @@ -142,8 +137,7 @@ Result SmtSolver::checkSatisfiability(Assertions& as, // then, initialize the assertions as.initializeCheckSat(assumptions, isEntailmentCheck); - // make the check - Assert(d_smt.isFullyInited()); + // make the check, where notice smt engine should be fully inited by now Trace("smt") << "SmtSolver::check()" << endl; diff --git a/src/smt/smt_solver.h b/src/smt/smt_solver.h index ea89f6d57..cf82d9309 100644 --- a/src/smt/smt_solver.h +++ b/src/smt/smt_solver.h @@ -64,8 +64,7 @@ struct SmtEngineStatistics; class SmtSolver { public: - SmtSolver(SmtEngine& smt, - Env& env, + SmtSolver(Env& env, SmtEngineState& state, Preprocessor& pp, SmtEngineStatistics& stats); @@ -132,8 +131,6 @@ class SmtSolver //------------------------------------------ end access methods private: - /** Reference to the parent SMT engine */ - SmtEngine& d_smt; /** Reference to the environment */ Env& d_env; /** Reference to the state of the SmtEngine */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index fb93403b9..233ea64ed 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -219,12 +219,10 @@ context::UserContext* TheoryEngine::getUserContext() const } TheoryEngine::TheoryEngine(Env& env, - OutputManager& outMgr, ProofNodeManager* pnm) : d_propEngine(nullptr), d_env(env), d_logicInfo(env.getLogicInfo()), - d_outMgr(outMgr), d_pnm(pnm), d_lazyProof(d_pnm != nullptr ? new LazyCDProof(d_pnm, @@ -361,8 +359,8 @@ void TheoryEngine::printAssertions(const char* tag) { void TheoryEngine::dumpAssertions(const char* tag) { if (Dump.isOn(tag)) { - const Printer& printer = d_outMgr.getPrinter(); - std::ostream& out = d_outMgr.getDumpOut(); + const Printer& printer = d_env.getPrinter(); + std::ostream& out = d_env.getDumpOut(); printer.toStreamCmdComment(out, "Starting completeness check"); for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) { Theory* theory = d_theoryTable[theoryId]; @@ -1358,8 +1356,8 @@ void TheoryEngine::lemma(TrustNode tlemma, if(Dump.isOn("t-lemmas")) { // we dump the negation of the lemma, to show validity of the lemma Node n = lemma.negate(); - const Printer& printer = d_outMgr.getPrinter(); - std::ostream& out = d_outMgr.getDumpOut(); + const Printer& printer = d_env.getPrinter(); + std::ostream& out = d_env.getDumpOut(); printer.toStreamCmdComment(out, "theory lemma: expect valid"); printer.toStreamCmdCheckSat(out, n); } @@ -1413,8 +1411,8 @@ void TheoryEngine::conflict(TrustNode tconflict, TheoryId theoryId) markInConflict(); if(Dump.isOn("t-conflicts")) { - const Printer& printer = d_outMgr.getPrinter(); - std::ostream& out = d_outMgr.getDumpOut(); + const Printer& printer = d_env.getPrinter(); + std::ostream& out = d_env.getDumpOut(); printer.toStreamCmdComment(out, "theory conflict: expect unsat"); printer.toStreamCmdCheckSat(out, conflict); } diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 5d16f04ba..0c4a80c98 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -44,7 +44,6 @@ namespace cvc5 { class Env; class ResourceManager; -class OutputManager; class TheoryEngineProofGenerator; class ProofChecker; @@ -132,9 +131,6 @@ class TheoryEngine { TypeNode d_sepLocType; TypeNode d_sepDataType; - /** Reference to the output manager of the smt engine */ - OutputManager& d_outMgr; - //--------------------------------- new proofs /** Proof node manager used by this theory engine, if proofs are enabled */ ProofNodeManager* d_pnm; @@ -299,7 +295,7 @@ class TheoryEngine { public: /** Constructs a theory engine */ - TheoryEngine(Env& env, OutputManager& outMgr, ProofNodeManager* pnm); + TheoryEngine(Env& env, ProofNodeManager* pnm); /** Destroys a theory engine */ ~TheoryEngine(); diff --git a/test/unit/prop/cnf_stream_white.cpp b/test/unit/prop/cnf_stream_white.cpp index 4dfd7a1bb..bc5bfe8f1 100644 --- a/test/unit/prop/cnf_stream_white.cpp +++ b/test/unit/prop/cnf_stream_white.cpp @@ -115,7 +115,7 @@ class TestPropWhiteCnfStream : public TestSmt new cvc5::prop::CnfStream(d_satSolver.get(), d_cnfRegistrar.get(), d_cnfContext.get(), - &d_smtEngine->getOutputManager(), + &d_smtEngine->getEnv(), d_smtEngine->getResourceManager())); } -- 2.30.2