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 53f3feffc8237cd87250ffed86d8828d41531620..3f6828a7b31a63308997202787590cc040da816f 100644 (file)
--- 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 63af575921ada6cf1ca4063bee6fa5d97c83482a..e66b709345aef87b3f053e4eaa7eef709e18be5f 100644 (file)
--- 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 c2ee563e3f2e3f9c283c1de09d34b2ea6c7ed815..0fd0eebd68c60a039be9fcc2a9872b48b9b5c335 100644 (file)
--- 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 309aaf4b7f88e5ed2bd2b1c3f703b0476f1eb630..71ae5649f9adcaed8fd81a6f174e596406862612 100644 (file)
--- 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 0f46fa7908ae368236135babc7b1bd1344a7e521..fa156c839006c9648d107bd2864a65ce2b22e837 100644 (file)
--- 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 79d0c6650f486ebce39acd8e892a347aefe7f973..8a5ce1c1f9af9a6b05e706b4335c528e666fe529 100644 (file)
--- 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 24ab7c30ab8bc2706e28fa90bc27db22fcd70253..92b7c105d2d94fb3d4a180690a12c352c9e857d5 100644 (file)
--- 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 32bc4744f331f7efefc5d4195cf6be742135f4b6..b38de1337b943c7a6689a1a8b19fd3da3ae4c05d 100644 (file)
--- 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 05361eaa11a3dd2ad71a0f871e75029e89f6d0c0..be1633d16be4aa25e8472b21b512aff77b197db3 100644 (file)
--- 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 3c3dd8d8479e4e247797bd012422fb2131713cf2..31d8c3c22c14737316df9c2642e9fd36a9d606d5 100644 (file)
--- 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 90b30a0168f47747fb9ea9be72366b8ad4b64db5..7738a4fe58c54f5ad3445231a7c3b0245a5aa851 100644 (file)
--- 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 ccc0763b7daffdf6098290778dc7bcaf55b1ee0c..8844950c78b6f77a769dd1bd72998dd68c0cb6b6 100644 (file)
--- 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 43545d6d9afd559d02d725c53890d1bea1d0fea6..e3da8c98663879d02791fe393e7060d0609061b3 100644 (file)
--- 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 99a5126aaf9b1d4b61163d786e68d552c5a83a31..f1caca1c433ff1f1d6d99f9a884e17c507c84f5f 100644 (file)
--- 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 72d41592a4cc969f6985dd1f7d5b5a5c4907e9ed..13757dba99f9ce285a332215b556fca08a6768d1 100644 (file)
--- 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 4bcede905a00f5900fb993f00cc8138ea685591a..165326db72358b0955863353acd76d25ab3b46b1 100644 (file)
--- 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 fd92e4d23d609f37ba80a07dbd9b59974080262e..8a2d70bfa4bc286e823b1a4d3c54aa9386b50f66 100644 (file)
--- 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 e610764e085778dfa302172c0ac1351980ab9f73..c786bb6f1872c87d370151c4ff11a8b34f8783fd 100644 (file)
--- 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 a1ae53ad1efe2b452da79106b9471298efc9322c..78f8d303c206805cd7c5def78e3f583ce7ee4421 100644 (file)
--- 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 4c9ae48e0e98a197b2e413e466852b1a3fbee218..294454fe2f0f6e30ddfc53a55681d625975ac815 100644 (file)
--- 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 7b32368325efbb9bbcad9d969d3daab90022b72e..3b536695ff399baf71383e92214bb820bb673124 100644 (file)
--- 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 46ca68c51616a428404b3ff04c00ff9efa7ae97c..5ed28b3099f7107f94f961f1b4a6b562a82a52d0 100644 (file)
--- 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 d4d1398f42d8f4b9163cdb818122aed95876779a..209d10297a24839eb58fc976de364814f1dacf79 100644 (file)
--- 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 07f5ed4adb388180b7b5494dabb354f1f55a8cfd..e86ac624a95ae3efdeaf4cc132d724ce2ab33751 100644 (file)
--- 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 5da282606032d24625fa8d4dfd4251122226cf35..3073a472d3eb13b71e7478248074a4b50cfa4d92 100644 (file)
--- 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 e86b1688ceaecaa08dec09eb145e4f6dc1183b6d..4102db713d9c892fc57666a7081251d84ed9dd35 100644 (file)
--- 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 739e9ab0dc9a87ee126492298bad270b8c6c6a7f..d4611e6ca27a94e20dce592b8cfcea1486734072 100644 (file)
--- 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 f0452a59c70a4cb3ab9c233d4665ad1f32fe4127..ce6c810119fb5bf8c34f0edf76c73adce0b58b1b 100644 (file)
--- 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 3f7ce158cbed629ce935752716df08bcaf765c64..eeadbdd5432cc8d4f6b8903f9e54fa1e71616e08 100644 (file)
--- 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 c1635c05c3b11142ae6ec5ff1a5eae386785a292..9cc488fd25f55b0f4754c3ccf8a9698350684449 100644 (file)
--- 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 2d7255415ed4f17df4398a8c7dc9c651e6bdfe63..23ee0e648e892ea4e9ef806edbc1a31605f6c9bb 100644 (file)
--- 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 794908ee546ada7e758e47a0f9f495253de31e2f..c4d1052da588bc131dc000a53153d341890e0785 100644 (file)
--- 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 c072fd7b4c9a6ddaf5e115b5a744f22cb0b27561..0cbc4df5b23ea86baa4912bbc3b9c248031b4780 100644 (file)
--- 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 c56b1c0b14d72fa45c1649d8375d2315a33df9a5..85606adc6f9c977bc3af2d31f3dd8263bf056d27 100644 (file)
--- 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 ccd177b7ddc4e7c38d5f2ec2f53de3abef1b2855..213b6c55ee7ec02b130d3d9fcd0f001e23961d77 100644 (file)
--- 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"