Remove `TheoryState::getEnv()` (#7163)

diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index 742e5ca49eeaf2c93eb7935082ca578c65a53179..b8170df457e9cd1fe8ca853d7757662680299bc1 100644 (file)
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -49,14 +49,14 @@ NonlinearExtension::NonlinearExtension(Env& env,
       d_extTheoryCb(state.getEqualityEngine()),
       d_extTheory(d_extTheoryCb, context(), userContext(), d_im),
       d_model(),
-      d_trSlv(d_im, d_model, d_astate.getEnv()),
-      d_extState(d_im, d_model, d_astate.getEnv()),
+      d_trSlv(d_im, d_model, d_env),
+      d_extState(d_im, d_model, d_env),
       d_factoringSlv(&d_extState),
       d_monomialBoundsSlv(&d_extState),
       d_monomialSlv(&d_extState),
       d_splitZeroSlv(&d_extState),
       d_tangentPlaneSlv(&d_extState),
-      d_cadSlv(d_astate.getEnv(), d_im, d_model),
+      d_cadSlv(d_env, d_im, d_model),
       d_icpSlv(d_im),
       d_iandSlv(env, d_im, state, d_model),
       d_pow2Slv(env, d_im, state, d_model)
@@ -72,9 +72,9 @@ NonlinearExtension::NonlinearExtension(Env& env,
   d_one = NodeManager::currentNM()->mkConst(Rational(1));
   d_neg_one = NodeManager::currentNM()->mkConst(Rational(-1));
 
-  if (d_astate.getEnv().isTheoryProofProducing())
+  if (d_env.isTheoryProofProducing())
   {
-    ProofChecker* pc = d_astate.getEnv().getProofNodeManager()->getChecker();
+    ProofChecker* pc = d_env.getProofNodeManager()->getChecker();
     d_proofChecker.registerTo(pc);
   }
 }

diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index 81366fabd2e1ebf1c305c705d415ffc2d8bd90ae..8334cc24832216de006bb6004a5dfcc8404aff9e 100644 (file)
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -47,11 +47,12 @@ TrustNode InstRewriterCegqi::rewriteInstantiation(Node q,
   return d_parent->rewriteInstantiation(q, terms, inst, doVts);
 }
 
-InstStrategyCegqi::InstStrategyCegqi(QuantifiersState& qs,
+InstStrategyCegqi::InstStrategyCegqi(Env& env,
+                                     QuantifiersState& qs,
                                      QuantifiersInferenceManager& qim,
                                      QuantifiersRegistry& qr,
                                      TermRegistry& tr)
-    : QuantifiersModule(qs, qim, qr, tr),
+    : QuantifiersModule(env, qs, qim, qr, tr),
       d_irew(new InstRewriterCegqi(this)),
       d_cbqi_set_quant_inactive(false),
       d_incomplete_check(false),
@@ -70,7 +71,7 @@ InstStrategyCegqi::InstStrategyCegqi(QuantifiersState& qs,
   }
   if (options::cegqiNestedQE())
   {
-    d_nestedQe.reset(new NestedQe(qs.getEnv()));
+    d_nestedQe.reset(new NestedQe(d_env));
   }
 }
 

diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
index 882f69b855df1e190682374266668c819708976a..a568b0b4d7c1cb79c8a484561c25f67df2c590c7 100644 (file)
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
@@ -18,6 +18,7 @@
 #ifndef CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_CEGQI_H
 #define CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_CEGQI_H
 
+#include "smt/env_obj.h"
 #include "theory/decision_manager.h"
 #include "theory/quantifiers/bv_inverter.h"
 #include "theory/quantifiers/cegqi/ceg_instantiator.h"
@@ -69,7 +70,8 @@ class InstStrategyCegqi : public QuantifiersModule
   typedef context::CDHashMap<Node, int> NodeIntMap;
 
  public:
-  InstStrategyCegqi(QuantifiersState& qs,
+  InstStrategyCegqi(Env& env,
+                    QuantifiersState& qs,
                     QuantifiersInferenceManager& qim,
                     QuantifiersRegistry& qr,
                     TermRegistry& tr);

diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index 17eaad5c648b04ec40b1c8e66eee9fad94c133e1..f9625d7ac4bd0480eb48c32be787f1e73c20687a 100644 (file)
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -86,15 +86,15 @@ void OpArgIndex::getGroundTerms( ConjectureGenerator * s, std::vector< TNode >&
   }
 }
 
-ConjectureGenerator::ConjectureGenerator(QuantifiersState& qs,
+ConjectureGenerator::ConjectureGenerator(Env& env,
+                                         QuantifiersState& qs,
                                          QuantifiersInferenceManager& qim,
                                          QuantifiersRegistry& qr,
                                          TermRegistry& tr)
-    : QuantifiersModule(qs, qim, qr, tr),
+    : QuantifiersModule(env, qs, qim, qr, tr),
       d_notify(*this),
-      d_uequalityEngine(
-          d_notify, qs.getSatContext(), "ConjectureGenerator::ee", false),
-      d_ee_conjectures(qs.getSatContext()),
+      d_uequalityEngine(d_notify, context(), "ConjectureGenerator::ee", false),
+      d_ee_conjectures(context()),
       d_conj_count(0),
       d_subs_confirmCount(0),
       d_subs_unkCount(0),

diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h
index ef60792a69166be0a2ca0aca86038b13cf9e43af..bc5f3fb131a57186619f7667a899195dfdcc61c7 100644 (file)
--- a/src/theory/quantifiers/conjecture_generator.h
+++ b/src/theory/quantifiers/conjecture_generator.h
@@ -21,6 +21,7 @@
 #include "context/cdhashmap.h"
 #include "expr/node_trie.h"
 #include "expr/term_canonize.h"
+#include "smt/env_obj.h"
 #include "theory/quantifiers/quant_module.h"
 #include "theory/type_enumerator.h"
 
@@ -437,7 +438,8 @@ private:  //information about ground equivalence classes
   unsigned flushWaitingConjectures( unsigned& addedLemmas, int ldepth, int rdepth );
 
  public:
-  ConjectureGenerator(QuantifiersState& qs,
+  ConjectureGenerator(Env& env,
+                      QuantifiersState& qs,
                       QuantifiersInferenceManager& qim,
                       QuantifiersRegistry& qr,
                       TermRegistry& tr);

diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp
index dcfa71f8c81c1bbfd85e279a0828c09e1b755625..62c5c2440efc741ed88a0acc0aff792278d769b5 100644 (file)
--- a/src/theory/quantifiers/ematching/instantiation_engine.cpp
+++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp
@@ -37,7 +37,7 @@ InstantiationEngine::InstantiationEngine(Env& env,
                                          QuantifiersInferenceManager& qim,
                                          QuantifiersRegistry& qr,
                                          TermRegistry& tr)
-    : QuantifiersModule(qs, qim, qr, tr),
+    : QuantifiersModule(env, qs, qim, qr, tr),
       d_instStrategies(),
       d_isup(),
       d_i_ag(),

diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index 3fd478c31f55734b60ef4a84eb1981880c79cd30..b04391db3e26936b5cac650af9957aef222a3cf4 100644 (file)
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -88,11 +88,12 @@ Node BoundedIntegers::IntRangeDecisionHeuristic::proxyCurrentRangeLemma()
   return lem;
 }
 
-BoundedIntegers::BoundedIntegers(QuantifiersState& qs,
+BoundedIntegers::BoundedIntegers(Env& env,
+                                 QuantifiersState& qs,
                                  QuantifiersInferenceManager& qim,
                                  QuantifiersRegistry& qr,
                                  TermRegistry& tr)
-    : QuantifiersModule(qs, qim, qr, tr)
+    : QuantifiersModule(env, qs, qim, qr, tr)
 {
 }
 

diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h
index d37e71b72d09246a09f798c10944b5a9ae8a72fe..8c468c1de8043e1dbbc59a61118daaea402b274c 100644 (file)
--- a/src/theory/quantifiers/fmf/bounded_integers.h
+++ b/src/theory/quantifiers/fmf/bounded_integers.h
@@ -18,13 +18,13 @@
 #ifndef CVC5__BOUNDED_INTEGERS_H
 #define CVC5__BOUNDED_INTEGERS_H
 
-#include "theory/quantifiers/quant_module.h"
-
 #include "context/cdhashmap.h"
 #include "context/context.h"
 #include "expr/attribute.h"
+#include "smt/env_obj.h"
 #include "theory/decision_strategy.h"
 #include "theory/quantifiers/quant_bound_inference.h"
+#include "theory/quantifiers/quant_module.h"
 
 namespace cvc5 {
 namespace theory {
@@ -164,7 +164,8 @@ private:
   std::map< Node, std::map< Node, BoundInstTrie > > d_bnd_it;
 
  public:
-  BoundedIntegers(QuantifiersState& qs,
+  BoundedIntegers(Env& env,
+                  QuantifiersState& qs,
                   QuantifiersInferenceManager& qim,
                   QuantifiersRegistry& qr,
                   TermRegistry& tr);

diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp
index e58f66d0b368f10548da2a2a142b1561f9224d57..25689958004479c7a75fa5272b2b0b5740d163a0 100644 (file)
--- a/src/theory/quantifiers/fmf/model_engine.cpp
+++ b/src/theory/quantifiers/fmf/model_engine.cpp
@@ -31,12 +31,13 @@ namespace theory {
 namespace quantifiers {
 
 //Model Engine constructor
-ModelEngine::ModelEngine(QuantifiersState& qs,
+ModelEngine::ModelEngine(Env& env,
+                         QuantifiersState& qs,
                          QuantifiersInferenceManager& qim,
                          QuantifiersRegistry& qr,
                          TermRegistry& tr,
                          QModelBuilder* builder)
-    : QuantifiersModule(qs, qim, qr, tr),
+    : QuantifiersModule(env, qs, qim, qr, tr),
       d_incomplete_check(true),
       d_addedLemmas(0),
       d_triedLemmas(0),

diff --git a/src/theory/quantifiers/fmf/model_engine.h b/src/theory/quantifiers/fmf/model_engine.h
index f818a63621a06c40676de03d6d5235c169e51304..b5ab86f207b0c0eabe280ed59dd84b558df75b46 100644 (file)
--- a/src/theory/quantifiers/fmf/model_engine.h
+++ b/src/theory/quantifiers/fmf/model_engine.h
@@ -18,6 +18,7 @@
 #ifndef CVC5__THEORY__QUANTIFIERS__MODEL_ENGINE_H
 #define CVC5__THEORY__QUANTIFIERS__MODEL_ENGINE_H
 
+#include "smt/env_obj.h"
 #include "theory/quantifiers/fmf/model_builder.h"
 #include "theory/quantifiers/quant_module.h"
 #include "theory/theory_model.h"
@@ -42,7 +43,8 @@ private:
   int d_triedLemmas;
   int d_totalLemmas;
 public:
- ModelEngine(QuantifiersState& qs,
+ ModelEngine(Env& env,
+             QuantifiersState& qs,
              QuantifiersInferenceManager& qim,
              QuantifiersRegistry& qr,
              TermRegistry& tr,

diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp
index aeff27433264c297584ce0de332422d6ff812606..6769d8bc2a1d7f608611505c0397a625d17c1d4b 100644 (file)
--- a/src/theory/quantifiers/inst_strategy_enumerative.cpp
+++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp
@@ -29,12 +29,13 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
-InstStrategyEnum::InstStrategyEnum(QuantifiersState& qs,
+InstStrategyEnum::InstStrategyEnum(Env& env,
+                                   QuantifiersState& qs,
                                    QuantifiersInferenceManager& qim,
                                    QuantifiersRegistry& qr,
                                    TermRegistry& tr,
                                    RelevantDomain* rd)
-    : QuantifiersModule(qs, qim, qr, tr), d_rd(rd), d_fullSaturateLimit(-1)
+    : QuantifiersModule(env, qs, qim, qr, tr), d_rd(rd), d_fullSaturateLimit(-1)
 {
 }
 void InstStrategyEnum::presolve()

diff --git a/src/theory/quantifiers/inst_strategy_enumerative.h b/src/theory/quantifiers/inst_strategy_enumerative.h
index a298e3a8a6a878f1c696c8c2b7735fee687660f0..66315c07005b38fcc2252af55c8ed86aab0460ba 100644 (file)
--- a/src/theory/quantifiers/inst_strategy_enumerative.h
+++ b/src/theory/quantifiers/inst_strategy_enumerative.h
@@ -18,6 +18,7 @@
 #ifndef CVC5__INST_STRATEGY_ENUMERATIVE_H
 #define CVC5__INST_STRATEGY_ENUMERATIVE_H
 
+#include "smt/env_obj.h"
 #include "theory/quantifiers/quant_module.h"
 
 namespace cvc5 {
@@ -62,7 +63,8 @@ class RelevantDomain;
 class InstStrategyEnum : public QuantifiersModule
 {
  public:
-  InstStrategyEnum(QuantifiersState& qs,
+  InstStrategyEnum(Env& env,
+                   QuantifiersState& qs,
                    QuantifiersInferenceManager& qim,
                    QuantifiersRegistry& qr,
                    TermRegistry& tr,

diff --git a/src/theory/quantifiers/inst_strategy_pool.cpp b/src/theory/quantifiers/inst_strategy_pool.cpp
index 0e32c246eb5e509c010c16df929ee8e307df4963..cadda033b7372fae48c2f8b99fdb07cf6b230cbd 100644 (file)
--- a/src/theory/quantifiers/inst_strategy_pool.cpp
+++ b/src/theory/quantifiers/inst_strategy_pool.cpp
@@ -30,11 +30,12 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
-InstStrategyPool::InstStrategyPool(QuantifiersState& qs,
+InstStrategyPool::InstStrategyPool(Env& env,
+                                   QuantifiersState& qs,
                                    QuantifiersInferenceManager& qim,
                                    QuantifiersRegistry& qr,
                                    TermRegistry& tr)
-    : QuantifiersModule(qs, qim, qr, tr)
+    : QuantifiersModule(env, qs, qim, qr, tr)
 {
 }
 

diff --git a/src/theory/quantifiers/inst_strategy_pool.h b/src/theory/quantifiers/inst_strategy_pool.h
index acdc0010b84adfd32a0e81392977161c93db3878..1f79717af1a0578ef209297e7e4a898e5d445118 100644 (file)
--- a/src/theory/quantifiers/inst_strategy_pool.h
+++ b/src/theory/quantifiers/inst_strategy_pool.h
@@ -18,6 +18,7 @@
 #ifndef CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_POOL_H
 #define CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_POOL_H
 
+#include "smt/env_obj.h"
 #include "theory/quantifiers/quant_module.h"
 
 namespace cvc5 {
@@ -38,7 +39,8 @@ namespace quantifiers {
 class InstStrategyPool : public QuantifiersModule
 {
  public:
-  InstStrategyPool(QuantifiersState& qs,
+  InstStrategyPool(Env& env,
+                   QuantifiersState& qs,
                    QuantifiersInferenceManager& qim,
                    QuantifiersRegistry& qr,
                    TermRegistry& tr);

diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 8c4d686311b26537eee0516bbb73cc6ec153a0c8..983eee9ae50b8a4143e955e9aac5cbbc0d07f18b 100644 (file)
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -1853,11 +1853,12 @@ bool MatchGen::isHandled( TNode n ) {
   return true;
 }
 
-QuantConflictFind::QuantConflictFind(QuantifiersState& qs,
+QuantConflictFind::QuantConflictFind(Env& env,
+                                     QuantifiersState& qs,
                                      QuantifiersInferenceManager& qim,
                                      QuantifiersRegistry& qr,
                                      TermRegistry& tr)
-    : QuantifiersModule(qs, qim, qr, tr),
+    : QuantifiersModule(env, qs, qim, qr, tr),
       d_conflict(qs.getSatContext(), false),
       d_true(NodeManager::currentNM()->mkConst<bool>(true)),
       d_false(NodeManager::currentNM()->mkConst<bool>(false)),

diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index de521cd0790241afabe78bf2a30b754ac80cf541..927a74ff25be4ca2acebd70104622054a6d6b06c 100644 (file)
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -238,7 +238,8 @@ private:  //for equivalence classes
   bool areMatchDisequal( TNode n1, TNode n2 );
 
  public:
-  QuantConflictFind(QuantifiersState& qs,
+  QuantConflictFind(Env& env,
+                    QuantifiersState& qs,
                     QuantifiersInferenceManager& qim,
                     QuantifiersRegistry& qr,
                     TermRegistry& tr);

diff --git a/src/theory/quantifiers/quant_module.cpp b/src/theory/quantifiers/quant_module.cpp
index d5488f0c983746b3f48bbe7be8c091cc544a82a4..8fb37c54826f3cf7eb5107215ffc35a44adfd531 100644 (file)
--- a/src/theory/quantifiers/quant_module.cpp
+++ b/src/theory/quantifiers/quant_module.cpp
@@ -21,11 +21,12 @@ namespace cvc5 {
 namespace theory {
 
 QuantifiersModule::QuantifiersModule(
+    Env& env,
     quantifiers::QuantifiersState& qs,
     quantifiers::QuantifiersInferenceManager& qim,
     quantifiers::QuantifiersRegistry& qr,
     quantifiers::TermRegistry& tr)
-    : EnvObj(qs.getEnv()), d_qstate(qs), d_qim(qim), d_qreg(qr), d_treg(tr)
+    : EnvObj(env), d_qstate(qs), d_qim(qim), d_qreg(qr), d_treg(tr)
 {
 }
 

diff --git a/src/theory/quantifiers/quant_module.h b/src/theory/quantifiers/quant_module.h
index 7358aa55549ed20e46e3229e932cfad1b92b6acb..639f9c2b41bf20a0da35091cd43335f118c1bd9a 100644 (file)
--- a/src/theory/quantifiers/quant_module.h
+++ b/src/theory/quantifiers/quant_module.h
@@ -60,7 +60,8 @@ class QuantifiersModule : protected EnvObj
   };
 
  public:
-  QuantifiersModule(quantifiers::QuantifiersState& qs,
+  QuantifiersModule(Env& env,
+                    quantifiers::QuantifiersState& qs,
                     quantifiers::QuantifiersInferenceManager& qim,
                     quantifiers::QuantifiersRegistry& qr,
                     quantifiers::TermRegistry& tr);

diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp
index 941b94d234cf451e409ca8b2f7083c2b33fb654b..905424107886f901d73617d4b5232e232782b905 100644 (file)
--- a/src/theory/quantifiers/quant_split.cpp
+++ b/src/theory/quantifiers/quant_split.cpp
@@ -28,11 +28,13 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
-QuantDSplit::QuantDSplit(QuantifiersState& qs,
+QuantDSplit::QuantDSplit(Env& env,
+                         QuantifiersState& qs,
                          QuantifiersInferenceManager& qim,
                          QuantifiersRegistry& qr,
                          TermRegistry& tr)
-    : QuantifiersModule(qs, qim, qr, tr), d_added_split(qs.getUserContext())
+    : QuantifiersModule(env, qs, qim, qr, tr),
+      d_added_split(qs.getUserContext())
 {
 }
 

diff --git a/src/theory/quantifiers/quant_split.h b/src/theory/quantifiers/quant_split.h
index 18aeec773138a07c7ce44408d41e0bebf7f55880..84cc6fea79a6e5699fa005a8aaeac297faee66ba 100644 (file)
--- a/src/theory/quantifiers/quant_split.h
+++ b/src/theory/quantifiers/quant_split.h
@@ -19,6 +19,7 @@
 #define CVC5__THEORY__QUANT_SPLIT_H
 
 #include "context/cdo.h"
+#include "smt/env_obj.h"
 #include "theory/quantifiers/quant_module.h"
 
 namespace cvc5 {
@@ -50,7 +51,8 @@ class QuantDSplit : public QuantifiersModule {
   typedef context::CDHashSet<Node> NodeSet;
 
  public:
-  QuantDSplit(QuantifiersState& qs,
+  QuantDSplit(Env& env,
+              QuantifiersState& qs,
               QuantifiersInferenceManager& qim,
               QuantifiersRegistry& qr,
               TermRegistry& tr);

diff --git a/src/theory/quantifiers/quantifiers_modules.cpp b/src/theory/quantifiers/quantifiers_modules.cpp
index 889b6ac26b21925d032657e8937b70d08b3b75ed..563951189a91510082566c96d57a6c862262aa07 100644 (file)
--- a/src/theory/quantifiers/quantifiers_modules.cpp
+++ b/src/theory/quantifiers/quantifiers_modules.cpp
@@ -52,12 +52,12 @@ void QuantifiersModules::initialize(Env& env,
   // add quantifiers modules
   if (options::quantConflictFind())
   {
-    d_qcf.reset(new QuantConflictFind(qs, qim, qr, tr));
+    d_qcf.reset(new QuantConflictFind(env, qs, qim, qr, tr));
     modules.push_back(d_qcf.get());
   }
   if (options::conjectureGen())
   {
-    d_sg_gen.reset(new ConjectureGenerator(qs, qim, qr, tr));
+    d_sg_gen.reset(new ConjectureGenerator(env, qs, qim, qr, tr));
     modules.push_back(d_sg_gen.get());
   }
   if (!options::finiteModelFind() || options::fmfInstEngine())
@@ -67,7 +67,7 @@ void QuantifiersModules::initialize(Env& env,
   }
   if (options::cegqi())
   {
-    d_i_cbqi.reset(new InstStrategyCegqi(qs, qim, qr, tr));
+    d_i_cbqi.reset(new InstStrategyCegqi(env, qs, qim, qr, tr));
     modules.push_back(d_i_cbqi.get());
     qim.getInstantiate()->addRewriter(d_i_cbqi->getInstRewriter());
   }
@@ -80,18 +80,18 @@ void QuantifiersModules::initialize(Env& env,
   // fmfBound, or if strings are enabled.
   if (options::fmfBound() || options::stringExp())
   {
-    d_bint.reset(new BoundedIntegers(qs, qim, qr, tr));
+    d_bint.reset(new BoundedIntegers(env, qs, qim, qr, tr));
     modules.push_back(d_bint.get());
   }
 
   if (options::finiteModelFind() || options::fmfBound() || options::stringExp())
   {
-    d_model_engine.reset(new ModelEngine(qs, qim, qr, tr, builder));
+    d_model_engine.reset(new ModelEngine(env, qs, qim, qr, tr, builder));
     modules.push_back(d_model_engine.get());
   }
   if (options::quantDynamicSplit() != options::QuantDSplitMode::NONE)
   {
-    d_qsplit.reset(new QuantDSplit(qs, qim, qr, tr));
+    d_qsplit.reset(new QuantDSplit(env, qs, qim, qr, tr));
     modules.push_back(d_qsplit.get());
   }
   if (options::quantAlphaEquiv())
@@ -102,17 +102,17 @@ void QuantifiersModules::initialize(Env& env,
   if (options::fullSaturateQuant() || options::fullSaturateInterleave())
   {
     d_rel_dom.reset(new RelevantDomain(env, qs, qr, tr));
-    d_fs.reset(new InstStrategyEnum(qs, qim, qr, tr, d_rel_dom.get()));
+    d_fs.reset(new InstStrategyEnum(env, qs, qim, qr, tr, d_rel_dom.get()));
     modules.push_back(d_fs.get());
   }
   if (options::poolInst())
   {
-    d_ipool.reset(new InstStrategyPool(qs, qim, qr, tr));
+    d_ipool.reset(new InstStrategyPool(env, qs, qim, qr, tr));
     modules.push_back(d_ipool.get());
   }
   if (options::sygusInst())
   {
-    d_sygus_inst.reset(new SygusInst(qs, qim, qr, tr));
+    d_sygus_inst.reset(new SygusInst(env, qs, qim, qr, tr));
     modules.push_back(d_sygus_inst.get());
   }
 }

diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index 708bffe806f6eb8d5a5e643e599cdc859aa639c1..f5774c76196f629d77bc618731ba0a1fb7ac5605 100644 (file)
--- a/src/theory/quantifiers/sygus/cegis.cpp
+++ b/src/theory/quantifiers/sygus/cegis.cpp
@@ -32,11 +32,12 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
-Cegis::Cegis(QuantifiersState& qs,
+Cegis::Cegis(Env& env,
+             QuantifiersState& qs,
              QuantifiersInferenceManager& qim,
              TermDbSygus* tds,
              SynthConjecture* p)
-    : SygusModule(qs, qim, tds, p),
+    : SygusModule(env, qs, qim, tds, p),
       d_eval_unfold(tds->getEvalUnfold()),
       d_usingSymCons(false)
 {

diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h
index d6678a305de2d655d855b771c3b1bf92c0457fb4..d728059509036b6db698dbe0a94923e1fff1698d 100644 (file)
--- a/src/theory/quantifiers/sygus/cegis.h
+++ b/src/theory/quantifiers/sygus/cegis.h
@@ -19,6 +19,8 @@
 #define CVC5__THEORY__QUANTIFIERS__CEGIS_H
 
 #include <map>
+
+#include "smt/env_obj.h"
 #include "theory/quantifiers/sygus/sygus_module.h"
 #include "theory/quantifiers/sygus_sampler.h"
 
@@ -42,7 +44,8 @@ namespace quantifiers {
 class Cegis : public SygusModule
 {
  public:
-  Cegis(QuantifiersState& qs,
+  Cegis(Env& env,
+        QuantifiersState& qs,
         QuantifiersInferenceManager& qim,
         TermDbSygus* tds,
         SynthConjecture* p);

diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
index 9a9d8f02d5f808bad148054bb2953ec0c2d49261..a4232322790cf379376fb0bbaf5a7c65bbdc75ab 100644 (file)
--- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp
+++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
@@ -68,11 +68,12 @@ bool VariadicTrie::hasSubset(const std::vector<Node>& is) const
   return false;
 }
 
-CegisCoreConnective::CegisCoreConnective(QuantifiersState& qs,
+CegisCoreConnective::CegisCoreConnective(Env& env,
+                                         QuantifiersState& qs,
                                          QuantifiersInferenceManager& qim,
                                          TermDbSygus* tds,
                                          SynthConjecture* p)
-    : Cegis(qs, qim, tds, p)
+    : Cegis(env, qs, qim, tds, p)
 {
   d_true = NodeManager::currentNM()->mkConst(true);
   d_false = NodeManager::currentNM()->mkConst(false);
@@ -629,9 +630,7 @@ bool CegisCoreConnective::getUnsatCore(
 Result CegisCoreConnective::checkSat(Node n, std::vector<Node>& mvs) const
 {
   Trace("sygus-ccore-debug") << "...check-sat " << n << "..." << std::endl;
-  Env& env = d_qstate.getEnv();
-  Result r =
-      checkWithSubsolver(n, d_vars, mvs, env.getOptions(), env.getLogicInfo());
+  Result r = checkWithSubsolver(n, d_vars, mvs, options(), logicInfo());
   Trace("sygus-ccore-debug") << "...got " << r << std::endl;
   return r;
 }
@@ -739,7 +738,7 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck,
     addSuccess = false;
     // try a new core
     std::unique_ptr<SmtEngine> checkSol;
-    initializeSubsolver(checkSol, d_qstate.getEnv());
+    initializeSubsolver(checkSol, d_env);
     Trace("sygus-ccore") << "----- Check candidate " << an << std::endl;
     std::vector<Node> rasserts = asserts;
     rasserts.push_back(d_sc);
@@ -779,7 +778,7 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck,
           // In terms of Variant #2, this is the check "if S ^ U is unsat"
           Trace("sygus-ccore") << "----- Check side condition" << std::endl;
           std::unique_ptr<SmtEngine> checkSc;
-          initializeSubsolver(checkSc, d_qstate.getEnv());
+          initializeSubsolver(checkSc, d_env);
           std::vector<Node> scasserts;
           scasserts.insert(scasserts.end(), uasserts.begin(), uasserts.end());
           scasserts.push_back(d_sc);

diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.h b/src/theory/quantifiers/sygus/cegis_core_connective.h
index e9a73e9bb56d4d7958dd16f11d51bb752da5dca8..80ba6f26e14b0436d986993268119380ebee8d1e 100644 (file)
--- a/src/theory/quantifiers/sygus/cegis_core_connective.h
+++ b/src/theory/quantifiers/sygus/cegis_core_connective.h
@@ -22,6 +22,7 @@
 
 #include "expr/node.h"
 #include "expr/node_trie.h"
+#include "smt/env_obj.h"
 #include "theory/evaluator.h"
 #include "theory/quantifiers/sygus/cegis.h"
 #include "util/result.h"
@@ -160,7 +161,8 @@ class VariadicTrie
 class CegisCoreConnective : public Cegis
 {
  public:
-  CegisCoreConnective(QuantifiersState& qs,
+  CegisCoreConnective(Env& env,
+                      QuantifiersState& qs,
                       QuantifiersInferenceManager& qim,
                       TermDbSygus* tds,
                       SynthConjecture* p);

diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index 797aecdab34359aec1e06f8f698c8079a883bbe5..871a85fbd591b1c8508b162a9360cd6d26cae7c1 100644 (file)
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -30,13 +30,14 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
-CegisUnif::CegisUnif(QuantifiersState& qs,
+CegisUnif::CegisUnif(Env& env,
+                     QuantifiersState& qs,
                      QuantifiersInferenceManager& qim,
                      TermDbSygus* tds,
                      SynthConjecture* p)
-    : Cegis(qs, qim, tds, p),
-      d_sygus_unif(qs.getEnv(), p),
-      d_u_enum_manager(qs, qim, tds, p)
+    : Cegis(env, qs, qim, tds, p),
+      d_sygus_unif(env, p),
+      d_u_enum_manager(env, qs, qim, tds, p)
 {
 }
 
@@ -403,6 +404,7 @@ void CegisUnif::registerRefinementLemma(const std::vector<Node>& vars, Node lem)
 }
 
 CegisUnifEnumDecisionStrategy::CegisUnifEnumDecisionStrategy(
+    Env& env,
     QuantifiersState& qs,
     QuantifiersInferenceManager& qim,
     TermDbSygus* tds,

diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h
index 0cddff9c129ab1892ad7c38542ea87e3e7273a27..da47aabbe2084a7c810f843efcd4e63c951467bc 100644 (file)
--- a/src/theory/quantifiers/sygus/cegis_unif.h
+++ b/src/theory/quantifiers/sygus/cegis_unif.h
@@ -20,6 +20,7 @@
 #include <map>
 #include <vector>
 
+#include "smt/env_obj.h"
 #include "theory/decision_strategy.h"
 #include "theory/quantifiers/sygus/cegis.h"
 #include "theory/quantifiers/sygus/sygus_unif_rl.h"
@@ -49,7 +50,8 @@ namespace quantifiers {
 class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf
 {
  public:
-  CegisUnifEnumDecisionStrategy(QuantifiersState& qs,
+  CegisUnifEnumDecisionStrategy(Env& env,
+                                QuantifiersState& qs,
                                 QuantifiersInferenceManager& qim,
                                 TermDbSygus* tds,
                                 SynthConjecture* parent);
@@ -207,7 +209,8 @@ class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf
 class CegisUnif : public Cegis
 {
  public:
-  CegisUnif(QuantifiersState& qs,
+  CegisUnif(Env& env,
+            QuantifiersState& qs,
             QuantifiersInferenceManager& qim,
             TermDbSygus* tds,
             SynthConjecture* p);

diff --git a/src/theory/quantifiers/sygus/sygus_module.cpp b/src/theory/quantifiers/sygus/sygus_module.cpp
index 8272c641807568a1144927aa23de1ff8b5bde15e..1840f0eb129f32236136f56e14c79de3b57117c6 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_module.cpp
+++ b/src/theory/quantifiers/sygus/sygus_module.cpp
@@ -21,11 +21,12 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
-SygusModule::SygusModule(QuantifiersState& qs,
+SygusModule::SygusModule(Env& env,
+                         QuantifiersState& qs,
                          QuantifiersInferenceManager& qim,
                          TermDbSygus* tds,
                          SynthConjecture* p)
-    : EnvObj(qs.getEnv()), d_qstate(qs), d_qim(qim), d_tds(tds), d_parent(p)
+    : EnvObj(env), d_qstate(qs), d_qim(qim), d_tds(tds), d_parent(p)
 {
 }
 

diff --git a/src/theory/quantifiers/sygus/sygus_module.h b/src/theory/quantifiers/sygus/sygus_module.h
index 8070fe009ed6b48c2d0b7a58c5819d8816a0c90c..8ee1fc9b409e86be0ba1fc500acd4e9b4f217fc3 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_module.h
+++ b/src/theory/quantifiers/sygus/sygus_module.h
@@ -53,7 +53,8 @@ class QuantifiersInferenceManager;
 class SygusModule : protected EnvObj
 {
  public:
-  SygusModule(QuantifiersState& qs,
+  SygusModule(Env& env,
+              QuantifiersState& qs,
               QuantifiersInferenceManager& qim,
               TermDbSygus* tds,
               SynthConjecture* p);

diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp
index 52bca15868733750e7f9aa82d1ae0ce8d50a67b2..453ac5c18c41667302379c963666dafc6dcf13d0 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_pbe.cpp
+++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp
@@ -30,11 +30,12 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
-SygusPbe::SygusPbe(QuantifiersState& qs,
+SygusPbe::SygusPbe(Env& env,
+                   QuantifiersState& qs,
                    QuantifiersInferenceManager& qim,
                    TermDbSygus* tds,
                    SynthConjecture* p)
-    : SygusModule(qs, qim, tds, p)
+    : SygusModule(env, qs, qim, tds, p)
 {
   d_true = NodeManager::currentNM()->mkConst(true);
   d_false = NodeManager::currentNM()->mkConst(false);

diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h
index 86776461780cbcfaee803a4a8e56d3d1804f30b1..e55479e18be9e8d2ba19c843de9c1b92cf790d85 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_pbe.h
+++ b/src/theory/quantifiers/sygus/sygus_pbe.h
@@ -18,6 +18,7 @@
 #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_PBE_H
 #define CVC5__THEORY__QUANTIFIERS__SYGUS_PBE_H
 
+#include "smt/env_obj.h"
 #include "theory/quantifiers/sygus/sygus_module.h"
 
 namespace cvc5 {
@@ -86,7 +87,8 @@ class SynthConjecture;
 class SygusPbe : public SygusModule
 {
  public:
-  SygusPbe(QuantifiersState& qs,
+  SygusPbe(Env& env,
+           QuantifiersState& qs,
            QuantifiersInferenceManager& qim,
            TermDbSygus* tds,
            SynthConjecture* p);

diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 730482073bd8f870c142c0eef173a37653ec3959..da021227ab8ae12c414bc125ca22d1e8ed18c60a 100644 (file)
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -66,10 +66,10 @@ SynthConjecture::SynthConjecture(Env& env,
       d_ceg_gc(new CegGrammarConstructor(d_tds, this)),
       d_sygus_rconst(new SygusRepairConst(env, d_tds)),
       d_exampleInfer(new ExampleInfer(d_tds)),
-      d_ceg_pbe(new SygusPbe(qs, qim, d_tds, this)),
-      d_ceg_cegis(new Cegis(qs, qim, d_tds, this)),
-      d_ceg_cegisUnif(new CegisUnif(qs, qim, d_tds, this)),
-      d_sygus_ccore(new CegisCoreConnective(qs, qim, d_tds, this)),
+      d_ceg_pbe(new SygusPbe(env, qs, qim, d_tds, this)),
+      d_ceg_cegis(new Cegis(env, qs, qim, d_tds, this)),
+      d_ceg_cegisUnif(new CegisUnif(env, qs, qim, d_tds, this)),
+      d_sygus_ccore(new CegisCoreConnective(env, qs, qim, d_tds, this)),
       d_master(nullptr),
       d_set_ce_sk_vars(false),
       d_repair_index(0),

diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp
index 64227793dd378b7d755155c377fc34c90fbfd9ed..454442351a6c4249cb8674ea3efd09350a5a7daa 100644 (file)
--- a/src/theory/quantifiers/sygus/synth_engine.cpp
+++ b/src/theory/quantifiers/sygus/synth_engine.cpp
@@ -31,7 +31,7 @@ SynthEngine::SynthEngine(Env& env,
                          QuantifiersInferenceManager& qim,
                          QuantifiersRegistry& qr,
                          TermRegistry& tr)
-    : QuantifiersModule(qs, qim, qr, tr), d_conj(nullptr), d_sqp(qs.getEnv())
+    : QuantifiersModule(env, qs, qim, qr, tr), d_conj(nullptr), d_sqp(env)
 {
   d_conjs.push_back(std::unique_ptr<SynthConjecture>(
       new SynthConjecture(env, qs, qim, qr, tr, d_statistics)));

diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp
index 21852f25a21ad7f919e008a9bdb071bbcf85d63b..4da273cd9f3c82d77fada08ceaeb6009fea9b20b 100644 (file)
--- a/src/theory/quantifiers/sygus_inst.cpp
+++ b/src/theory/quantifiers/sygus_inst.cpp
@@ -182,14 +182,15 @@ void addSpecialValues(const TypeNode& tn,
 
 }  // namespace
 
-SygusInst::SygusInst(QuantifiersState& qs,
+SygusInst::SygusInst(Env& env,
+                     QuantifiersState& qs,
                      QuantifiersInferenceManager& qim,
                      QuantifiersRegistry& qr,
                      TermRegistry& tr)
-    : QuantifiersModule(qs, qim, qr, tr),
-      d_ce_lemma_added(qs.getUserContext()),
-      d_global_terms(qs.getUserContext()),
-      d_notified_assertions(qs.getUserContext())
+    : QuantifiersModule(env, qs, qim, qr, tr),
+      d_ce_lemma_added(userContext()),
+      d_global_terms(userContext()),
+      d_notified_assertions(userContext())
 {
 }
 

diff --git a/src/theory/quantifiers/sygus_inst.h b/src/theory/quantifiers/sygus_inst.h
index 80c7e809fc0b5fdf90123a48795e72c29eef9955..060ab7226c5f99988748a849c2a1818e39f614df 100644 (file)
--- a/src/theory/quantifiers/sygus_inst.h
+++ b/src/theory/quantifiers/sygus_inst.h
@@ -22,6 +22,7 @@
 #include <unordered_set>
 
 #include "context/cdhashset.h"
+#include "smt/env_obj.h"
 #include "theory/decision_strategy.h"
 #include "theory/quantifiers/quant_module.h"
 
@@ -64,7 +65,8 @@ namespace quantifiers {
 class SygusInst : public QuantifiersModule
 {
  public:
-  SygusInst(QuantifiersState& qs,
+  SygusInst(Env& env,
+            QuantifiersState& qs,
             QuantifiersInferenceManager& qim,
             QuantifiersRegistry& qr,
             TermRegistry& tr);

diff --git a/src/theory/quantifiers/term_registry.cpp b/src/theory/quantifiers/term_registry.cpp
index 7ad782fda0a01e4ba9800fe59bcf044a3979c894..98618f3f7701819a357ae4b3341d0d4f6efb8704 100644 (file)
--- a/src/theory/quantifiers/term_registry.cpp
+++ b/src/theory/quantifiers/term_registry.cpp
@@ -32,13 +32,13 @@ namespace quantifiers {
 TermRegistry::TermRegistry(Env& env,
                            QuantifiersState& qs,
                            QuantifiersRegistry& qr)
-    : d_presolve(qs.getUserContext(), true),
+    : EnvObj(env),
+      d_presolve(qs.getUserContext(), true),
       d_presolveCache(qs.getUserContext()),
       d_termEnum(new TermEnumeration),
       d_termPools(new TermPools(env, qs)),
-      d_termDb(qs.getEnv().getLogicInfo().isHigherOrder()
-                   ? new HoTermDb(env, qs, qr)
-                   : new TermDb(env, qs, qr)),
+      d_termDb(logicInfo().isHigherOrder() ? new HoTermDb(env, qs, qr)
+                                           : new TermDb(env, qs, qr)),
       d_sygusTdb(nullptr),
       d_qmodel(nullptr)
 {

diff --git a/src/theory/quantifiers/term_registry.h b/src/theory/quantifiers/term_registry.h
index e0ce732868aef6980d14d1c37f67a0626a1a3a12..175d450dfd9fcb691e0a7666a29f825a4527141e 100644 (file)
--- a/src/theory/quantifiers/term_registry.h
+++ b/src/theory/quantifiers/term_registry.h
@@ -22,6 +22,7 @@
 #include <unordered_set>
 
 #include "context/cdhashset.h"
+#include "smt/env_obj.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_enumeration.h"
@@ -37,7 +38,7 @@ class FirstOrderModel;
  * Term Registry, which manages notifying modules within quantifiers about
  * (ground) terms that exist in the current context.
  */
-class TermRegistry
+class TermRegistry : protected EnvObj
 {
   using NodeSet = context::CDHashSet<Node>;
 

diff --git a/src/theory/theory_state.h b/src/theory/theory_state.h
index 049123b8d2d28c0e54f1c7d131a1bfdfa7bc1ebf..574aa935510403bcc9c13b84d8925cdfb5da1668 100644 (file)
--- a/src/theory/theory_state.h
+++ b/src/theory/theory_state.h
@@ -46,8 +46,6 @@ class TheoryState : protected EnvObj
   context::Context* getSatContext() const;
   /** Get the user context */
   context::UserContext* getUserContext() const;
-  /** Get the environment */
-  Env& getEnv() const { return d_env; }
   //-------------------------------------- equality information
   /** Is t registered as a term in the equality engine of this class? */
   virtual bool hasTerm(TNode a) const;