From 19c382b8666492fa8818444c7f2ee907da3d9479 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 3 Aug 2021 20:15:43 -0500
Subject: 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 -----
 4 files changed, 13 insertions(+), 20 deletions(-)

(limited to 'src/prop')

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<TNode> 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.
-- 
cgit v1.2.3