Remove `TheoryState::options()` (#7148)

This commit removes TheoryState::options() by changing more classes to
EnvObjs.

diff --git a/src/theory/arith/arith_preprocess.cpp b/src/theory/arith/arith_preprocess.cpp
index 6ab39934870cb9f7496b56a8a92d99720e954511..ba2de9fdf1db3d2950ec980133d613069d31d7a2 100644 (file)
--- a/src/theory/arith/arith_preprocess.cpp
+++ b/src/theory/arith/arith_preprocess.cpp
@@ -23,11 +23,12 @@ namespace cvc5 {
 namespace theory {
 namespace arith {
 
-ArithPreprocess::ArithPreprocess(ArithState& state,
+ArithPreprocess::ArithPreprocess(Env& env,
+                                 ArithState& state,
                                  InferenceManager& im,
                                  ProofNodeManager* pnm,
                                  OperatorElim& oe)
-    : d_im(im), d_opElim(oe), d_reduced(state.getUserContext())
+    : EnvObj(env), d_im(im), d_opElim(oe), d_reduced(userContext())
 {
 }
 TrustNode ArithPreprocess::eliminate(TNode n,

diff --git a/src/theory/arith/arith_preprocess.h b/src/theory/arith/arith_preprocess.h
index a537c33c70ca69b6016405f953c46315fa10c54f..939306a6eb693dc5b6dc3bccc493587af2319fd9 100644 (file)
--- a/src/theory/arith/arith_preprocess.h
+++ b/src/theory/arith/arith_preprocess.h
@@ -19,6 +19,7 @@
 #define CVC5__THEORY__ARITH__ARITH_PREPROCESS_H
 
 #include "context/cdhashmap.h"
+#include "smt/env_obj.h"
 #include "theory/arith/operator_elim.h"
 #include "theory/logic_info.h"
 
@@ -40,10 +41,11 @@ class OperatorElim;
  * extends that utility with the ability to generate lemmas on demand via
  * the provided inference manager.
  */
-class ArithPreprocess
+class ArithPreprocess : protected EnvObj
 {
  public:
-  ArithPreprocess(ArithState& state,
+  ArithPreprocess(Env& env,
+                  ArithState& state,
                   InferenceManager& im,
                   ProofNodeManager* pnm,
                   OperatorElim& oe);

diff --git a/src/theory/arith/branch_and_bound.cpp b/src/theory/arith/branch_and_bound.cpp
index ca1a2fa6fd0d1df10ef55da190683df11ed92b8b..31017dea60d5e7f74cb930890526d2ba7dc60bfd 100644 (file)
--- a/src/theory/arith/branch_and_bound.cpp
+++ b/src/theory/arith/branch_and_bound.cpp
@@ -28,14 +28,16 @@ namespace cvc5 {
 namespace theory {
 namespace arith {
 
-BranchAndBound::BranchAndBound(ArithState& s,
+BranchAndBound::BranchAndBound(Env& env,
+                               ArithState& s,
                                InferenceManager& im,
                                PreprocessRewriteEq& ppre,
                                ProofNodeManager* pnm)
-    : d_astate(s),
+    : EnvObj(env),
+      d_astate(s),
       d_im(im),
       d_ppre(ppre),
-      d_pfGen(new EagerProofGenerator(pnm, s.getUserContext())),
+      d_pfGen(new EagerProofGenerator(pnm, userContext())),
       d_pnm(pnm)
 {
 }
@@ -45,7 +47,7 @@ TrustNode BranchAndBound::branchIntegerVariable(TNode var, Rational value)
   TrustNode lem = TrustNode::null();
   NodeManager* nm = NodeManager::currentNM();
   Integer floor = value.floor();
-  if (d_astate.options().arith.brabTest)
+  if (options().arith.brabTest)
   {
     Trace("integers") << "branch-round-and-bound enabled" << std::endl;
     Integer ceil = value.ceiling();

diff --git a/src/theory/arith/branch_and_bound.h b/src/theory/arith/branch_and_bound.h
index 4281ba6780ff182d7cf9f4e52a6c23284da42f91..52acf6aae57309b9f455badfe95b4e0380b0fb94 100644 (file)
--- a/src/theory/arith/branch_and_bound.h
+++ b/src/theory/arith/branch_and_bound.h
@@ -23,6 +23,7 @@
 #include "expr/node.h"
 #include "proof/proof_node_manager.h"
 #include "proof/trust_node.h"
+#include "smt/env_obj.h"
 #include "theory/arith/arith_state.h"
 #include "theory/arith/inference_manager.h"
 #include "theory/arith/pp_rewrite_eq.h"
@@ -37,10 +38,11 @@ namespace arith {
  * agnostic to the state of solver; instead is simply given (variable, value)
  * pairs in branchIntegerVariable below and constructs the appropriate lemma.
  */
-class BranchAndBound
+class BranchAndBound : protected EnvObj
 {
  public:
-  BranchAndBound(ArithState& s,
+  BranchAndBound(Env& env,
+                 ArithState& s,
                  InferenceManager& im,
                  PreprocessRewriteEq& ppre,
                  ProofNodeManager* pnm);

diff --git a/src/theory/arith/equality_solver.cpp b/src/theory/arith/equality_solver.cpp
index 8b4e1b8dd877ce9d15bc809552b82fd035f28c7b..8e5cc9a289f87cad5c15af2b42bbf302d176706b 100644 (file)
--- a/src/theory/arith/equality_solver.cpp
+++ b/src/theory/arith/equality_solver.cpp
@@ -23,12 +23,15 @@ namespace cvc5 {
 namespace theory {
 namespace arith {
 
-EqualitySolver::EqualitySolver(ArithState& astate, InferenceManager& aim)
-    : d_astate(astate),
+EqualitySolver::EqualitySolver(Env& env,
+                               ArithState& astate,
+                               InferenceManager& aim)
+    : EnvObj(env),
+      d_astate(astate),
       d_aim(aim),
       d_notify(*this),
       d_ee(nullptr),
-      d_propLits(astate.getSatContext())
+      d_propLits(context())
 {
 }
 

diff --git a/src/theory/arith/equality_solver.h b/src/theory/arith/equality_solver.h
index bce30e697fc33eb89cd57a674a776c822ada60cf..8528650f0e0722b44b51a128dd80b992b18d0f52 100644 (file)
--- a/src/theory/arith/equality_solver.h
+++ b/src/theory/arith/equality_solver.h
@@ -21,6 +21,7 @@
 #include "context/cdhashset.h"
 #include "expr/node.h"
 #include "proof/trust_node.h"
+#include "smt/env_obj.h"
 #include "theory/arith/arith_state.h"
 #include "theory/ee_setup_info.h"
 #include "theory/uf/equality_engine.h"
@@ -39,12 +40,12 @@ class InferenceManager;
  * the literals that it propagates and only explains the literals that
  * originated from this class.
  */
-class EqualitySolver
+class EqualitySolver : protected EnvObj
 {
   using NodeSet = context::CDHashSet<Node>;
 
  public:
-  EqualitySolver(ArithState& astate, InferenceManager& aim);
+  EqualitySolver(Env& env, ArithState& astate, InferenceManager& aim);
   ~EqualitySolver() {}
   //--------------------------------- initialization
   /**

diff --git a/src/theory/arith/inference_manager.cpp b/src/theory/arith/inference_manager.cpp
index 5ab606f96456626a490bc8bebe421af5b80ce3d7..0c6b18893279826326656d23769998845402c943 100644 (file)
--- a/src/theory/arith/inference_manager.cpp
+++ b/src/theory/arith/inference_manager.cpp
@@ -30,7 +30,7 @@ InferenceManager::InferenceManager(Env& env,
                                    ProofNodeManager* pnm)
     : InferenceManagerBuffered(env, ta, astate, pnm, "theory::arith::"),
       // currently must track propagated literals if using the equality solver
-      d_trackPropLits(astate.options().arith.arithEqSolver),
+      d_trackPropLits(options().arith.arithEqSolver),
       d_propLits(context())
 {
 }
@@ -128,7 +128,7 @@ bool InferenceManager::cacheLemma(TNode lem, LemmaProperty p)
 
 bool InferenceManager::isEntailedFalse(const SimpleTheoryLemma& lem)
 {
-  if (d_theoryState.options().arith.nlExtEntailConflicts)
+  if (options().arith.nlExtEntailConflicts)
   {
     Node ch_lemma = lem.d_node.negate();
     ch_lemma = Rewriter::rewrite(ch_lemma);

diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp
index eb5620a82fc0106a9055141a1fbdf72fc3feeac4..76d964934ca2e7b86c021c0a490c2159eb2b8935 100644 (file)
--- a/src/theory/arith/nl/iand_solver.cpp
+++ b/src/theory/arith/nl/iand_solver.cpp
@@ -34,11 +34,15 @@ namespace theory {
 namespace arith {
 namespace nl {
 
-IAndSolver::IAndSolver(InferenceManager& im, ArithState& state, NlModel& model)
-    : d_im(im),
+IAndSolver::IAndSolver(Env& env,
+                       InferenceManager& im,
+                       ArithState& state,
+                       NlModel& model)
+    : EnvObj(env),
+      d_im(im),
       d_model(model),
       d_astate(state),
-      d_initRefine(state.getUserContext())
+      d_initRefine(userContext())
 {
   NodeManager* nm = NodeManager::currentNM();
   d_false = nm->mkConst(false);
@@ -152,7 +156,7 @@ void IAndSolver::checkFullRefine()
       }
 
       // ************* additional lemma schemas go here
-      if (d_astate.options().smt.iandMode == options::IandMode::SUM)
+      if (options().smt.iandMode == options::IandMode::SUM)
       {
         Node lem = sumBasedLemma(i);  // add lemmas based on sum mode
         Trace("iand-lemma")
@@ -162,7 +166,7 @@ void IAndSolver::checkFullRefine()
         d_im.addPendingLemma(
             lem, InferenceId::ARITH_NL_IAND_SUM_REFINE, nullptr, true);
       }
-      else if (d_astate.options().smt.iandMode == options::IandMode::BITWISE)
+      else if (options().smt.iandMode == options::IandMode::BITWISE)
       {
         Node lem = bitwiseLemma(i);  // check for violated bitwise axioms
         Trace("iand-lemma")
@@ -245,7 +249,7 @@ Node IAndSolver::sumBasedLemma(Node i)
   Node x = i[0];
   Node y = i[1];
   size_t bvsize = i.getOperator().getConst<IntAnd>().d_size;
-  uint64_t granularity = d_astate.options().smt.BVAndIntegerGranularity;
+  uint64_t granularity = options().smt.BVAndIntegerGranularity;
   NodeManager* nm = NodeManager::currentNM();
   Node lem = nm->mkNode(
       EQUAL, i, d_iandUtils.createSumNode(x, y, bvsize, granularity));
@@ -259,7 +263,7 @@ Node IAndSolver::bitwiseLemma(Node i)
   Node y = i[1];
 
   unsigned bvsize = i.getOperator().getConst<IntAnd>().d_size;
-  uint64_t granularity = d_astate.options().smt.BVAndIntegerGranularity;
+  uint64_t granularity = options().smt.BVAndIntegerGranularity;
 
   Rational absI = d_model.computeAbstractModelValue(i).getConst<Rational>();
   Rational concI = d_model.computeConcreteModelValue(i).getConst<Rational>();

diff --git a/src/theory/arith/nl/iand_solver.h b/src/theory/arith/nl/iand_solver.h
index 1be469259921a0b15ed015121a0411dad207881f..0b6a1fac65b3f6b451eb615dd42f5072a2bd346b 100644 (file)
--- a/src/theory/arith/nl/iand_solver.h
+++ b/src/theory/arith/nl/iand_solver.h
@@ -21,6 +21,7 @@
 
 #include "context/cdhashset.h"
 #include "expr/node.h"
+#include "smt/env_obj.h"
 #include "theory/arith/nl/iand_utils.h"
 
 namespace cvc5 {
@@ -37,12 +38,12 @@ class NlModel;
 /** Integer and solver class
  *
  */
-class IAndSolver
+class IAndSolver : protected EnvObj
 {
   typedef context::CDHashSet<Node> NodeSet;
 
  public:
-  IAndSolver(InferenceManager& im, ArithState& state, NlModel& model);
+  IAndSolver(Env& env, InferenceManager& im, ArithState& state, NlModel& model);
   ~IAndSolver();
 
   /** init last call

diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index db92009f4b39b47312efc87217c8eddaf45b9e0c..742e5ca49eeaf2c93eb7935082ca578c65a53179 100644 (file)
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -58,8 +58,8 @@ NonlinearExtension::NonlinearExtension(Env& env,
       d_tangentPlaneSlv(&d_extState),
       d_cadSlv(d_astate.getEnv(), d_im, d_model),
       d_icpSlv(d_im),
-      d_iandSlv(d_im, state, d_model),
-      d_pow2Slv(d_im, state, d_model)
+      d_iandSlv(env, d_im, state, d_model),
+      d_pow2Slv(env, d_im, state, d_model)
 {
   d_extTheory.addFunctionKind(kind::NONLINEAR_MULT);
   d_extTheory.addFunctionKind(kind::EXPONENTIAL);

diff --git a/src/theory/arith/nl/pow2_solver.cpp b/src/theory/arith/nl/pow2_solver.cpp
index d708e86e1ec72f0a442e60fc85d510c3980cff91..597a0df96a03a8a9f8e70351819055058e72aea8 100644 (file)
--- a/src/theory/arith/nl/pow2_solver.cpp
+++ b/src/theory/arith/nl/pow2_solver.cpp
@@ -33,8 +33,11 @@ namespace theory {
 namespace arith {
 namespace nl {
 
-Pow2Solver::Pow2Solver(InferenceManager& im, ArithState& state, NlModel& model)
-    : d_im(im), d_model(model), d_initRefine(state.getUserContext())
+Pow2Solver::Pow2Solver(Env& env,
+                       InferenceManager& im,
+                       ArithState& state,
+                       NlModel& model)
+    : EnvObj(env), d_im(im), d_model(model), d_initRefine(userContext())
 {
   NodeManager* nm = NodeManager::currentNM();
   d_false = nm->mkConst(false);

diff --git a/src/theory/arith/nl/pow2_solver.h b/src/theory/arith/nl/pow2_solver.h
index 4c6fb8014752b1575e9b8fbf260a9656d8818998..b4e12616cb48d8a1acc53c2bc9980d408e648558 100644 (file)
--- a/src/theory/arith/nl/pow2_solver.h
+++ b/src/theory/arith/nl/pow2_solver.h
@@ -20,6 +20,7 @@
 
 #include "context/cdhashset.h"
 #include "expr/node.h"
+#include "smt/env_obj.h"
 
 namespace cvc5 {
 namespace theory {
@@ -35,12 +36,12 @@ class NlModel;
 /** pow2 solver class
  *
  */
-class Pow2Solver
+class Pow2Solver : protected EnvObj
 {
   using NodeSet = context::CDHashSet<Node>;
 
  public:
-  Pow2Solver(InferenceManager& im, ArithState& state, NlModel& model);
+  Pow2Solver(Env& env, InferenceManager& im, ArithState& state, NlModel& model);
   ~Pow2Solver();
 
   /** init last call

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index d94f81e9c737ace930c1826c0674a451a54eca2d..9642bf394edd280fd03e9a1df87a10e5224b9f36 100644 (file)
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -42,12 +42,12 @@ TheoryArith::TheoryArith(Env& env, OutputChannel& out, Valuation valuation)
       d_astate(env, valuation),
       d_im(env, *this, d_astate, d_pnm),
       d_ppre(context(), d_pnm),
-      d_bab(d_astate, d_im, d_ppre, d_pnm),
+      d_bab(env, d_astate, d_im, d_ppre, d_pnm),
       d_eqSolver(nullptr),
       d_internal(new TheoryArithPrivate(*this, env, d_bab)),
       d_nonlinearExtension(nullptr),
       d_opElim(d_pnm, logicInfo()),
-      d_arithPreproc(d_astate, d_im, d_pnm, d_opElim),
+      d_arithPreproc(env, d_astate, d_im, d_pnm, d_opElim),
       d_rewriter(d_opElim)
 {
   // currently a cyclic dependency to TheoryArithPrivate
@@ -58,7 +58,7 @@ TheoryArith::TheoryArith(Env& env, OutputChannel& out, Valuation valuation)
 
   if (options().arith.arithEqSolver)
   {
-    d_eqSolver.reset(new EqualitySolver(d_astate, d_im));
+    d_eqSolver.reset(new EqualitySolver(env, d_astate, d_im));
   }
 }
 

diff --git a/src/theory/arrays/inference_manager.cpp b/src/theory/arrays/inference_manager.cpp
index e59dfcc1349a8617bb43bcfecd77811d609ab711..4eef9a018c7ca6a8b2098bb6e920e97bae078fc3 100644 (file)
--- a/src/theory/arrays/inference_manager.cpp
+++ b/src/theory/arrays/inference_manager.cpp
@@ -33,7 +33,7 @@ InferenceManager::InferenceManager(Env& env,
                                    ProofNodeManager* pnm)
     : TheoryInferenceManager(env, t, state, pnm, "theory::arrays::", false),
       d_lemmaPg(pnm ? new EagerProofGenerator(
-                    pnm, state.getUserContext(), "ArrayLemmaProofGenerator")
+                    pnm, userContext(), "ArrayLemmaProofGenerator")
                     : nullptr)
 {
 }

diff --git a/src/theory/bags/term_registry.cpp b/src/theory/bags/term_registry.cpp
index 659886e83d020df44d56bcd92bf9c2add38017af..7e995eab5624fcb8a4c0fbd5914ae6056b7b504f 100644 (file)
--- a/src/theory/bags/term_registry.cpp
+++ b/src/theory/bags/term_registry.cpp
@@ -26,10 +26,11 @@ namespace cvc5 {
 namespace theory {
 namespace bags {
 
-TermRegistry::TermRegistry(SolverState& state, InferenceManager& im)
-    : d_im(im),
-      d_proxy(state.getUserContext()),
-      d_proxy_to_term(state.getUserContext())
+TermRegistry::TermRegistry(Env& env, SolverState& state, InferenceManager& im)
+    : EnvObj(env),
+      d_im(im),
+      d_proxy(userContext()),
+      d_proxy_to_term(userContext())
 {
 }
 

diff --git a/src/theory/bags/term_registry.h b/src/theory/bags/term_registry.h
index 2b0218fdf84ffeb85a24c3c3e340cbf08913945f..f36dda1a979981b798b1e206a68ac9ff5b2569a3 100644 (file)
--- a/src/theory/bags/term_registry.h
+++ b/src/theory/bags/term_registry.h
@@ -22,6 +22,7 @@
 
 #include "context/cdhashmap.h"
 #include "expr/node.h"
+#include "smt/env_obj.h"
 
 namespace cvc5 {
 namespace theory {
@@ -34,12 +35,12 @@ class SolverState;
  * Term registry, the purpose of this class is to maintain a database of
  * commonly used terms, and mappings from bags to their "proxy variables".
  */
-class TermRegistry
+class TermRegistry : protected EnvObj
 {
   typedef context::CDHashMap<Node, Node> NodeMap;
 
  public:
-  TermRegistry(SolverState& state, InferenceManager& im);
+  TermRegistry(Env& env, SolverState& state, InferenceManager& im);
 
   /**
    * Returns the existing empty bag for type tn

diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp
index c421b9ec210eaf1efbd42ca19039100cb630d00d..004766d83a00480a2aff26e202cd6e21cf5719f6 100644 (file)
--- a/src/theory/bags/theory_bags.cpp
+++ b/src/theory/bags/theory_bags.cpp
@@ -35,7 +35,7 @@ TheoryBags::TheoryBags(Env& env, OutputChannel& out, Valuation valuation)
       d_notify(*this, d_im),
       d_statistics(),
       d_rewriter(&d_statistics.d_rewrites),
-      d_termReg(d_state, d_im),
+      d_termReg(env, d_state, d_im),
       d_solver(d_state, d_im, d_termReg)
 {
   // use the official theory state and inference manager objects

diff --git a/src/theory/datatypes/inference_manager.cpp b/src/theory/datatypes/inference_manager.cpp
index c9750a5050e2ccc604781c53113cb89bb9b4d09c..d158cff08854fcd4d77432bc5cd5f7cab5c74af5 100644 (file)
--- a/src/theory/datatypes/inference_manager.cpp
+++ b/src/theory/datatypes/inference_manager.cpp
@@ -36,12 +36,10 @@ InferenceManager::InferenceManager(Env& env,
                                    ProofNodeManager* pnm)
     : InferenceManagerBuffered(env, t, state, pnm, "theory::datatypes::"),
       d_pnm(pnm),
-      d_ipc(pnm == nullptr ? nullptr
-                           : new InferProofCons(state.getSatContext(), pnm)),
-      d_lemPg(pnm == nullptr
-                  ? nullptr
-                  : new EagerProofGenerator(
-                      pnm, state.getUserContext(), "datatypes::lemPg"))
+      d_ipc(pnm == nullptr ? nullptr : new InferProofCons(context(), pnm)),
+      d_lemPg(pnm == nullptr ? nullptr
+                             : new EagerProofGenerator(
+                                 pnm, userContext(), "datatypes::lemPg"))
 {
   d_false = NodeManager::currentNM()->mkConst(false);
 }

diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp
index 8e3c22fb8ba371814ea23ee5a482982f16bc3bf1..ed112e4ea2ba502eddc72643dbdb96bd83caf8ec 100644 (file)
--- a/src/theory/datatypes/sygus_extension.cpp
+++ b/src/theory/datatypes/sygus_extension.cpp
@@ -1110,7 +1110,7 @@ Node SygusExtension::registerSearchValue(Node a,
             its = d_sampler[a].find(tn);
           }
           // check equivalent
-          its->second.checkEquivalent(bv, bvr, *d_state.options().base.out);
+          its->second.checkEquivalent(bv, bvr, *options().base.out);
         }
       }
 

diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp
index ead42a3cd51f47ff62ce8bf12a3915e04a9de958..dcfa71f8c81c1bbfd85e279a0828c09e1b755625 100644 (file)
--- a/src/theory/quantifiers/ematching/instantiation_engine.cpp
+++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp
@@ -32,7 +32,8 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
-InstantiationEngine::InstantiationEngine(QuantifiersState& qs,
+InstantiationEngine::InstantiationEngine(Env& env,
+                                         QuantifiersState& qs,
                                          QuantifiersInferenceManager& qim,
                                          QuantifiersRegistry& qr,
                                          TermRegistry& tr)
@@ -46,7 +47,7 @@ InstantiationEngine::InstantiationEngine(QuantifiersState& qs,
 {
   if (options::relevantTriggers())
   {
-    d_quant_rel.reset(new quantifiers::QuantRelevance);
+    d_quant_rel.reset(new quantifiers::QuantRelevance(env));
   }
   if (options::eMatching()) {
     // these are the instantiation strategies for E-matching

diff --git a/src/theory/quantifiers/ematching/instantiation_engine.h b/src/theory/quantifiers/ematching/instantiation_engine.h
index 45e137dd56013effd4cea484750432024022f68d..50685642dbce8a1871d13347e5d25dc712a7f5c9 100644 (file)
--- a/src/theory/quantifiers/ematching/instantiation_engine.h
+++ b/src/theory/quantifiers/ematching/instantiation_engine.h
@@ -34,7 +34,8 @@ class InstStrategyAutoGenTriggers;
 
 class InstantiationEngine : public QuantifiersModule {
  public:
-  InstantiationEngine(QuantifiersState& qs,
+  InstantiationEngine(Env& env,
+                      QuantifiersState& qs,
                       QuantifiersInferenceManager& qim,
                       QuantifiersRegistry& qr,
                       TermRegistry& tr);

diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp
index f87ec6435ebd7942361a271db52ee205b96ac53c..92ec1e4520442df24dc64449f79c4884605ec3ed 100644 (file)
--- a/src/theory/quantifiers/equality_query.cpp
+++ b/src/theory/quantifiers/equality_query.cpp
@@ -29,8 +29,9 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
-EqualityQuery::EqualityQuery(QuantifiersState& qs, FirstOrderModel* m)
-    : d_qstate(qs),
+EqualityQuery::EqualityQuery(Env& env, QuantifiersState& qs, FirstOrderModel* m)
+    : QuantifiersUtil(env),
+      d_qstate(qs),
       d_model(m),
       d_eqi_counter(qs.getSatContext()),
       d_reset_count(0)

diff --git a/src/theory/quantifiers/equality_query.h b/src/theory/quantifiers/equality_query.h
index f39ff86e3095eb3130a33df04ff684ba4d2a4dc2..200863cd61ca9b9672d53e666e9104feb8330446 100644 (file)
--- a/src/theory/quantifiers/equality_query.h
+++ b/src/theory/quantifiers/equality_query.h
@@ -43,7 +43,7 @@ class QuantifiersState;
 class EqualityQuery : public QuantifiersUtil
 {
  public:
-  EqualityQuery(QuantifiersState& qs, FirstOrderModel* m);
+  EqualityQuery(Env& env, QuantifiersState& qs, FirstOrderModel* m);
   virtual ~EqualityQuery();
 
   /** reset */

diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index d4bc7dfcb7f2103e8e71586a6d6380ed81486383..841177a7f340f4cf41e0a13e5d5fb4ac686c28e5 100644 (file)
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -42,13 +42,14 @@ struct ModelBasisArgAttributeId
 };
 using ModelBasisArgAttribute = expr::Attribute<ModelBasisArgAttributeId, uint64_t>;
 
-FirstOrderModel::FirstOrderModel(QuantifiersState& qs,
+FirstOrderModel::FirstOrderModel(Env& env,
+                                 QuantifiersState& qs,
                                  QuantifiersRegistry& qr,
                                  TermRegistry& tr)
     : d_model(nullptr),
       d_qreg(qr),
       d_treg(tr),
-      d_eq_query(qs, this),
+      d_eq_query(env, qs, this),
       d_forall_asserts(qs.getSatContext()),
       d_forallRlvComputed(false)
 {

diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index 1969fdde7a087e3093312b6c6f668f764830f243..05bdcbee6984c464b3f73acad2cfd4d253f55763 100644 (file)
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -39,7 +39,8 @@ class QuantifiersRegistry;
 class FirstOrderModel
 {
  public:
-  FirstOrderModel(QuantifiersState& qs,
+  FirstOrderModel(Env& env,
+                  QuantifiersState& qs,
                   QuantifiersRegistry& qr,
                   TermRegistry& tr);
   virtual ~FirstOrderModel() {}

diff --git a/src/theory/quantifiers/fmf/first_order_model_fmc.cpp b/src/theory/quantifiers/fmf/first_order_model_fmc.cpp
index e17271613cdcf2c67cbd58fa76b5b065bb8b59f7..4be13ba5ff3582f5219f2327046a856c8f671fed 100644 (file)
--- a/src/theory/quantifiers/fmf/first_order_model_fmc.cpp
+++ b/src/theory/quantifiers/fmf/first_order_model_fmc.cpp
@@ -36,10 +36,11 @@ struct IsStarAttributeId
 };
 using IsStarAttribute = expr::Attribute<IsStarAttributeId, bool>;
 
-FirstOrderModelFmc::FirstOrderModelFmc(QuantifiersState& qs,
+FirstOrderModelFmc::FirstOrderModelFmc(Env& env,
+                                       QuantifiersState& qs,
                                        QuantifiersRegistry& qr,
                                        TermRegistry& tr)
-    : FirstOrderModel(qs, qr, tr)
+    : FirstOrderModel(env, qs, qr, tr)
 {
 }
 

diff --git a/src/theory/quantifiers/fmf/first_order_model_fmc.h b/src/theory/quantifiers/fmf/first_order_model_fmc.h
index f148a9e1972ef2a5119fdf3fcd5bd2d030123d96..5a528ede1a43a4eedc05483a1f621cf4ba851c50 100644 (file)
--- a/src/theory/quantifiers/fmf/first_order_model_fmc.h
+++ b/src/theory/quantifiers/fmf/first_order_model_fmc.h
@@ -39,7 +39,8 @@ class FirstOrderModelFmc : public FirstOrderModel
   void processInitializeModelForTerm(Node n) override;
 
  public:
-  FirstOrderModelFmc(QuantifiersState& qs,
+  FirstOrderModelFmc(Env& env,
+                     QuantifiersState& qs,
                      QuantifiersRegistry& qr,
                      TermRegistry& tr);
   ~FirstOrderModelFmc() override;

diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp
index c4f83191b255ae3ea5d5d85d34a37c68842ac9fa..f8b90f6248701cb768a981a4ba00463d2270248a 100644 (file)
--- a/src/theory/quantifiers/fmf/full_model_check.cpp
+++ b/src/theory/quantifiers/fmf/full_model_check.cpp
@@ -286,11 +286,13 @@ void Def::debugPrint(const char * tr, Node op, FullModelChecker * m) {
   }
 }
 
-FullModelChecker::FullModelChecker(QuantifiersState& qs,
+FullModelChecker::FullModelChecker(Env& env,
+                                   QuantifiersState& qs,
                                    QuantifiersInferenceManager& qim,
                                    QuantifiersRegistry& qr,
                                    TermRegistry& tr)
-    : QModelBuilder(qs, qim, qr, tr), d_fm(new FirstOrderModelFmc(qs, qr, tr))
+    : QModelBuilder(env, qs, qim, qr, tr),
+      d_fm(new FirstOrderModelFmc(env, qs, qr, tr))
 {
   d_true = NodeManager::currentNM()->mkConst(true);
   d_false = NodeManager::currentNM()->mkConst(false);

diff --git a/src/theory/quantifiers/fmf/full_model_check.h b/src/theory/quantifiers/fmf/full_model_check.h
index e33d1db6d7d756af11a0c1a8fef9a05e0a5ff799..f3f8699aff06c787d221b8772f92293d2fcd2a1f 100644 (file)
--- a/src/theory/quantifiers/fmf/full_model_check.h
+++ b/src/theory/quantifiers/fmf/full_model_check.h
@@ -155,7 +155,8 @@ protected:
   Node getSomeDomainElement( FirstOrderModelFmc * fm, TypeNode tn );
 
  public:
-  FullModelChecker(QuantifiersState& qs,
+  FullModelChecker(Env& env,
+                   QuantifiersState& qs,
                    QuantifiersInferenceManager& qim,
                    QuantifiersRegistry& qr,
                    TermRegistry& tr);

diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp
index a331409f118ae93a4ab90a25ebf46d46cd033ac4..f43b7a6c98e472b4dbe6da0959d07c2ca91f3bdc 100644 (file)
--- a/src/theory/quantifiers/fmf/model_builder.cpp
+++ b/src/theory/quantifiers/fmf/model_builder.cpp
@@ -30,11 +30,12 @@ using namespace cvc5::context;
 using namespace cvc5::theory;
 using namespace cvc5::theory::quantifiers;
 
-QModelBuilder::QModelBuilder(QuantifiersState& qs,
+QModelBuilder::QModelBuilder(Env& env,
+                             QuantifiersState& qs,
                              QuantifiersInferenceManager& qim,
                              QuantifiersRegistry& qr,
                              TermRegistry& tr)
-    : TheoryEngineModelBuilder(qs.getEnv()),
+    : TheoryEngineModelBuilder(env),
       d_addedLemmas(0),
       d_triedLemmas(0),
       d_qstate(qs),
@@ -48,7 +49,7 @@ QModelBuilder::QModelBuilder(QuantifiersState& qs,
 void QModelBuilder::finishInit()
 {
   // allocate the default model
-  d_modelAloc.reset(new FirstOrderModel(d_qstate, d_qreg, d_treg));
+  d_modelAloc.reset(new FirstOrderModel(d_env, d_qstate, d_qreg, d_treg));
   d_model = d_modelAloc.get();
 }
 

diff --git a/src/theory/quantifiers/fmf/model_builder.h b/src/theory/quantifiers/fmf/model_builder.h
index a767af47aa2216fe8767af010e45406d754c86f8..f5dc7155b0d34bb3aebdd8285dadfd02f02d2e67 100644 (file)
--- a/src/theory/quantifiers/fmf/model_builder.h
+++ b/src/theory/quantifiers/fmf/model_builder.h
@@ -43,7 +43,8 @@ class QModelBuilder : public TheoryEngineModelBuilder
   unsigned d_triedLemmas;
 
  public:
-  QModelBuilder(QuantifiersState& qs,
+  QModelBuilder(Env& env,
+                QuantifiersState& qs,
                 QuantifiersInferenceManager& qim,
                 QuantifiersRegistry& qr,
                 TermRegistry& tr);

diff --git a/src/theory/quantifiers/ho_term_database.cpp b/src/theory/quantifiers/ho_term_database.cpp
index 3b97409cc66850ca7f3bc102bb0b910289271140..a2a8b8145e81d8be408fb1efd8f0763a2fab4dff 100644 (file)
--- a/src/theory/quantifiers/ho_term_database.cpp
+++ b/src/theory/quantifiers/ho_term_database.cpp
@@ -28,8 +28,8 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
-HoTermDb::HoTermDb(QuantifiersState& qs, QuantifiersRegistry& qr)
-    : TermDb(qs, qr)
+HoTermDb::HoTermDb(Env& env, QuantifiersState& qs, QuantifiersRegistry& qr)
+    : TermDb(env, qs, qr)
 {
 }
 
@@ -152,7 +152,7 @@ bool HoTermDb::resetInternal(Theory::Effort effort)
 
 bool HoTermDb::finishResetInternal(Theory::Effort effort)
 {
-  if (!d_qstate.options().quantifiers.hoMergeTermDb)
+  if (!options().quantifiers.hoMergeTermDb)
   {
     return true;
   }

diff --git a/src/theory/quantifiers/ho_term_database.h b/src/theory/quantifiers/ho_term_database.h
index 12bf0b49ff8b574a2043ea8175af5dbdcaca8472..885fec8f4d53e8d9105cf4edfd2e6510b339fea7 100644 (file)
--- a/src/theory/quantifiers/ho_term_database.h
+++ b/src/theory/quantifiers/ho_term_database.h
@@ -34,7 +34,7 @@ namespace quantifiers {
 class HoTermDb : public TermDb
 {
  public:
-  HoTermDb(QuantifiersState& qs, QuantifiersRegistry& qr);
+  HoTermDb(Env& env, QuantifiersState& qs, QuantifiersRegistry& qr);
   ~HoTermDb();
   /** identify */
   std::string identify() const override { return "HoTermDb"; }

diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index 9010d4fe17162108cd98c74f0d5e72ee5a09cbd8..f0af73832b09012ce2a667f6031d93e10c97591f 100644 (file)
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -42,12 +42,14 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
-Instantiate::Instantiate(QuantifiersState& qs,
+Instantiate::Instantiate(Env& env,
+                         QuantifiersState& qs,
                          QuantifiersInferenceManager& qim,
                          QuantifiersRegistry& qr,
                          TermRegistry& tr,
                          ProofNodeManager* pnm)
-    : d_qstate(qs),
+    : QuantifiersUtil(env),
+      d_qstate(qs),
       d_qim(qim),
       d_qreg(qr),
       d_treg(tr),

diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h
index 1f380350f4850d47f5d2b13f1af4d6d4724454f3..753213f35319e65d0749f102f2ac6e0ed8f1d0ed 100644 (file)
--- a/src/theory/quantifiers/instantiate.h
+++ b/src/theory/quantifiers/instantiate.h
@@ -104,7 +104,8 @@ class Instantiate : public QuantifiersUtil
       context::CDHashMap<Node, std::shared_ptr<InstLemmaList>>;
 
  public:
-  Instantiate(QuantifiersState& qs,
+  Instantiate(Env& env,
+              QuantifiersState& qs,
               QuantifiersInferenceManager& qim,
               QuantifiersRegistry& qr,
               TermRegistry& tr,

diff --git a/src/theory/quantifiers/quant_relevance.cpp b/src/theory/quantifiers/quant_relevance.cpp
index 0c1db860f079824d7ac2646cf64bd06b2bda000f..abb8c92198a86c4b3d842450fc3389cd214373fb 100644 (file)
--- a/src/theory/quantifiers/quant_relevance.cpp
+++ b/src/theory/quantifiers/quant_relevance.cpp
@@ -23,6 +23,8 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
+QuantRelevance::QuantRelevance(Env& env) : QuantifiersUtil(env) {}
+
 void QuantRelevance::registerQuantifier(Node f)
 {
   // compute symbols in f

diff --git a/src/theory/quantifiers/quant_relevance.h b/src/theory/quantifiers/quant_relevance.h
index c22e560f9171b09be2c831cd5f8e796ec5da0ee1..418b859b9de60a9d936e0d2b764e76123d911b5a 100644 (file)
--- a/src/theory/quantifiers/quant_relevance.h
+++ b/src/theory/quantifiers/quant_relevance.h
@@ -40,7 +40,7 @@ class QuantRelevance : public QuantifiersUtil
    * if this is false, then all calls to getRelevance
    * return -1.
    */
-  QuantRelevance() {}
+  QuantRelevance(Env& env);
   ~QuantRelevance() {}
   /** reset */
   bool reset(Theory::Effort e) override { return true; }

diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index 64a816975e20b083eea5884ac55ce179a880351d..cbe09af2e04ccba2082081cee713e0152c3d268a 100644 (file)
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -22,6 +22,8 @@ using namespace cvc5::kind;
 namespace cvc5 {
 namespace theory {
 
+QuantifiersUtil::QuantifiersUtil(Env& env) : EnvObj(env) {}
+
 QuantPhaseReq::QuantPhaseReq( Node n, bool computeEq ){
   initialize( n, computeEq );
 }

diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index 7ca17b6ad29fb1ca2713c22bb75bc8a282b4b374..a422101f09b8d74c68aee5445b3288ca38410207 100644 (file)
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -23,6 +23,7 @@
 #include <vector>
 
 #include "expr/node.h"
+#include "smt/env_obj.h"
 #include "theory/incomplete_id.h"
 #include "theory/theory.h"
 
@@ -34,9 +35,10 @@ namespace theory {
  * This is a lightweight version of a quantifiers module that does not implement
  * methods for checking satisfiability.
  */
-class QuantifiersUtil {
-public:
-  QuantifiersUtil(){}
+class QuantifiersUtil : protected EnvObj
+{
+ public:
+  QuantifiersUtil(Env& env);
   virtual ~QuantifiersUtil(){}
   /**  Called at the beginning of check-sat call. */
   virtual void presolve() {}

diff --git a/src/theory/quantifiers/quantifiers_inference_manager.cpp b/src/theory/quantifiers/quantifiers_inference_manager.cpp
index 24159d397a761a530814ce5e2b834bbf267d6617..b2a08c2493cab60e18b4027bbea99c26ee8a95af 100644 (file)
--- a/src/theory/quantifiers/quantifiers_inference_manager.cpp
+++ b/src/theory/quantifiers/quantifiers_inference_manager.cpp
@@ -30,7 +30,7 @@ QuantifiersInferenceManager::QuantifiersInferenceManager(
     TermRegistry& tr,
     ProofNodeManager* pnm)
     : InferenceManagerBuffered(env, t, state, pnm, "theory::quantifiers::"),
-      d_instantiate(new Instantiate(state, *this, qr, tr, pnm)),
+      d_instantiate(new Instantiate(env, state, *this, qr, tr, pnm)),
       d_skolemize(new Skolemize(state, tr, pnm))
 {
 }

diff --git a/src/theory/quantifiers/quantifiers_modules.cpp b/src/theory/quantifiers/quantifiers_modules.cpp
index 6cfc48fb95a5d4d4e928dd04d4202a0c26ce1d58..889b6ac26b21925d032657e8937b70d08b3b75ed 100644 (file)
--- a/src/theory/quantifiers/quantifiers_modules.cpp
+++ b/src/theory/quantifiers/quantifiers_modules.cpp
@@ -62,7 +62,7 @@ void QuantifiersModules::initialize(Env& env,
   }
   if (!options::finiteModelFind() || options::fmfInstEngine())
   {
-    d_inst_engine.reset(new InstantiationEngine(qs, qim, qr, tr));
+    d_inst_engine.reset(new InstantiationEngine(env, qs, qim, qr, tr));
     modules.push_back(d_inst_engine.get());
   }
   if (options::cegqi())
@@ -101,7 +101,7 @@ void QuantifiersModules::initialize(Env& env,
   // full saturation : instantiate from relevant domain, then arbitrary terms
   if (options::fullSaturateQuant() || options::fullSaturateInterleave())
   {
-    d_rel_dom.reset(new RelevantDomain(qs, qr, tr));
+    d_rel_dom.reset(new RelevantDomain(env, qs, qr, tr));
     d_fs.reset(new InstStrategyEnum(qs, qim, qr, tr, d_rel_dom.get()));
     modules.push_back(d_fs.get());
   }

diff --git a/src/theory/quantifiers/quantifiers_registry.cpp b/src/theory/quantifiers/quantifiers_registry.cpp
index 4dc329d8ee9006865d0275f1dcac7d3c9a922554..6d5e003635cbe9c64ea11174f70e7978512f5cb8 100644 (file)
--- a/src/theory/quantifiers/quantifiers_registry.cpp
+++ b/src/theory/quantifiers/quantifiers_registry.cpp
@@ -24,7 +24,8 @@ namespace theory {
 namespace quantifiers {
 
 QuantifiersRegistry::QuantifiersRegistry(Env& env)
-    : d_quantAttr(),
+    : QuantifiersUtil(env),
+      d_quantAttr(),
       d_quantBoundInf(options::fmfTypeCompletionThresh(),
                       options::finiteModelFind()),
       d_quantPreproc(env)

diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp
index 7e2c0c909f9614ed4bfb767ff79cfffa44dbf4e8..f4eb954692c83a8c780aae8e95fbd1e492d6b072 100644 (file)
--- a/src/theory/quantifiers/relevant_domain.cpp
+++ b/src/theory/quantifiers/relevant_domain.cpp
@@ -75,10 +75,11 @@ void RelevantDomain::RDomain::removeRedundantTerms(QuantifiersState& qs)
   }
 }
 
-RelevantDomain::RelevantDomain(QuantifiersState& qs,
+RelevantDomain::RelevantDomain(Env& env,
+                               QuantifiersState& qs,
                                QuantifiersRegistry& qr,
                                TermRegistry& tr)
-    : d_qs(qs), d_qreg(qr), d_treg(tr)
+    : QuantifiersUtil(env), d_qs(qs), d_qreg(qr), d_treg(tr)
 {
   d_is_computed = false;
 }

diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h
index 5643a466503ebf90505f7e1a263ceb2d4cfd4318..3b44b226301c56062b3174d8750d50d5901df6e0 100644 (file)
--- a/src/theory/quantifiers/relevant_domain.h
+++ b/src/theory/quantifiers/relevant_domain.h
@@ -45,7 +45,8 @@ class TermRegistry;
 class RelevantDomain : public QuantifiersUtil
 {
  public:
-  RelevantDomain(QuantifiersState& qs,
+  RelevantDomain(Env& env,
+                 QuantifiersState& qs,
                  QuantifiersRegistry& qr,
                  TermRegistry& tr);
   virtual ~RelevantDomain();

diff --git a/src/theory/quantifiers/sygus/enum_value_manager.cpp b/src/theory/quantifiers/sygus/enum_value_manager.cpp
index 1d0ba5bee455f7056e024c6e2d6a5af36d551d35..e7b3bbaa995abb70d91fc66011bfe353f72b2592 100644 (file)
--- a/src/theory/quantifiers/sygus/enum_value_manager.cpp
+++ b/src/theory/quantifiers/sygus/enum_value_manager.cpp
@@ -110,7 +110,7 @@ Node EnumValueManager::getEnumeratedValue(bool& activeIncomplete)
             d_samplerRrV->initializeSygus(
                 d_tds, e, options::sygusSamples(), false);
             // use the default output for the output of sygusRewVerify
-            out = d_qstate.options().base.out;
+            out = options().base.out;
           }
           d_secd.reset(new SygusEnumeratorCallbackDefault(
               e, &d_stats, d_eec.get(), d_samplerRrV.get(), out));

diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index e87857c3bd1b79ace355e7951c09f7f51c20785e..730482073bd8f870c142c0eef173a37653ec3959 100644 (file)
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -58,7 +58,7 @@ SynthConjecture::SynthConjecture(Env& env,
       d_treg(tr),
       d_stats(s),
       d_tds(tr.getTermDatabaseSygus()),
-      d_verify(qs.options(), qs.getLogicInfo(), d_tds),
+      d_verify(options(), qs.getLogicInfo(), d_tds),
       d_hasSolution(false),
       d_ceg_si(new CegSingleInv(env, tr, s)),
       d_templInfer(new SygusTemplateInfer),
@@ -515,7 +515,7 @@ bool SynthConjecture::doCheck()
   {
     if (printDebug)
     {
-      const Options& sopts = d_qstate.options();
+      const Options& sopts = options();
       std::ostream& out = *sopts.base.out;
       out << "(sygus-candidate ";
       Assert(d_quant[0].getNumChildren() == candidate_values.size());
@@ -801,8 +801,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
-  const Options& sopts = d_qstate.options();
-  printSynthSolutionInternal(*sopts.base.out);
+  printSynthSolutionInternal(*options().base.out);
   excludeCurrentSolution(enums, values);
 }
 

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index d2f872afb3d3a610467f6943975a9daae3ca7bc5..6aa2a816a356083ce5cbcc00155f33f8735dbf7a 100644 (file)
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -37,8 +37,9 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
-TermDb::TermDb(QuantifiersState& qs, QuantifiersRegistry& qr)
-    : d_qstate(qs),
+TermDb::TermDb(Env& env, QuantifiersState& qs, QuantifiersRegistry& qr)
+    : QuantifiersUtil(env),
+      d_qstate(qs),
       d_qim(nullptr),
       d_qreg(qr),
       d_termsContext(),

diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index a4e95487c7942c2a0255a75416286b3715d2387f..af0b87bd843cfd08e1fd366c9b8f328cda83efb9 100644 (file)
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -73,8 +73,7 @@ class TermDb : public QuantifiersUtil {
   using NodeDbListMap = context::CDHashMap<Node, std::shared_ptr<DbList>>;
 
  public:
-  TermDb(QuantifiersState& qs,
-         QuantifiersRegistry& qr);
+  TermDb(Env& env, QuantifiersState& qs, QuantifiersRegistry& qr);
   virtual ~TermDb();
   /** Finish init, which sets the inference manager */
   void finishInit(QuantifiersInferenceManager* qim);

diff --git a/src/theory/quantifiers/term_pools.cpp b/src/theory/quantifiers/term_pools.cpp
index 2d95c8b20640163df85d8294a7096091593fe58a..7bac0252d0e2ba280522c98ba0bc9b5bc113b45e 100644 (file)
--- a/src/theory/quantifiers/term_pools.cpp
+++ b/src/theory/quantifiers/term_pools.cpp
@@ -36,7 +36,10 @@ void TermPoolQuantInfo::initialize()
   d_skolemAddToPool.clear();
 }
 
-TermPools::TermPools(QuantifiersState& qs) : d_qs(qs) {}
+TermPools::TermPools(Env& env, QuantifiersState& qs)
+    : QuantifiersUtil(env), d_qs(qs)
+{
+}
 
 bool TermPools::reset(Theory::Effort e)
 {

diff --git a/src/theory/quantifiers/term_pools.h b/src/theory/quantifiers/term_pools.h
index 5a7556ad9392163feff4cc5289dbc0de0a454752..37b16a785e033779d9f5ee82a0ac76fec0a6207c 100644 (file)
--- a/src/theory/quantifiers/term_pools.h
+++ b/src/theory/quantifiers/term_pools.h
@@ -71,7 +71,7 @@ class TermPoolQuantInfo
 class TermPools : public QuantifiersUtil
 {
  public:
-  TermPools(QuantifiersState& qs);
+  TermPools(Env& env, QuantifiersState& qs);
   ~TermPools() {}
   /** reset, which resets the current values of pools */
   bool reset(Theory::Effort e) override;

diff --git a/src/theory/quantifiers/term_registry.cpp b/src/theory/quantifiers/term_registry.cpp
index 36dc8865c86bb4c502c83f7be8d47491922fe33c..7ad782fda0a01e4ba9800fe59bcf044a3979c894 100644 (file)
--- a/src/theory/quantifiers/term_registry.cpp
+++ b/src/theory/quantifiers/term_registry.cpp
@@ -35,9 +35,10 @@ TermRegistry::TermRegistry(Env& env,
     : d_presolve(qs.getUserContext(), true),
       d_presolveCache(qs.getUserContext()),
       d_termEnum(new TermEnumeration),
-      d_termPools(new TermPools(qs)),
-      d_termDb(qs.getEnv().getLogicInfo().isHigherOrder() ? new HoTermDb(qs, qr)
-                                                          : new TermDb(qs, qr)),
+      d_termPools(new TermPools(env, qs)),
+      d_termDb(qs.getEnv().getLogicInfo().isHigherOrder()
+                   ? new HoTermDb(env, qs, qr)
+                   : new TermDb(env, qs, qr)),
       d_sygusTdb(nullptr),
       d_qmodel(nullptr)
 {

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 40923ad0dc1b1525a47c788c4e74cddfc9622db0..5f914484a53c80a8240e8da45e011c6e5a2eb69f 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -76,12 +76,12 @@ QuantifiersEngine::QuantifiersEngine(
   {
     Trace("quant-init-debug") << "...make fmc builder." << std::endl;
     d_builder.reset(
-        new quantifiers::fmcheck::FullModelChecker(qs, qim, qr, tr));
+        new quantifiers::fmcheck::FullModelChecker(env, qs, qim, qr, tr));
   }
   else
   {
     Trace("quant-init-debug") << "...make default model builder." << std::endl;
-    d_builder.reset(new quantifiers::QModelBuilder(qs, qim, qr, tr));
+    d_builder.reset(new quantifiers::QModelBuilder(env, qs, qim, qr, tr));
   }
   // set the model object
   d_builder->finishInit();
@@ -113,7 +113,7 @@ void QuantifiersEngine::finishInit(TheoryEngine* te)
   d_model->finishInit(te->getModel());
   d_te = te;
   // Initialize the modules and the utilities here.
-  d_qmodules.reset(new quantifiers::QuantifiersModules);
+  d_qmodules.reset(new quantifiers::QuantifiersModules());
   d_qmodules->initialize(
       d_env, d_qstate, d_qim, d_qreg, d_treg, d_builder.get(), d_modules);
   if (d_qmodules->d_rel_dom.get())

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