diff options
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/arith_preprocess.cpp | 5 | ||||
-rw-r--r-- | src/theory/arith/arith_preprocess.h | 6 | ||||
-rw-r--r-- | src/theory/arith/branch_and_bound.cpp | 10 | ||||
-rw-r--r-- | src/theory/arith/branch_and_bound.h | 6 | ||||
-rw-r--r-- | src/theory/arith/equality_solver.cpp | 9 | ||||
-rw-r--r-- | src/theory/arith/equality_solver.h | 5 | ||||
-rw-r--r-- | src/theory/arith/inference_manager.cpp | 4 | ||||
-rw-r--r-- | src/theory/arith/nl/iand_solver.cpp | 18 | ||||
-rw-r--r-- | src/theory/arith/nl/iand_solver.h | 5 | ||||
-rw-r--r-- | src/theory/arith/nl/nonlinear_extension.cpp | 4 | ||||
-rw-r--r-- | src/theory/arith/nl/pow2_solver.cpp | 7 | ||||
-rw-r--r-- | src/theory/arith/nl/pow2_solver.h | 5 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 6 |
13 files changed, 55 insertions, 35 deletions
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<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 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<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 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<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 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<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 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)); } } |