Minor cleanup of SmtEngine (#5450)

9 files changed, 73 insertions, 96 deletions

diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp
index 9b4d02032..a4e7ac703 100644
--- a/src/preprocessing/passes/unconstrained_simplifier.cpp
+++ b/src/preprocessing/passes/unconstrained_simplifier.cpp
@@ -34,8 +34,7 @@ UnconstrainedSimplifier::UnconstrainedSimplifier(
     : PreprocessingPass(preprocContext, "unconstrained-simplifier"),
       d_numUnconstrainedElim("preprocessor::number of unconstrained elims", 0),
       d_context(preprocContext->getDecisionContext()),
-      d_substitutions(preprocContext->getDecisionContext()),
-      d_logicInfo(preprocContext->getLogicInfo())
+      d_substitutions(preprocContext->getDecisionContext())
 {
   smtStatisticsRegistry()->registerStat(&d_numUnconstrainedElim);
 }
@@ -588,7 +587,7 @@ void UnconstrainedSimplifier::processUnconstrained()
         // Uninterpreted function - if domain is infinite, no quantifiers are
         // used, and any child is unconstrained, result is unconstrained
         case kind::APPLY_UF:
-          if (d_logicInfo.isQuantified()
+          if (d_preprocContext->getLogicInfo().isQuantified()
               || !current.getType().getCardinality().isInfinite())
           {
             break;
diff --git a/src/preprocessing/passes/unconstrained_simplifier.h b/src/preprocessing/passes/unconstrained_simplifier.h
index 8c7457b92..ebfe51e79 100644
--- a/src/preprocessing/passes/unconstrained_simplifier.h
+++ b/src/preprocessing/passes/unconstrained_simplifier.h
@@ -61,7 +61,6 @@ class UnconstrainedSimplifier : public PreprocessingPass
   context::Context* d_context;
   theory::SubstitutionMap d_substitutions;
 
-  const LogicInfo& d_logicInfo;
   /**
    * Visit all subterms in assertion. This method throws a LogicException if
    * there is a subterm that is unhandled by this preprocessing pass (e.g. a
diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h
index d0747b5d9..824197bc5 100644
--- a/src/preprocessing/preprocessing_pass_context.h
+++ b/src/preprocessing/preprocessing_pass_context.h
@@ -66,7 +66,8 @@ class PreprocessingPassContext
     d_resourceManager->spendResource(r);
   }
 
-  const LogicInfo& getLogicInfo() { return d_smt->d_logic; }
+  /** Get the current logic info of the SmtEngine */
+  const LogicInfo& getLogicInfo() { return d_smt->getLogicInfo(); }
 
   /* Widen the logic to include the given theory. */
   void widenLogic(theory::TheoryId id);
diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp
index 912c0ea28..98a2a7a36 100644
--- a/src/smt/preprocessor.cpp
+++ b/src/smt/preprocessor.cpp
@@ -29,13 +29,14 @@ namespace smt {
 
 Preprocessor::Preprocessor(SmtEngine& smt,
                            context::UserContext* u,
-                           AbstractValues& abs)
+                           AbstractValues& abs,
+                           SmtEngineStatistics& stats)
     : d_context(u),
       d_smt(smt),
       d_absValues(abs),
       d_propagator(true, true),
       d_assertionsProcessed(u, false),
-      d_processor(smt, *smt.getResourceManager()),
+      d_processor(smt, *smt.getResourceManager(), stats),
       d_rtf(u),
       d_pnm(nullptr)
 {
diff --git a/src/smt/preprocessor.h b/src/smt/preprocessor.h
index b07e7ec97..cb83f969e 100644
--- a/src/smt/preprocessor.h
+++ b/src/smt/preprocessor.h
@@ -41,7 +41,10 @@ class AbstractValues;
 class Preprocessor
 {
  public:
-  Preprocessor(SmtEngine& smt, context::UserContext* u, AbstractValues& abs);
+  Preprocessor(SmtEngine& smt,
+               context::UserContext* u,
+               AbstractValues& abs,
+               SmtEngineStatistics& stats);
   ~Preprocessor();
   /**
    * Finish initialization
diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp
index 387085de8..2011e7b83 100644
--- a/src/smt/process_assertions.cpp
+++ b/src/smt/process_assertions.cpp
@@ -52,8 +52,13 @@ class ScopeCounter
   unsigned& d_depth;
 };
 
-ProcessAssertions::ProcessAssertions(SmtEngine& smt, ResourceManager& rm)
-    : d_smt(smt), d_resourceManager(rm), d_preprocessingPassContext(nullptr)
+ProcessAssertions::ProcessAssertions(SmtEngine& smt,
+                                     ResourceManager& rm,
+                                     SmtEngineStatistics& stats)
+    : d_smt(smt),
+      d_resourceManager(rm),
+      d_smtStats(stats),
+      d_preprocessingPassContext(nullptr)
 {
   d_true = NodeManager::currentNM()->mkConst(true);
 }
@@ -127,7 +132,7 @@ bool ProcessAssertions::apply(Assertions& as)
     Chat() << "expanding definitions..." << endl;
     Trace("simplify") << "ProcessAssertions::simplify(): expanding definitions"
                       << endl;
-    TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_definitionExpansionTime);
+    TimerStat::CodeTimer codeTimer(d_smtStats.d_definitionExpansionTime);
     unordered_map<Node, Node, NodeHashFunction> cache;
     for (size_t i = 0, nasserts = assertions.size(); i < nasserts; ++i)
     {
@@ -232,7 +237,7 @@ bool ProcessAssertions::apply(Assertions& as)
     d_passes["sep-skolem-emp"]->apply(&assertions);
   }
 
-  if (d_smt.d_logic.isQuantified())
+  if (d_smt.getLogicInfo().isQuantified())
   {
     // remove rewrite rules, apply pre-skolemization to existential quantifiers
     d_passes["quantifiers-preprocess"]->apply(&assertions);
@@ -261,7 +266,7 @@ bool ProcessAssertions::apply(Assertions& as)
   }
 
   // rephrasing normal inputs as sygus problems
-  if (!d_smt.d_isInternalSubsolver)
+  if (!d_smt.isInternalSubsolver())
   {
     if (options::sygusInference())
     {
@@ -281,7 +286,7 @@ bool ProcessAssertions::apply(Assertions& as)
   noConflict = simplifyAssertions(assertions);
   if (!noConflict)
   {
-    ++(d_smt.d_stats->d_simplifiedToFalse);
+    ++(d_smtStats.d_simplifiedToFalse);
   }
   Trace("smt-proc") << "ProcessAssertions::processAssertions() : post-simplify"
                     << endl;
@@ -294,13 +299,13 @@ bool ProcessAssertions::apply(Assertions& as)
   Debug("smt") << " assertions     : " << assertions.size() << endl;
 
   {
-    d_smt.d_stats->d_numAssertionsPre += assertions.size();
+    d_smtStats.d_numAssertionsPre += assertions.size();
     d_passes["ite-removal"]->apply(&assertions);
     // This is needed because when solving incrementally, removeITEs may
     // introduce skolems that were solved for earlier and thus appear in the
     // substitution map.
     d_passes["apply-substs"]->apply(&assertions);
-    d_smt.d_stats->d_numAssertionsPost += assertions.size();
+    d_smtStats.d_numAssertionsPost += assertions.size();
   }
 
   dumpAssertions("pre-repeat-simplify", assertions);
@@ -456,7 +461,7 @@ bool ProcessAssertions::simplifyAssertions(AssertionPipeline& assertions)
       if (  // check that option is on
           options::arithMLTrick() &&
           // only useful in arith
-          d_smt.d_logic.isTheoryEnabled(THEORY_ARITH) &&
+          d_smt.getLogicInfo().isTheoryEnabled(THEORY_ARITH) &&
           // we add new assertions and need this (in practice, this
           // restriction only disables miplib processing during
           // re-simplification, which we don't expect to be useful anyway)
@@ -550,7 +555,7 @@ Node ProcessAssertions::expandDefinitions(
     unordered_map<Node, Node, NodeHashFunction>& cache,
     bool expandOnly)
 {
-  NodeManager* nm = d_smt.d_nodeManager;
+  NodeManager* nm = d_smt.getNodeManager();
   std::stack<std::tuple<Node, Node, bool>> worklist;
   std::stack<Node> result;
   worklist.push(std::make_tuple(Node(n), Node(n), false));
@@ -577,9 +582,9 @@ Node ProcessAssertions::expandDefinitions(
       // we can short circuit (variable) leaves
       if (n.isVar())
       {
-        SmtEngine::DefinedFunctionMap::const_iterator i =
-            d_smt.d_definedFunctions->find(n);
-        if (i != d_smt.d_definedFunctions->end())
+        SmtEngine::DefinedFunctionMap* dfuns = d_smt.getDefinedFunctionMap();
+        SmtEngine::DefinedFunctionMap::const_iterator i = dfuns->find(n);
+        if (i != dfuns->end())
         {
           Node f = (*i).second.getFormula();
           // must expand its definition
@@ -651,9 +656,9 @@ Node ProcessAssertions::expandDefinitions(
         {
           // application of a user-defined symbol
           TNode func = n.getOperator();
-          SmtEngine::DefinedFunctionMap::const_iterator i =
-              d_smt.d_definedFunctions->find(func);
-          if (i == d_smt.d_definedFunctions->end())
+          SmtEngine::DefinedFunctionMap* dfuns = d_smt.getDefinedFunctionMap();
+          SmtEngine::DefinedFunctionMap::const_iterator i = dfuns->find(func);
+          if (i == dfuns->end())
           {
             throw TypeCheckingException(
                 n.toExpr(),
diff --git a/src/smt/process_assertions.h b/src/smt/process_assertions.h
index a4f16ab1d..d260edf14 100644
--- a/src/smt/process_assertions.h
+++ b/src/smt/process_assertions.h
@@ -57,7 +57,9 @@ class ProcessAssertions
   typedef unordered_map<Node, bool, NodeHashFunction> NodeToBoolHashMap;
 
  public:
-  ProcessAssertions(SmtEngine& smt, ResourceManager& rm);
+  ProcessAssertions(SmtEngine& smt,
+                    ResourceManager& rm,
+                    SmtEngineStatistics& stats);
   ~ProcessAssertions();
   /** Finish initialize
    *
@@ -92,6 +94,8 @@ class ProcessAssertions
   SmtEngine& d_smt;
   /** Reference to resource manager */
   ResourceManager& d_resourceManager;
+  /** Reference to the SMT stats */
+  SmtEngineStatistics& d_smtStats;
   /** The preprocess context */
   preprocessing::PreprocessingPassContext* d_preprocessingPassContext;
   /** True node */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 9826cd097..8aad05235 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -18,21 +18,15 @@
 
 #include "api/cvc4cpp.h"
 #include "base/check.h"
-#include "base/configuration.h"
-#include "base/configuration_private.h"
 #include "base/exception.h"
 #include "base/modal_exception.h"
 #include "base/output.h"
 #include "decision/decision_engine.h"
 #include "expr/node.h"
-#include "expr/node_self_iterator.h"
-#include "expr/node_visitor.h"
 #include "options/base_options.h"
 #include "options/language.h"
 #include "options/main_options.h"
-#include "options/option_exception.h"
 #include "options/printer_options.h"
-#include "options/set_language.h"
 #include "options/smt_options.h"
 #include "options/theory_options.h"
 #include "printer/printer.h"
@@ -60,19 +54,18 @@
 #include "smt/smt_engine_stats.h"
 #include "smt/smt_solver.h"
 #include "smt/sygus_solver.h"
-#include "smt/term_formula_removal.h"
-#include "smt/update_ostream.h"
-#include "theory/logic_info.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/rewriter.h"
 #include "theory/smt_engine_subsolver.h"
 #include "theory/theory_engine.h"
-#include "util/hash.h"
 #include "util/random.h"
 #include "util/resource_manager.h"
 
+// required for hacks related to old proofs for unsat cores
+#include "base/configuration.h"
+#include "base/configuration_private.h"
+
 using namespace std;
-using namespace CVC4;
 using namespace CVC4::smt;
 using namespace CVC4::preprocessing;
 using namespace CVC4::prop;
@@ -136,14 +129,15 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr)
   d_resourceManager.reset(
       new ResourceManager(*d_statisticsRegistry.get(), d_options));
   d_optm.reset(new smt::OptionsManager(&d_options, d_resourceManager.get()));
-  d_pp.reset(
-      new smt::Preprocessor(*this, getUserContext(), *d_absValues.get()));
   // listen to node manager events
   d_nodeManager->subscribeEvents(d_snmListener.get());
   // listen to resource out
   d_resourceManager->registerListener(d_routListener.get());
   // make statistics
   d_stats.reset(new SmtEngineStatistics());
+  // reset the preprocessor
+  d_pp.reset(new smt::Preprocessor(
+      *this, getUserContext(), *d_absValues.get(), *d_stats));
   // make the SMT solver
   d_smtSolver.reset(
       new SmtSolver(*this, *d_state, d_resourceManager.get(), *d_pp, *d_stats));
@@ -397,9 +391,8 @@ void SmtEngine::setLogic(const std::string& s)
 }
 
 void SmtEngine::setLogic(const char* logic) { setLogic(string(logic)); }
-LogicInfo SmtEngine::getLogicInfo() const {
-  return d_logic;
-}
+
+const LogicInfo& SmtEngine::getLogicInfo() const { return d_logic; }
 
 LogicInfo SmtEngine::getUserLogicInfo() const
 {
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 7a55d3b74..d8d2ea171 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -50,19 +50,13 @@ typedef NodeTemplate<true> Node;
 typedef NodeTemplate<false> TNode;
 struct NodeHashFunction;
 
-class Command;
-class GetModelCommand;
-
 class SmtEngine;
 class DecisionEngine;
 class TheoryEngine;
-
 class ProofManager;
 class UnsatCore;
-
 class LogicRequest;
 class StatisticsRegistry;
-
 class Printer;
 
 /* -------------------------------------------------------------------------- */
@@ -134,32 +128,15 @@ namespace theory {
   class Rewriter;
 }/* CVC4::theory namespace */
 
-// TODO: SAT layer (esp. CNF- versus non-clausal solvers under the
-// hood): use a type parameter and have check() delegate, or subclass
-// SmtEngine and override check()?
-//
-// Probably better than that is to have a configuration object that
-// indicates which passes are desired.  The configuration occurs
-// elsewhere (and can even occur at runtime).  A simple "pass manager"
-// of sorts determines check()'s behavior.
-//
-// The CNF conversion can go on in PropEngine.
 
 /* -------------------------------------------------------------------------- */
 
 class CVC4_PUBLIC SmtEngine
 {
   friend class ::CVC4::api::Solver;
-  // TODO (Issue #1096): Remove this friend relationship.
-  friend class ::CVC4::preprocessing::PreprocessingPassContext;
   friend class ::CVC4::smt::SmtEngineState;
   friend class ::CVC4::smt::SmtScope;
-  friend class ::CVC4::smt::ProcessAssertions;
-  friend class ::CVC4::smt::SmtSolver;
-  friend ProofManager* ::CVC4::smt::currentProofManager();
   friend class ::CVC4::LogicRequest;
-  friend class ::CVC4::theory::TheoryModel;
-  friend class ::CVC4::theory::Rewriter;
 
   /* .......................................................................  */
  public:
@@ -237,7 +214,7 @@ class CVC4_PUBLIC SmtEngine
   void setLogic(const LogicInfo& logic);
 
   /** Get the logic information currently set. */
-  LogicInfo getLogicInfo() const;
+  const LogicInfo& getLogicInfo() const;
 
   /** Get the logic information set by the user. */
   LogicInfo getUserLogicInfo() const;
@@ -865,6 +842,24 @@ class CVC4_PUBLIC SmtEngine
   Options& getOptions();
   const Options& getOptions() const;
 
+  /** Get a pointer to the UserContext owned by this SmtEngine. */
+  context::UserContext* getUserContext();
+
+  /** Get a pointer to the Context owned by this SmtEngine. */
+  context::Context* getContext();
+
+  /** Get a pointer to the TheoryEngine owned by this SmtEngine. */
+  TheoryEngine* getTheoryEngine();
+
+  /** Get a pointer to the PropEngine owned by this SmtEngine. */
+  prop::PropEngine* getPropEngine();
+
+  /**
+   * Get a pointer to the ProofManager owned by this SmtEngine.
+   * TODO (project #37): this is the old proof manager and will be deleted
+   */
+  ProofManager* getProofManager() { return d_proofManager.get(); };
+
   /** Get the resource manager of this SMT engine */
   ResourceManager* getResourceManager();
 
@@ -880,6 +875,12 @@ class CVC4_PUBLIC SmtEngine
   /** Get a pointer to the Rewriter owned by this SmtEngine. */
   theory::Rewriter* getRewriter() { return d_rewriter.get(); }
 
+  /** The type of our internal map of defined functions */
+  using DefinedFunctionMap =
+      context::CDHashMap<Node, smt::DefinedFunction, NodeHashFunction>;
+
+  /** Get the defined function map */
+  DefinedFunctionMap* getDefinedFunctionMap() { return d_definedFunctions; }
   /**
    * Get expanded assertions.
    *
@@ -889,10 +890,6 @@ class CVC4_PUBLIC SmtEngine
   /* .......................................................................  */
  private:
   /* .......................................................................  */
-
-  /** The type of our internal map of defined functions */
-  typedef context::CDHashMap<Node, smt::DefinedFunction, NodeHashFunction>
-      DefinedFunctionMap;
   /** The type of our internal assertion list */
   typedef context::CDList<Node> AssertionList;
 
@@ -903,24 +900,6 @@ class CVC4_PUBLIC SmtEngine
   /** Set solver instance that owns this SmtEngine. */
   void setSolver(api::Solver* solver) { d_solver = solver; }
 
-  /** Get a pointer to the UserContext owned by this SmtEngine. */
-  context::UserContext* getUserContext();
-
-  /** Get a pointer to the Context owned by this SmtEngine. */
-  context::Context* getContext();
-
-  /** Get a pointer to the TheoryEngine owned by this SmtEngine. */
-  TheoryEngine* getTheoryEngine();
-
-  /** Get a pointer to the PropEngine owned by this SmtEngine. */
-  prop::PropEngine* getPropEngine();
-
-  /**
-   * Get a pointer to the ProofManager owned by this SmtEngine.
-   * TODO (project #37): this is the old proof manager and will be deleted
-   */
-  ProofManager* getProofManager() { return d_proofManager.get(); };
-
   /** Get a pointer to the StatisticsRegistry owned by this SmtEngine. */
   StatisticsRegistry* getStatisticsRegistry()
   {
@@ -1021,15 +1000,6 @@ class CVC4_PUBLIC SmtEngine
    */
   void setLogicInternal();
 
-  /**
-   * Add to Model command.  This is used for recording a command
-   * that should be reported during a get-model call.
-   */
-  void addToModelCommandAndDump(const Command& c,
-                                uint32_t flags = 0,
-                                bool userVisible = true,
-                                const char* dumpTag = "declarations");
-
   /*
    * Check satisfiability (used to check satisfiability and entailment).
    */
@@ -1153,8 +1123,10 @@ class CVC4_PUBLIC SmtEngine
    */
   std::map<std::string, Integer> d_commandVerbosity;
 
+  /** The statistics registry */
   std::unique_ptr<StatisticsRegistry> d_statisticsRegistry;
 
+  /** The statistics class */
   std::unique_ptr<smt::SmtEngineStatistics> d_stats;
 
   /** The options object */