From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 25 Aug 2021 16:27:03 +0000 (-0500)
Subject: Eliminate calls to currentSmtEngine (#7060)
X-Git-Tag: cvc5-1.0.0~1338
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=76c8bc4c963b494db36074afac74e51ab39917e4;p=cvc5.git

Eliminate calls to currentSmtEngine (#7060)

Work towards supporting multiple solvers running in parallel.

There are now only 5 remaining internal calls to smt::currentSmtEngine.

More will be eliminated on future PRs.
---

diff --git a/src/preprocessing/passes/sort_infer.cpp b/src/preprocessing/passes/sort_infer.cpp
index 53f3feffc..3f6828a7b 100644
--- a/src/preprocessing/passes/sort_infer.cpp
+++ b/src/preprocessing/passes/sort_infer.cpp
@@ -20,7 +20,6 @@
 #include "preprocessing/assertion_pipeline.h"
 #include "preprocessing/preprocessing_pass_context.h"
 #include "smt/dump_manager.h"
-#include "smt/smt_engine_scope.h"
 #include "theory/rewriter.h"
 #include "theory/sort_inference.h"
 #include "theory/theory_engine.h"
@@ -72,7 +71,7 @@ PreprocessingPassResult SortInferencePass::applyInternal(
       assertionsToPreprocess->push_back(nar);
     }
     // indicate correspondence between the functions
-    SmtEngine* smt = smt::currentSmtEngine();
+    SmtEngine* smt = d_preprocContext->getSmt();
     smt::DumpManager* dm = smt->getDumpManager();
     for (const std::pair<const Node, Node>& mrf : model_replace_f)
     {
diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp
index 63af57592..e66b70934 100644
--- a/src/theory/datatypes/sygus_extension.cpp
+++ b/src/theory/datatypes/sygus_extension.cpp
@@ -1108,7 +1108,7 @@ Node SygusExtension::registerSearchValue(Node a,
             its = d_sampler[a].find(tn);
           }
           // check equivalent
-          its->second.checkEquivalent(bv, bvr);
+          its->second.checkEquivalent(bv, bvr, *d_state.options().base.out);
         }
       }
 
diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp
index c2ee563e3..0fd0eebd6 100644
--- a/src/theory/quantifiers/candidate_rewrite_database.cpp
+++ b/src/theory/quantifiers/candidate_rewrite_database.cpp
@@ -33,11 +33,10 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
-CandidateRewriteDatabase::CandidateRewriteDatabase(bool doCheck,
-                                                   bool rewAccel,
-                                                   bool silent,
-                                                   bool filterPairs)
-    : d_tds(nullptr),
+CandidateRewriteDatabase::CandidateRewriteDatabase(
+    Env& env, bool doCheck, bool rewAccel, bool silent, bool filterPairs)
+    : ExprMiner(env),
+      d_tds(nullptr),
       d_ext_rewrite(nullptr),
       d_doCheck(doCheck),
       d_rewAccel(rewAccel),
diff --git a/src/theory/quantifiers/candidate_rewrite_database.h b/src/theory/quantifiers/candidate_rewrite_database.h
index 309aaf4b7..71ae5649f 100644
--- a/src/theory/quantifiers/candidate_rewrite_database.h
+++ b/src/theory/quantifiers/candidate_rewrite_database.h
@@ -45,6 +45,7 @@ class CandidateRewriteDatabase : public ExprMiner
  public:
   /**
    * Constructor
+   * @param env Reference to the environment
    * @param doCheck Whether to check rewrite rules using subsolvers.
    * @param rewAccel Whether to construct symmetry breaking lemmas based on
    * discovered rewrites (see option sygusRewSynthAccel()).
@@ -53,7 +54,8 @@ class CandidateRewriteDatabase : public ExprMiner
    * @param filterPairs Whether to filter rewrite pairs using filtering
    * techniques from the SAT 2019 paper above.
    */
-  CandidateRewriteDatabase(bool doCheck,
+  CandidateRewriteDatabase(Env& env,
+                           bool doCheck,
                            bool rewAccel = false,
                            bool silent = false,
                            bool filterPairs = true);
diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp
index 0f46fa790..fa156c839 100644
--- a/src/theory/quantifiers/expr_miner.cpp
+++ b/src/theory/quantifiers/expr_miner.cpp
@@ -17,11 +17,8 @@
 
 #include "expr/skolem_manager.h"
 #include "options/quantifiers_options.h"
-#include "smt/smt_engine.h"
-#include "smt/smt_engine_scope.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/rewriter.h"
-#include "theory/smt_engine_subsolver.h"
 
 using namespace std;
 using namespace cvc5::kind;
diff --git a/src/theory/quantifiers/expr_miner.h b/src/theory/quantifiers/expr_miner.h
index 79d0c6650..8a5ce1c1f 100644
--- a/src/theory/quantifiers/expr_miner.h
+++ b/src/theory/quantifiers/expr_miner.h
@@ -23,10 +23,14 @@
 #include <vector>
 
 #include "expr/node.h"
-#include "smt/smt_engine.h"
 #include "theory/quantifiers/sygus_sampler.h"
+#include "theory/smt_engine_subsolver.h"
 
 namespace cvc5 {
+
+class Env;
+class SmtEngine;
+
 namespace theory {
 namespace quantifiers {
 
@@ -39,7 +43,7 @@ namespace quantifiers {
 class ExprMiner
 {
  public:
-  ExprMiner() : d_sampler(nullptr) {}
+  ExprMiner(Env& env) : d_env(env), d_sampler(nullptr) {}
   virtual ~ExprMiner() {}
   /** initialize
    *
@@ -60,6 +64,8 @@ class ExprMiner
   virtual bool addTerm(Node n, std::ostream& out) = 0;
 
  protected:
+  /** Reference to the env */
+  Env& d_env;
   /** the set of variables used by this class */
   std::vector<Node> d_vars;
   /**
diff --git a/src/theory/quantifiers/expr_miner_manager.cpp b/src/theory/quantifiers/expr_miner_manager.cpp
index 24ab7c30a..92b7c105d 100644
--- a/src/theory/quantifiers/expr_miner_manager.cpp
+++ b/src/theory/quantifiers/expr_miner_manager.cpp
@@ -21,13 +21,19 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
-ExpressionMinerManager::ExpressionMinerManager()
-    : d_doRewSynth(false),
+ExpressionMinerManager::ExpressionMinerManager(Env& env)
+    : d_env(env),
+      d_doRewSynth(false),
       d_doQueryGen(false),
       d_doFilterLogicalStrength(false),
       d_use_sygus_type(false),
       d_tds(nullptr),
-      d_crd(options::sygusRewSynthCheck(), options::sygusRewSynthAccel(), false)
+      d_crd(env,
+            options::sygusRewSynthCheck(),
+            options::sygusRewSynthAccel(),
+            false),
+      d_qg(env),
+      d_sols(env)
 {
 }
 
diff --git a/src/theory/quantifiers/expr_miner_manager.h b/src/theory/quantifiers/expr_miner_manager.h
index 32bc4744f..b38de1337 100644
--- a/src/theory/quantifiers/expr_miner_manager.h
+++ b/src/theory/quantifiers/expr_miner_manager.h
@@ -26,10 +26,10 @@
 #include "theory/quantifiers/sygus_sampler.h"
 
 namespace cvc5 {
-namespace theory {
 
-class QuantifiersEngine;
+class Env;
 
+namespace theory {
 namespace quantifiers {
 
 /** ExpressionMinerManager
@@ -42,7 +42,7 @@ namespace quantifiers {
 class ExpressionMinerManager
 {
  public:
-  ExpressionMinerManager();
+  ExpressionMinerManager(Env& env);
   ~ExpressionMinerManager() {}
   /**  Initialize this class
    *
@@ -93,6 +93,8 @@ class ExpressionMinerManager
   bool addTerm(Node sol, std::ostream& out, bool& rew_print);
 
  private:
+  /** Reference to the env */
+  Env& d_env;
   /** whether we are doing rewrite synthesis */
   bool d_doRewSynth;
   /** whether we are doing query generation */
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index 05361eaa1..be1633d16 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -24,8 +24,6 @@
 #include "proof/lazy_proof.h"
 #include "proof/proof_node_manager.h"
 #include "smt/logic_exception.h"
-#include "smt/smt_engine.h"
-#include "smt/smt_engine_scope.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/quantifiers/cegqi/inst_strategy_cegqi.h"
 #include "theory/quantifiers/first_order_model.h"
diff --git a/src/theory/quantifiers/query_generator.cpp b/src/theory/quantifiers/query_generator.cpp
index 3c3dd8d84..31d8c3c22 100644
--- a/src/theory/quantifiers/query_generator.cpp
+++ b/src/theory/quantifiers/query_generator.cpp
@@ -20,8 +20,6 @@
 #include <sstream>
 
 #include "options/quantifiers_options.h"
-#include "smt/smt_engine.h"
-#include "smt/smt_engine_scope.h"
 #include "util/random.h"
 
 using namespace std;
@@ -31,7 +29,7 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
-QueryGenerator::QueryGenerator() : d_queryCount(0) {}
+QueryGenerator::QueryGenerator(Env& env) : ExprMiner(env), d_queryCount(0) {}
 void QueryGenerator::initialize(const std::vector<Node>& vars, SygusSampler* ss)
 {
   Assert(ss != nullptr);
diff --git a/src/theory/quantifiers/query_generator.h b/src/theory/quantifiers/query_generator.h
index 90b30a016..7738a4fe5 100644
--- a/src/theory/quantifiers/query_generator.h
+++ b/src/theory/quantifiers/query_generator.h
@@ -52,7 +52,7 @@ namespace quantifiers {
 class QueryGenerator : public ExprMiner
 {
  public:
-  QueryGenerator();
+  QueryGenerator(Env& env);
   ~QueryGenerator() {}
   /** initialize */
   void initialize(const std::vector<Node>& vars,
diff --git a/src/theory/quantifiers/solution_filter.cpp b/src/theory/quantifiers/solution_filter.cpp
index ccc0763b7..8844950c7 100644
--- a/src/theory/quantifiers/solution_filter.cpp
+++ b/src/theory/quantifiers/solution_filter.cpp
@@ -19,8 +19,6 @@
 
 #include "options/base_options.h"
 #include "options/quantifiers_options.h"
-#include "smt/smt_engine.h"
-#include "smt/smt_engine_scope.h"
 #include "util/random.h"
 
 using namespace cvc5::kind;
@@ -29,7 +27,10 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
-SolutionFilterStrength::SolutionFilterStrength() : d_isStrong(true) {}
+SolutionFilterStrength::SolutionFilterStrength(Env& env)
+    : ExprMiner(env), d_isStrong(true)
+{
+}
 void SolutionFilterStrength::initialize(const std::vector<Node>& vars,
                                         SygusSampler* ss)
 {
@@ -91,7 +92,7 @@ bool SolutionFilterStrength::addTerm(Node n, std::ostream& out)
       }
       else
       {
-        Options& opts = smt::currentSmtEngine()->getOptions();
+        const Options& opts = d_env.getOptions();
         std::ostream* smtOut = opts.base.out;
         (*smtOut) << "; (filtered " << (d_isStrong ? s : s.negate()) << ")"
                   << std::endl;
diff --git a/src/theory/quantifiers/solution_filter.h b/src/theory/quantifiers/solution_filter.h
index 43545d6d9..e3da8c986 100644
--- a/src/theory/quantifiers/solution_filter.h
+++ b/src/theory/quantifiers/solution_filter.h
@@ -40,7 +40,7 @@ namespace quantifiers {
 class SolutionFilterStrength : public ExprMiner
 {
  public:
-  SolutionFilterStrength();
+  SolutionFilterStrength(Env& d_env);
   ~SolutionFilterStrength() {}
   /** initialize */
   void initialize(const std::vector<Node>& vars,
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index 99a5126aa..f1caca1c4 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -17,8 +17,6 @@
 #include "expr/skolem_manager.h"
 #include "options/quantifiers_options.h"
 #include "smt/logic_exception.h"
-#include "smt/smt_engine.h"
-#include "smt/smt_engine_scope.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
@@ -39,9 +37,9 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
-CegSingleInv::CegSingleInv(TermRegistry& tr, SygusStatistics& s)
+CegSingleInv::CegSingleInv(Env& env, TermRegistry& tr, SygusStatistics& s)
     : d_sip(new SingleInvocationPartition),
-      d_srcons(new SygusReconstruct(tr.getTermDatabaseSygus(), s)),
+      d_srcons(new SygusReconstruct(env, tr.getTermDatabaseSygus(), s)),
       d_isSolved(false),
       d_single_invocation(false),
       d_treg(tr)
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.h b/src/theory/quantifiers/sygus/ce_guided_single_inv.h
index 72d41592a..13757dba9 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.h
@@ -91,7 +91,7 @@ class CegSingleInv
   Node d_single_inv;
   
  public:
-  CegSingleInv(TermRegistry& tr, SygusStatistics& s);
+  CegSingleInv(Env& env, TermRegistry& tr, SygusStatistics& s);
   ~CegSingleInv();
 
   // get simplified conjecture
diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
index 4bcede905..165326db7 100644
--- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp
+++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
@@ -19,8 +19,6 @@
 #include "options/base_options.h"
 #include "printer/printer.h"
 #include "proof/unsat_core.h"
-#include "smt/smt_engine.h"
-#include "smt/smt_engine_scope.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
 #include "theory/quantifiers/sygus/ce_guided_single_inv.h"
 #include "theory/quantifiers/sygus/transition_inference.h"
diff --git a/src/theory/quantifiers/sygus/enum_value_manager.cpp b/src/theory/quantifiers/sygus/enum_value_manager.cpp
index fd92e4d23..8a2d70bfa 100644
--- a/src/theory/quantifiers/sygus/enum_value_manager.cpp
+++ b/src/theory/quantifiers/sygus/enum_value_manager.cpp
@@ -14,6 +14,7 @@
  */
 #include "theory/quantifiers/sygus/enum_value_manager.h"
 
+#include "options/base_options.h"
 #include "options/datatypes_options.h"
 #include "options/quantifiers_options.h"
 #include "theory/datatypes/sygus_datatype_utils.h"
@@ -33,11 +34,13 @@ namespace theory {
 namespace quantifiers {
 
 EnumValueManager::EnumValueManager(Node e,
+                                   QuantifiersState& qs,
                                    QuantifiersInferenceManager& qim,
                                    TermRegistry& tr,
                                    SygusStatistics& s,
                                    bool hasExamples)
     : d_enum(e),
+      d_qstate(qs),
       d_qim(qim),
       d_treg(tr),
       d_stats(s),
@@ -98,14 +101,17 @@ Node EnumValueManager::getEnumeratedValue(bool& activeIncomplete)
         // create the enumerator callback
         if (options::sygusSymBreakDynamic())
         {
+          std::ostream* out = nullptr;
           if (options::sygusRewVerify())
           {
             d_samplerRrV.reset(new SygusSampler);
             d_samplerRrV->initializeSygus(
                 d_tds, e, options::sygusSamples(), false);
+            // use the default output for the output of sygusRewVerify
+            out = d_qstate.options().base.out;
           }
           d_secd.reset(new SygusEnumeratorCallbackDefault(
-              e, &d_stats, d_eec.get(), d_samplerRrV.get()));
+              e, &d_stats, d_eec.get(), d_samplerRrV.get(), out));
         }
         // if sygus repair const is enabled, we enumerate terms with free
         // variables as arguments to any-constant constructors
diff --git a/src/theory/quantifiers/sygus/enum_value_manager.h b/src/theory/quantifiers/sygus/enum_value_manager.h
index e610764e0..c786bb6f1 100644
--- a/src/theory/quantifiers/sygus/enum_value_manager.h
+++ b/src/theory/quantifiers/sygus/enum_value_manager.h
@@ -42,6 +42,7 @@ class EnumValueManager
 {
  public:
   EnumValueManager(Node e,
+                   QuantifiersState& qs,
                    QuantifiersInferenceManager& qim,
                    TermRegistry& tr,
                    SygusStatistics& s,
@@ -71,6 +72,8 @@ class EnumValueManager
   Node getModelValue(Node n);
   /** The enumerator */
   Node d_enum;
+  /** Reference to the quantifiers state */
+  QuantifiersState& d_qstate;
   /** Reference to the quantifiers inference manager */
   QuantifiersInferenceManager& d_qim;
   /** Reference to the term registry */
diff --git a/src/theory/quantifiers/sygus/rcons_type_info.cpp b/src/theory/quantifiers/sygus/rcons_type_info.cpp
index a1ae53ad1..78f8d303c 100644
--- a/src/theory/quantifiers/sygus/rcons_type_info.cpp
+++ b/src/theory/quantifiers/sygus/rcons_type_info.cpp
@@ -23,7 +23,8 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
-void RConsTypeInfo::initialize(TermDbSygus* tds,
+void RConsTypeInfo::initialize(Env& env,
+                               TermDbSygus* tds,
                                SygusStatistics& s,
                                TypeNode stn,
                                const std::vector<Node>& builtinVars)
@@ -33,7 +34,7 @@ void RConsTypeInfo::initialize(TermDbSygus* tds,
 
   d_enumerator.reset(new SygusEnumerator(tds, nullptr, &s, true));
   d_enumerator->initialize(sm->mkDummySkolem("sygus_rcons", stn));
-  d_crd.reset(new CandidateRewriteDatabase(true, false, true, false));
+  d_crd.reset(new CandidateRewriteDatabase(env, true, false, true, false));
   // since initial samples are not always useful for equivalence checks, set
   // their number to 0
   d_sygusSampler.initialize(stn, builtinVars, 0);
diff --git a/src/theory/quantifiers/sygus/rcons_type_info.h b/src/theory/quantifiers/sygus/rcons_type_info.h
index 4c9ae48e0..294454fe2 100644
--- a/src/theory/quantifiers/sygus/rcons_type_info.h
+++ b/src/theory/quantifiers/sygus/rcons_type_info.h
@@ -41,13 +41,15 @@ class RConsTypeInfo
    * Initialize a sygus enumerator and a candidate rewrite database for this
    * class' sygus datatype type.
    *
+   * @param env Reference to the environment
    * @param tds Database for sygus terms
    * @param s Statistics managed for the synth engine
    * @param stn The sygus datatype type encoding the syntax restrictions
    * @param builtinVars A list containing the builtin analog of sygus variable
    *                    list for the sygus datatype type
    */
-  void initialize(TermDbSygus* tds,
+  void initialize(Env& env,
+                  TermDbSygus* tds,
                   SygusStatistics& s,
                   TypeNode stn,
                   const std::vector<Node>& builtinVars);
diff --git a/src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp b/src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp
index 7b3236832..3b536695f 100644
--- a/src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp
+++ b/src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp
@@ -63,8 +63,12 @@ bool SygusEnumeratorCallback::addTerm(Node n, std::unordered_set<Node>& bterms)
 }
 
 SygusEnumeratorCallbackDefault::SygusEnumeratorCallbackDefault(
-    Node e, SygusStatistics* s, ExampleEvalCache* eec, SygusSampler* ssrv)
-    : SygusEnumeratorCallback(e, s), d_eec(eec), d_samplerRrV(ssrv)
+    Node e,
+    SygusStatistics* s,
+    ExampleEvalCache* eec,
+    SygusSampler* ssrv,
+    std::ostream* out)
+    : SygusEnumeratorCallback(e, s), d_eec(eec), d_samplerRrV(ssrv), d_out(out)
 {
 }
 void SygusEnumeratorCallbackDefault::notifyTermInternal(Node n,
@@ -73,7 +77,8 @@ void SygusEnumeratorCallbackDefault::notifyTermInternal(Node n,
 {
   if (d_samplerRrV != nullptr)
   {
-    d_samplerRrV->checkEquivalent(bn, bnr);
+    Assert(d_out != nullptr);
+    d_samplerRrV->checkEquivalent(bn, bnr, *d_out);
   }
 }
 
diff --git a/src/theory/quantifiers/sygus/sygus_enumerator_callback.h b/src/theory/quantifiers/sygus/sygus_enumerator_callback.h
index 46ca68c51..5ed28b309 100644
--- a/src/theory/quantifiers/sygus/sygus_enumerator_callback.h
+++ b/src/theory/quantifiers/sygus/sygus_enumerator_callback.h
@@ -86,7 +86,8 @@ class SygusEnumeratorCallbackDefault : public SygusEnumeratorCallback
   SygusEnumeratorCallbackDefault(Node e,
                                  SygusStatistics* s = nullptr,
                                  ExampleEvalCache* eec = nullptr,
-                                 SygusSampler* ssrv = nullptr);
+                                 SygusSampler* ssrv = nullptr,
+                                 std::ostream* out = nullptr);
   virtual ~SygusEnumeratorCallbackDefault() {}
 
  protected:
@@ -101,6 +102,8 @@ class SygusEnumeratorCallbackDefault : public SygusEnumeratorCallback
   ExampleEvalCache* d_eec;
   /** sampler (for --sygus-rr-verify) */
   SygusSampler* d_samplerRrV;
+  /** The output stream to print unsound rewrites for above */
+  std::ostream* d_out;
 };
 
 }  // namespace quantifiers
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
index d4d1398f4..209d10297 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
@@ -21,8 +21,6 @@
 #include "expr/dtype_cons.h"
 #include "expr/node_manager_attributes.h"  // for VarNameAttr
 #include "options/quantifiers_options.h"
-#include "smt/smt_engine.h"
-#include "smt/smt_engine_scope.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
 #include "theory/quantifiers/cegqi/ceg_instantiator.h"
 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
diff --git a/src/theory/quantifiers/sygus/sygus_interpol.h b/src/theory/quantifiers/sygus/sygus_interpol.h
index 07f5ed4ad..e86ac624a 100644
--- a/src/theory/quantifiers/sygus/sygus_interpol.h
+++ b/src/theory/quantifiers/sygus/sygus_interpol.h
@@ -22,9 +22,11 @@
 
 #include "expr/node.h"
 #include "expr/type_node.h"
-#include "smt/smt_engine.h"
 
 namespace cvc5 {
+
+class SmtEngine;
+
 namespace theory {
 namespace quantifiers {
 /**
diff --git a/src/theory/quantifiers/sygus/sygus_reconstruct.cpp b/src/theory/quantifiers/sygus/sygus_reconstruct.cpp
index 5da282606..3073a472d 100644
--- a/src/theory/quantifiers/sygus/sygus_reconstruct.cpp
+++ b/src/theory/quantifiers/sygus/sygus_reconstruct.cpp
@@ -26,8 +26,10 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
-SygusReconstruct::SygusReconstruct(TermDbSygus* tds, SygusStatistics& s)
-    : d_tds(tds), d_stats(s)
+SygusReconstruct::SygusReconstruct(Env& env,
+                                   TermDbSygus* tds,
+                                   SygusStatistics& s)
+    : d_env(env), d_tds(tds), d_stats(s)
 {
 }
 
@@ -408,7 +410,7 @@ void SygusReconstruct::initialize(TypeNode stn)
   // the database.
   for (TypeNode tn : sfTypes)
   {
-    d_stnInfo[tn].initialize(d_tds, d_stats, tn, builtinVars);
+    d_stnInfo[tn].initialize(d_env, d_tds, d_stats, tn, builtinVars);
   }
 }
 
diff --git a/src/theory/quantifiers/sygus/sygus_reconstruct.h b/src/theory/quantifiers/sygus/sygus_reconstruct.h
index e86b1688c..4102db713 100644
--- a/src/theory/quantifiers/sygus/sygus_reconstruct.h
+++ b/src/theory/quantifiers/sygus/sygus_reconstruct.h
@@ -144,10 +144,11 @@ class SygusReconstruct : public expr::NotifyMatch
   /**
    * Constructor.
    *
+   * @param env reference to the environment
    * @param tds database for sygus terms
    * @param s statistics managed for the synth engine
    */
-  SygusReconstruct(TermDbSygus* tds, SygusStatistics& s);
+  SygusReconstruct(Env& env, TermDbSygus* tds, SygusStatistics& s);
 
   /** Reconstruct solution.
    *
@@ -297,6 +298,8 @@ class SygusReconstruct : public expr::NotifyMatch
   void printPool(
       const std::unordered_map<TypeNode, std::vector<Node>>& pool) const;
 
+  /** Reference to the env */
+  Env& d_env;
   /** pointer to the sygus term database */
   TermDbSygus* d_tds;
   /** reference to the statistics of parent */
diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
index 739e9ab0d..d4611e6ca 100644
--- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
@@ -21,9 +21,6 @@
 #include "options/base_options.h"
 #include "options/quantifiers_options.h"
 #include "printer/printer.h"
-#include "smt/smt_engine.h"
-#include "smt/smt_engine_scope.h"
-#include "smt/smt_statistics_registry.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
 #include "theory/logic_info.h"
 #include "theory/quantifiers/cegqi/ceg_instantiator.h"
@@ -37,8 +34,8 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
-SygusRepairConst::SygusRepairConst(TermDbSygus* tds)
-    : d_tds(tds), d_allow_constant_grammar(false)
+SygusRepairConst::SygusRepairConst(Env& env, TermDbSygus* tds)
+    : d_env(env), d_tds(tds), d_allow_constant_grammar(false)
 {
 }
 
@@ -192,7 +189,7 @@ bool SygusRepairConst::repairSolution(Node sygusBody,
 
   // check whether it is not in the current logic, e.g. non-linear arithmetic.
   // if so, undo replacements until it is in the current logic.
-  LogicInfo logic = smt::currentSmtEngine()->getLogicInfo();
+  const LogicInfo& logic = d_env.getLogicInfo();
   if (logic.isTheoryEnabled(THEORY_ARITH) && logic.isLinear())
   {
     fo_body = fitToLogic(sygusBody,
@@ -531,7 +528,7 @@ Node SygusRepairConst::getFoQuery(Node body,
 }
 
 Node SygusRepairConst::fitToLogic(Node body,
-                                  LogicInfo& logic,
+                                  const LogicInfo& logic,
                                   Node n,
                                   const std::vector<Node>& candidates,
                                   std::vector<Node>& candidate_skeletons,
@@ -570,7 +567,7 @@ Node SygusRepairConst::fitToLogic(Node body,
   return Node::null();
 }
 
-bool SygusRepairConst::getFitToLogicExcludeVar(LogicInfo& logic,
+bool SygusRepairConst::getFitToLogicExcludeVar(const LogicInfo& logic,
                                                Node n,
                                                Node& exvar)
 {
diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.h b/src/theory/quantifiers/sygus/sygus_repair_const.h
index f0452a59c..ce6c81011 100644
--- a/src/theory/quantifiers/sygus/sygus_repair_const.h
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.h
@@ -23,6 +23,7 @@
 
 namespace cvc5 {
 
+class Env;
 class LogicInfo;
 
 namespace theory {
@@ -48,7 +49,7 @@ class TermDbSygus;
 class SygusRepairConst
 {
  public:
-  SygusRepairConst(TermDbSygus* tds);
+  SygusRepairConst(Env& env, TermDbSygus* tds);
   ~SygusRepairConst() {}
   /** initialize
    *
@@ -105,6 +106,8 @@ class SygusRepairConst
   static bool mustRepair(Node n);
 
  private:
+  /** Reference to the env */
+  Env& d_env;
   /** pointer to the sygus term database of d_qe */
   TermDbSygus* d_tds;
   /**
@@ -188,7 +191,7 @@ class SygusRepairConst
    * sk_vars.
    */
   Node fitToLogic(Node body,
-                  LogicInfo& logic,
+                  const LogicInfo& logic,
                   Node n,
                   const std::vector<Node>& candidates,
                   std::vector<Node>& candidate_skeletons,
@@ -205,7 +208,7 @@ class SygusRepairConst
    * exvar to x.
    * If n is in the given logic, this method returns true.
    */
-  bool getFitToLogicExcludeVar(LogicInfo& logic, Node n, Node& exvar);
+  bool getFitToLogicExcludeVar(const LogicInfo& logic, Node n, Node& exvar);
 };
 
 }  // namespace quantifiers
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 3f7ce158c..eeadbdd54 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -24,7 +24,6 @@
 #include "options/quantifiers_options.h"
 #include "printer/printer.h"
 #include "smt/logic_exception.h"
-#include "smt/smt_engine_scope.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/datatypes/sygus_datatype_utils.h"
 #include "theory/quantifiers/first_order_model.h"
@@ -57,13 +56,13 @@ SynthConjecture::SynthConjecture(QuantifiersState& qs,
       d_treg(tr),
       d_stats(s),
       d_tds(tr.getTermDatabaseSygus()),
-      d_verify(d_tds),
+      d_verify(qs.options(), d_tds),
       d_hasSolution(false),
-      d_ceg_si(new CegSingleInv(tr, s)),
+      d_ceg_si(new CegSingleInv(qs.getEnv(), tr, s)),
       d_templInfer(new SygusTemplateInfer),
       d_ceg_proc(new SynthConjectureProcess),
       d_ceg_gc(new CegGrammarConstructor(d_tds, this)),
-      d_sygus_rconst(new SygusRepairConst(d_tds)),
+      d_sygus_rconst(new SygusRepairConst(qs.getEnv(), d_tds)),
       d_exampleInfer(new ExampleInfer(d_tds)),
       d_ceg_pbe(new SygusPbe(qim, d_tds, this)),
       d_ceg_cegis(new Cegis(qim, d_tds, this)),
@@ -514,7 +513,7 @@ bool SynthConjecture::doCheck()
   {
     if (printDebug)
     {
-      Options& sopts = smt::currentSmtEngine()->getOptions();
+      const Options& sopts = d_qstate.options();
       std::ostream& out = *sopts.base.out;
       out << "(sygus-candidate ";
       Assert(d_quant[0].getNumChildren() == candidate_values.size());
@@ -764,7 +763,7 @@ EnumValueManager* SynthConjecture::getEnumValueManagerFor(Node e)
   bool hasExamples = (d_exampleInfer->hasExamples(f)
                       && d_exampleInfer->getNumExamples(f) != 0);
   d_enumManager[e].reset(
-      new EnumValueManager(e, d_qim, d_treg, d_stats, hasExamples));
+      new EnumValueManager(e, d_qstate, d_qim, d_treg, d_stats, hasExamples));
   EnumValueManager* eman = d_enumManager[e].get();
   // set up the examples
   if (hasExamples)
@@ -800,7 +799,7 @@ void SynthConjecture::printAndContinueStream(const std::vector<Node>& enums,
   Assert(d_master != nullptr);
   // we have generated a solution, print it
   // get the current output stream
-  Options& sopts = smt::currentSmtEngine()->getOptions();
+  const Options& sopts = d_qstate.options();
   printSynthSolutionInternal(*sopts.base.out);
   excludeCurrentSolution(enums, values);
 }
@@ -881,19 +880,21 @@ void SynthConjecture::printSynthSolutionInternal(std::ostream& out)
                      != options::SygusFilterSolMode::NONE))
       {
         Trace("cegqi-sol-debug") << "Run expression mining..." << std::endl;
-        std::map<Node, ExpressionMinerManager>::iterator its =
+        std::map<Node, std::unique_ptr<ExpressionMinerManager>>::iterator its =
             d_exprm.find(prog);
         if (its == d_exprm.end())
         {
-          d_exprm[prog].initializeSygus(
+          d_exprm[prog].reset(new ExpressionMinerManager(d_qstate.getEnv()));
+          ExpressionMinerManager* emm = d_exprm[prog].get();
+          emm->initializeSygus(
               d_tds, d_candidates[i], options::sygusSamples(), true);
           if (options::sygusRewSynth())
           {
-            d_exprm[prog].enableRewriteRuleSynth();
+            emm->enableRewriteRuleSynth();
           }
           if (options::sygusQueryGen())
           {
-            d_exprm[prog].enableQueryGeneration(options::sygusQueryGenThresh());
+            emm->enableQueryGeneration(options::sygusQueryGenThresh());
           }
           if (options::sygusFilterSolMode()
               != options::SygusFilterSolMode::NONE)
@@ -901,18 +902,18 @@ void SynthConjecture::printSynthSolutionInternal(std::ostream& out)
             if (options::sygusFilterSolMode()
                 == options::SygusFilterSolMode::STRONG)
             {
-              d_exprm[prog].enableFilterStrongSolutions();
+              emm->enableFilterStrongSolutions();
             }
             else if (options::sygusFilterSolMode()
                      == options::SygusFilterSolMode::WEAK)
             {
-              d_exprm[prog].enableFilterWeakSolutions();
+              emm->enableFilterWeakSolutions();
             }
           }
           its = d_exprm.find(prog);
         }
         bool rew_print = false;
-        is_unique_term = d_exprm[prog].addTerm(sol, out, rew_print);
+        is_unique_term = its->second->addTerm(sol, out, rew_print);
         if (rew_print)
         {
           ++(d_stats.d_candidate_rewrites_print);
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h
index c1635c05c..9cc488fd2 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.h
+++ b/src/theory/quantifiers/sygus/synth_conjecture.h
@@ -363,7 +363,7 @@ class SynthConjecture
    * This is used for the sygusRewSynth() option to synthesize new candidate
    * rewrite rules.
    */
-  std::map<Node, ExpressionMinerManager> d_exprm;
+  std::map<Node, std::unique_ptr<ExpressionMinerManager>> d_exprm;
 };
 
 }  // namespace quantifiers
diff --git a/src/theory/quantifiers/sygus/synth_verify.cpp b/src/theory/quantifiers/sygus/synth_verify.cpp
index 2d7255415..23ee0e648 100644
--- a/src/theory/quantifiers/sygus/synth_verify.cpp
+++ b/src/theory/quantifiers/sygus/synth_verify.cpp
@@ -19,7 +19,6 @@
 #include "options/arith_options.h"
 #include "options/base_options.h"
 #include "options/quantifiers_options.h"
-#include "smt/smt_engine_scope.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
@@ -33,12 +32,11 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
-SynthVerify::SynthVerify(TermDbSygus* tds) : d_tds(tds)
+SynthVerify::SynthVerify(const Options& opts, TermDbSygus* tds) : d_tds(tds)
 {
   // determine the options to use for the verification subsolvers we spawn
-  // we start with the options of the current SmtEngine
-  SmtEngine* smtCurr = smt::currentSmtEngine();
-  d_subOptions.copyValues(smtCurr->getOptions());
+  // we start with the provided options
+  d_subOptions.copyValues(opts);
   // limit the number of instantiation rounds on subcalls
   d_subOptions.quantifiers.instMaxRounds =
       d_subOptions.quantifiers.sygusVerifyInstMaxRounds;
diff --git a/src/theory/quantifiers/sygus/synth_verify.h b/src/theory/quantifiers/sygus/synth_verify.h
index 794908ee5..c4d1052da 100644
--- a/src/theory/quantifiers/sygus/synth_verify.h
+++ b/src/theory/quantifiers/sygus/synth_verify.h
@@ -34,7 +34,7 @@ namespace quantifiers {
 class SynthVerify
 {
  public:
-  SynthVerify(TermDbSygus* tds);
+  SynthVerify(const Options& opts, TermDbSygus* tds);
   ~SynthVerify();
   /**
    * Verification call, which takes into account specific aspects of the
diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp
index c072fd7b4..0cbc4df5b 100644
--- a/src/theory/quantifiers/sygus_sampler.cpp
+++ b/src/theory/quantifiers/sygus_sampler.cpp
@@ -23,8 +23,6 @@
 #include "options/base_options.h"
 #include "options/quantifiers_options.h"
 #include "printer/printer.h"
-#include "smt/smt_engine.h"
-#include "smt/smt_engine_scope.h"
 #include "theory/quantifiers/lazy_trie.h"
 #include "theory/rewriter.h"
 #include "util/bitvector.h"
@@ -780,7 +778,7 @@ void SygusSampler::registerSygusType(TypeNode tn)
   }
 }
 
-void SygusSampler::checkEquivalent(Node bv, Node bvr)
+void SygusSampler::checkEquivalent(Node bv, Node bvr, std::ostream& out)
 {
   if (bv == bvr)
   {
@@ -831,14 +829,12 @@ void SygusSampler::checkEquivalent(Node bv, Node bvr)
       return;
     }
     // we have detected unsoundness in the rewriter
-    Options& sopts = smt::currentSmtEngine()->getOptions();
-    std::ostream* out = sopts.base.out;
-    (*out) << "(unsound-rewrite " << bv << " " << bvr << ")" << std::endl;
+    out << "(unsound-rewrite " << bv << " " << bvr << ")" << std::endl;
     // debugging information
-    (*out) << "Terms are not equivalent for : " << std::endl;
-    (*out) << ptOut.str();
+    out << "Terms are not equivalent for : " << std::endl;
+    out << ptOut.str();
     Assert(bve != bvre);
-    (*out) << "where they evaluate to " << bve << " and " << bvre << std::endl;
+    out << "where they evaluate to " << bve << " and " << bvre << std::endl;
 
     if (options::sygusRewVerifyAbort())
     {
diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h
index c56b1c0b1..85606adc6 100644
--- a/src/theory/quantifiers/sygus_sampler.h
+++ b/src/theory/quantifiers/sygus_sampler.h
@@ -170,8 +170,12 @@ class SygusSampler : public LazyTrieEvaluator
    *
    * Check whether bv and bvr are equivalent on all sample points, print
    * an error if not. Used with --sygus-rr-verify.
+   *
+   * @param bv The original term
+   * @param bvr The rewritten form of bvr
+   * @param out The output stream to write if the rewrite was unsound.
    */
-  void checkEquivalent(Node bv, Node bvr);
+  void checkEquivalent(Node bv, Node bvr, std::ostream& out);
 
  protected:
   /** sygus term database of d_qe */
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index ccd177b7d..213b6c55e 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -21,7 +21,6 @@
 #include "options/smt_options.h"
 #include "options/strings_options.h"
 #include "options/uf_options.h"
-#include "smt/smt_engine_scope.h"
 #include "theory/quantifiers/equality_query.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/fmf/first_order_model_fmc.h"