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.

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 4897f8e6a33a140a9d549e9fe32394363b84a292..e04651fc3b8c8e6057095cff5bc2b9df28d9b474 100644 (file)
--- 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 aeed973806cdedce32861ebb9051511ae0838789..664a2bf6190be211752bdea70b4b1564c5f4def1 100644 (file)
--- 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<TNode> d_booleanVariables;

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 24b98577f8e66e46d2959f12945b464a104851fa..0308715e63f65b6408bc7580f573b2d237eb0db7 100644 (file)
--- 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 e458ca5e532aed5685be52b58d8bd59080d61324..4d06adfba914828bf63245160f5360cd1bcca444 100644 (file)
--- 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 774d8b19247e82a1091efb590caf3b036bebd9c3..55f3d1c5fb2f8f5da5702d50210a76ee73f9ac56 100644 (file)
--- 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<Node> assump;
   if (!assumption.isNull())
@@ -852,11 +848,11 @@ Result SmtEngine::checkSat(const std::vector<Node>& 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<Node>() : std::vector<Node>{node},
@@ -975,8 +971,7 @@ std::vector<Node> SmtEngine::getUnsatAssumptions(void)
   finishInit();
   if (Dump.isOn("benchmark"))
   {
-    getPrinter().toStreamCmdGetUnsatAssumptions(
-        getOutputManager().getDumpOut());
+    getPrinter().toStreamCmdGetUnsatAssumptions(d_env->getDumpOut());
   }
   UnsatCore core = getUnsatCoreInternal();
   std::vector<Node> 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<Node>& 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<Node> 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 6d3326603e77970e425eee649bf53354d7f13485..503d9d1db25766b599726f0e08d5384b754c3ee5 100644 (file)
--- 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 ea89f6d575638df22ec3624b6850edcb9edd536b..cf82d93093eefb57f610e37d9232a9a5994b0171 100644 (file)
--- 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 fb93403b96dfb4d7eacfdc5a66614e45a5a3cd84..233ea64ed39b6208d95587e2d1b4170668ea9f5a 100644 (file)
--- 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 5d16f04ba475ed58b6e2bc85f8cd680e0695f2c8..0c4a80c98d8d82709ef2b8aadd5bdd49b26e40eb 100644 (file)
--- 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 4dfd7a1bb740ee510b1fe60a224171bdedd8d584..bc5bfe8f1d5b387f50c39ff44fb1c790ffc8c5d2 100644 (file)
--- 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()));
   }