From d6b3329e3f2b6e29e5f4af6cf09fd32e26c47e15 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 8 Sep 2021 12:30:31 -0500 Subject: Towards standard usage of ExtendedRewriter (#7145) This PR: Adds extendedRewrite to EnvObj and Rewriter. Eliminates static calls to Rewriter::rewrite from within the extended rewriter. Instead, the use of extended rewriter is always through Rewriter, which passes itself to the ExtendedRewriter. Make most uses of extended rewriter non-static. I've added a placeholder method Rewriter::callExtendedRewrite for places in the code that call the extended rewriter are currently difficult to eliminate. --- src/theory/quantifiers/sygus/enum_value_manager.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'src/theory/quantifiers/sygus/enum_value_manager.cpp') diff --git a/src/theory/quantifiers/sygus/enum_value_manager.cpp b/src/theory/quantifiers/sygus/enum_value_manager.cpp index 8a2d70bfa..1d0ba5bee 100644 --- a/src/theory/quantifiers/sygus/enum_value_manager.cpp +++ b/src/theory/quantifiers/sygus/enum_value_manager.cpp @@ -33,13 +33,15 @@ namespace cvc5 { namespace theory { namespace quantifiers { -EnumValueManager::EnumValueManager(Node e, +EnumValueManager::EnumValueManager(Env& env, QuantifiersState& qs, QuantifiersInferenceManager& qim, TermRegistry& tr, SygusStatistics& s, + Node e, bool hasExamples) - : d_enum(e), + : EnvObj(env), + d_enum(e), d_qstate(qs), d_qim(qim), d_treg(tr), -- cgit v1.2.3 From dfd135ee8039c901e535b0781ae1b27cb3365166 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 8 Sep 2021 18:28:25 -0700 Subject: Remove `TheoryState::options()` (#7148) This commit removes TheoryState::options() by changing more classes to EnvObjs. --- src/theory/arith/arith_preprocess.cpp | 5 +++-- src/theory/arith/arith_preprocess.h | 6 ++++-- src/theory/arith/branch_and_bound.cpp | 10 ++++++---- src/theory/arith/branch_and_bound.h | 6 ++++-- src/theory/arith/equality_solver.cpp | 9 ++++++--- src/theory/arith/equality_solver.h | 5 +++-- src/theory/arith/inference_manager.cpp | 4 ++-- src/theory/arith/nl/iand_solver.cpp | 18 +++++++++++------- src/theory/arith/nl/iand_solver.h | 5 +++-- src/theory/arith/nl/nonlinear_extension.cpp | 4 ++-- src/theory/arith/nl/pow2_solver.cpp | 7 +++++-- src/theory/arith/nl/pow2_solver.h | 5 +++-- src/theory/arith/theory_arith.cpp | 6 +++--- src/theory/arrays/inference_manager.cpp | 2 +- src/theory/bags/term_registry.cpp | 9 +++++---- src/theory/bags/term_registry.h | 5 +++-- src/theory/bags/theory_bags.cpp | 2 +- src/theory/datatypes/inference_manager.cpp | 10 ++++------ src/theory/datatypes/sygus_extension.cpp | 2 +- .../quantifiers/ematching/instantiation_engine.cpp | 5 +++-- .../quantifiers/ematching/instantiation_engine.h | 3 ++- src/theory/quantifiers/equality_query.cpp | 5 +++-- src/theory/quantifiers/equality_query.h | 2 +- src/theory/quantifiers/first_order_model.cpp | 5 +++-- src/theory/quantifiers/first_order_model.h | 3 ++- src/theory/quantifiers/fmf/first_order_model_fmc.cpp | 5 +++-- src/theory/quantifiers/fmf/first_order_model_fmc.h | 3 ++- src/theory/quantifiers/fmf/full_model_check.cpp | 6 ++++-- src/theory/quantifiers/fmf/full_model_check.h | 3 ++- src/theory/quantifiers/fmf/model_builder.cpp | 7 ++++--- src/theory/quantifiers/fmf/model_builder.h | 3 ++- src/theory/quantifiers/ho_term_database.cpp | 6 +++--- src/theory/quantifiers/ho_term_database.h | 2 +- src/theory/quantifiers/instantiate.cpp | 6 ++++-- src/theory/quantifiers/instantiate.h | 3 ++- src/theory/quantifiers/quant_relevance.cpp | 2 ++ src/theory/quantifiers/quant_relevance.h | 2 +- src/theory/quantifiers/quant_util.cpp | 2 ++ src/theory/quantifiers/quant_util.h | 8 +++++--- .../quantifiers/quantifiers_inference_manager.cpp | 2 +- src/theory/quantifiers/quantifiers_modules.cpp | 4 ++-- src/theory/quantifiers/quantifiers_registry.cpp | 3 ++- src/theory/quantifiers/relevant_domain.cpp | 5 +++-- src/theory/quantifiers/relevant_domain.h | 3 ++- src/theory/quantifiers/sygus/enum_value_manager.cpp | 2 +- src/theory/quantifiers/sygus/synth_conjecture.cpp | 7 +++---- src/theory/quantifiers/term_database.cpp | 5 +++-- src/theory/quantifiers/term_database.h | 3 +-- src/theory/quantifiers/term_pools.cpp | 5 ++++- src/theory/quantifiers/term_pools.h | 2 +- src/theory/quantifiers/term_registry.cpp | 7 ++++--- src/theory/quantifiers_engine.cpp | 6 +++--- src/theory/theory_state.h | 2 -- 53 files changed, 151 insertions(+), 106 deletions(-) (limited to 'src/theory/quantifiers/sygus/enum_value_manager.cpp') diff --git a/src/theory/arith/arith_preprocess.cpp b/src/theory/arith/arith_preprocess.cpp index 6ab399348..ba2de9fdf 100644 --- 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 a537c33c7..939306a6e 100644 --- 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 ca1a2fa6f..31017dea6 100644 --- 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 4281ba678..52acf6aae 100644 --- 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 8b4e1b8dd..8e5cc9a28 100644 --- 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 bce30e697..8528650f0 100644 --- 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; 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 5ab606f96..0c6b18893 100644 --- 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 eb5620a82..76d964934 100644 --- 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().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().d_size; - uint64_t granularity = d_astate.options().smt.BVAndIntegerGranularity; + uint64_t granularity = options().smt.BVAndIntegerGranularity; Rational absI = d_model.computeAbstractModelValue(i).getConst(); Rational concI = d_model.computeConcreteModelValue(i).getConst(); diff --git a/src/theory/arith/nl/iand_solver.h b/src/theory/arith/nl/iand_solver.h index 1be469259..0b6a1fac6 100644 --- 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 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 db92009f4..742e5ca49 100644 --- 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 d708e86e1..597a0df96 100644 --- 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 4c6fb8014..b4e12616c 100644 --- 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; 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 d94f81e9c..9642bf394 100644 --- 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 e59dfcc13..4eef9a018 100644 --- 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 659886e83..7e995eab5 100644 --- 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 2b0218fdf..f36dda1a9 100644 --- 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 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 c421b9ec2..004766d83 100644 --- 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 c9750a505..d158cff08 100644 --- 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 8e3c22fb8..ed112e4ea 100644 --- 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 ead42a3cd..dcfa71f8c 100644 --- 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 45e137dd5..50685642d 100644 --- 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 f87ec6435..92ec1e452 100644 --- 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 f39ff86e3..200863cd6 100644 --- 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 d4bc7dfcb..841177a7f 100644 --- 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; -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 1969fdde7..05bdcbee6 100644 --- 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 e17271613..4be13ba5f 100644 --- 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; -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 f148a9e19..5a528ede1 100644 --- 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 c4f83191b..f8b90f624 100644 --- 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 e33d1db6d..f3f8699af 100644 --- 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 a331409f1..f43b7a6c9 100644 --- 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 a767af47a..f5dc7155b 100644 --- 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 3b97409cc..a2a8b8145 100644 --- 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 12bf0b49f..885fec8f4 100644 --- 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 9010d4fe1..f0af73832 100644 --- 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 1f380350f..753213f35 100644 --- a/src/theory/quantifiers/instantiate.h +++ b/src/theory/quantifiers/instantiate.h @@ -104,7 +104,8 @@ class Instantiate : public QuantifiersUtil context::CDHashMap>; 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 0c1db860f..abb8c9219 100644 --- 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 c22e560f9..418b859b9 100644 --- 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 64a816975..cbe09af2e 100644 --- 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 7ca17b6ad..a422101f0 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -23,6 +23,7 @@ #include #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 24159d397..b2a08c249 100644 --- 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 6cfc48fb9..889b6ac26 100644 --- 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 4dc329d8e..6d5e00363 100644 --- 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 7e2c0c909..f4eb95469 100644 --- 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 5643a4665..3b44b2263 100644 --- 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 1d0ba5bee..e7b3bbaa9 100644 --- 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 e87857c3b..730482073 100644 --- 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& 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 d2f872afb..6aa2a816a 100644 --- 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 a4e95487c..af0b87bd8 100644 --- 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>; 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 2d95c8b20..7bac0252d 100644 --- 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 5a7556ad9..37b16a785 100644 --- 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 36dc8865c..7ad782fda 100644 --- 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 40923ad0d..5f914484a 100644 --- 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 9162fdeb6..049123b8d 100644 --- 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; -- cgit v1.2.3