diff options
Diffstat (limited to 'src/theory/arith/nl')
-rw-r--r-- | src/theory/arith/nl/cad/cdcac.cpp | 9 | ||||
-rw-r--r-- | src/theory/arith/nl/cad/cdcac.h | 6 | ||||
-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 | 14 | ||||
-rw-r--r-- | src/theory/arith/nl/pow2_solver.cpp | 7 | ||||
-rw-r--r-- | src/theory/arith/nl/pow2_solver.h | 5 |
7 files changed, 35 insertions, 29 deletions
diff --git a/src/theory/arith/nl/cad/cdcac.cpp b/src/theory/arith/nl/cad/cdcac.cpp index 9b37a135f..9b7678388 100644 --- a/src/theory/arith/nl/cad/cdcac.cpp +++ b/src/theory/arith/nl/cad/cdcac.cpp @@ -23,7 +23,7 @@ #include "theory/arith/nl/cad/projections.h" #include "theory/arith/nl/cad/variable_ordering.h" #include "theory/arith/nl/nl_model.h" -#include "theory/quantifiers/extended_rewrite.h" +#include "theory/rewriter.h" namespace std { /** Generic streaming operator for std::vector. */ @@ -42,7 +42,7 @@ namespace nl { namespace cad { CDCAC::CDCAC(Env& env, const std::vector<poly::Variable>& ordering) - : d_env(env), d_variableOrdering(ordering) + : EnvObj(env), d_variableOrdering(ordering) { if (d_env.isTheoryProofProducing()) { @@ -276,9 +276,8 @@ PolyVector requiredCoefficientsLazardModified( Kind::EQUAL, nl::as_cvc_polynomial(coeff, vm), zero)); } // if phi is false (i.e. p can not vanish) - quantifiers::ExtendedRewriter rew; - Node rewritten = - rew.extendedRewrite(NodeManager::currentNM()->mkAnd(conditions)); + Node rewritten = Rewriter::callExtendedRewrite( + NodeManager::currentNM()->mkAnd(conditions)); if (rewritten.isConst()) { Assert(rewritten.getKind() == Kind::CONST_BOOLEAN); diff --git a/src/theory/arith/nl/cad/cdcac.h b/src/theory/arith/nl/cad/cdcac.h index b504998d8..be72e4063 100644 --- a/src/theory/arith/nl/cad/cdcac.h +++ b/src/theory/arith/nl/cad/cdcac.h @@ -26,6 +26,7 @@ #include <vector> #include "smt/env.h" +#include "smt/env_obj.h" #include "theory/arith/nl/cad/cdcac_utils.h" #include "theory/arith/nl/cad/constraints.h" #include "theory/arith/nl/cad/proof_generator.h" @@ -44,7 +45,7 @@ namespace cad { * This class implements Cylindrical Algebraic Coverings as presented in * https://arxiv.org/pdf/2003.05633.pdf */ -class CDCAC +class CDCAC : protected EnvObj { public: /** Initialize this method with the given variable ordering. */ @@ -184,9 +185,6 @@ class CDCAC */ void pruneRedundantIntervals(std::vector<CACInterval>& intervals); - /** A reference to the environment */ - Env& d_env; - /** * The current assignment. When the method terminates with SAT, it contains a * model for the input constraints. 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..b8170df45 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -49,17 +49,17 @@ NonlinearExtension::NonlinearExtension(Env& env, d_extTheoryCb(state.getEqualityEngine()), d_extTheory(d_extTheoryCb, context(), userContext(), d_im), d_model(), - d_trSlv(d_im, d_model, d_astate.getEnv()), - d_extState(d_im, d_model, d_astate.getEnv()), + d_trSlv(d_im, d_model, d_env), + d_extState(d_im, d_model, d_env), d_factoringSlv(&d_extState), d_monomialBoundsSlv(&d_extState), d_monomialSlv(&d_extState), d_splitZeroSlv(&d_extState), d_tangentPlaneSlv(&d_extState), - d_cadSlv(d_astate.getEnv(), d_im, d_model), + d_cadSlv(d_env, d_im, d_model), d_icpSlv(d_im), - d_iandSlv(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); @@ -72,9 +72,9 @@ NonlinearExtension::NonlinearExtension(Env& env, d_one = NodeManager::currentNM()->mkConst(Rational(1)); d_neg_one = NodeManager::currentNM()->mkConst(Rational(-1)); - if (d_astate.getEnv().isTheoryProofProducing()) + if (d_env.isTheoryProofProducing()) { - ProofChecker* pc = d_astate.getEnv().getProofNodeManager()->getChecker(); + ProofChecker* pc = d_env.getProofNodeManager()->getChecker(); d_proofChecker.registerTo(pc); } } diff --git a/src/theory/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 |