From 48904b48eff10b6db84053584511d779fe2bc5fe Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Thu, 19 Aug 2021 18:30:31 -0700 Subject: [PATCH] Use Env class in nonlinear extension (#7039) This PR refactors the nonlinear extension(s) to access options only via the environment class. --- src/theory/arith/branch_and_bound.cpp | 2 +- src/theory/arith/inference_manager.cpp | 4 +-- src/theory/arith/nl/cad/cdcac.cpp | 24 +++++++------- src/theory/arith/nl/cad/cdcac.h | 8 +++-- src/theory/arith/nl/cad_solver.cpp | 11 +++---- src/theory/arith/nl/cad_solver.h | 5 +-- src/theory/arith/nl/iand_solver.cpp | 9 +++--- src/theory/arith/nl/iand_solver.h | 2 ++ src/theory/arith/nl/nl_model.cpp | 7 ++-- src/theory/arith/nl/nl_model.h | 5 +-- src/theory/arith/nl/nonlinear_extension.cpp | 29 +++++++++-------- src/theory/arith/nl/strategy.cpp | 36 ++++++++++----------- src/theory/arith/nl/strategy.h | 4 ++- src/theory/arith/theory_arith.cpp | 2 +- test/unit/theory/theory_arith_cad_white.cpp | 20 +++++++++--- 15 files changed, 92 insertions(+), 76 deletions(-) diff --git a/src/theory/arith/branch_and_bound.cpp b/src/theory/arith/branch_and_bound.cpp index 22859977b..ca1a2fa6f 100644 --- a/src/theory/arith/branch_and_bound.cpp +++ b/src/theory/arith/branch_and_bound.cpp @@ -45,7 +45,7 @@ TrustNode BranchAndBound::branchIntegerVariable(TNode var, Rational value) TrustNode lem = TrustNode::null(); NodeManager* nm = NodeManager::currentNM(); Integer floor = value.floor(); - if (options::brabTest()) + if (d_astate.options().arith.brabTest) { Trace("integers") << "branch-round-and-bound enabled" << std::endl; Integer ceil = value.ceiling(); diff --git a/src/theory/arith/inference_manager.cpp b/src/theory/arith/inference_manager.cpp index 9cb232908..1563ca418 100644 --- a/src/theory/arith/inference_manager.cpp +++ b/src/theory/arith/inference_manager.cpp @@ -29,7 +29,7 @@ InferenceManager::InferenceManager(TheoryArith& ta, ProofNodeManager* pnm) : InferenceManagerBuffered(ta, astate, pnm, "theory::arith::"), // currently must track propagated literals if using the equality solver - d_trackPropLits(options::arithEqSolver()), + d_trackPropLits(astate.options().arith.arithEqSolver), d_propLits(astate.getSatContext()) { } @@ -127,7 +127,7 @@ bool InferenceManager::cacheLemma(TNode lem, LemmaProperty p) bool InferenceManager::isEntailedFalse(const SimpleTheoryLemma& lem) { - if (options::nlExtEntailConflicts()) + if (d_theoryState.options().arith.nlExtEntailConflicts) { Node ch_lemma = lem.d_node.negate(); ch_lemma = Rewriter::rewrite(ch_lemma); diff --git a/src/theory/arith/nl/cad/cdcac.cpp b/src/theory/arith/nl/cad/cdcac.cpp index 57010d1a1..9b37a135f 100644 --- a/src/theory/arith/nl/cad/cdcac.cpp +++ b/src/theory/arith/nl/cad/cdcac.cpp @@ -41,14 +41,13 @@ namespace arith { namespace nl { namespace cad { -CDCAC::CDCAC(context::Context* ctx, - ProofNodeManager* pnm, - const std::vector& ordering) - : d_variableOrdering(ordering) +CDCAC::CDCAC(Env& env, const std::vector& ordering) + : d_env(env), d_variableOrdering(ordering) { - if (pnm != nullptr) + if (d_env.isTheoryProofProducing()) { - d_proof.reset(new CADProofGenerator(ctx, pnm)); + d_proof.reset( + new CADProofGenerator(d_env.getContext(), d_env.getProofNodeManager())); } } @@ -77,7 +76,7 @@ void CDCAC::computeVariableOrdering() void CDCAC::retrieveInitialAssignment(NlModel& model, const Node& ran_variable) { - if (!options::nlCadUseInitial()) return; + if (!d_env.getOptions().arith.nlCadUseInitial) return; d_initialAssignment.clear(); Trace("cdcac") << "Retrieving initial assignment:" << std::endl; for (const auto& var : d_variableOrdering) @@ -103,7 +102,8 @@ std::vector CDCAC::getUnsatIntervals(std::size_t cur_variable) { std::vector res; LazardEvaluation le; - if (options::nlCadLifting() == options::NlCadLiftingMode::LAZARD) + if (d_env.getOptions().arith.nlCadLifting + == options::NlCadLiftingMode::LAZARD) { for (size_t vid = 0; vid < cur_variable; ++vid) { @@ -127,7 +127,8 @@ std::vector CDCAC::getUnsatIntervals(std::size_t cur_variable) Trace("cdcac") << "Infeasible intervals for " << p << " " << sc << " 0 over " << d_assignment << std::endl; std::vector intervals; - if (options::nlCadLifting() == options::NlCadLiftingMode::LAZARD) + if (d_env.getOptions().arith.nlCadLifting + == options::NlCadLiftingMode::LAZARD) { intervals = le.infeasibleRegions(p, sc); if (Trace.isOn("cdcac")) @@ -171,7 +172,8 @@ bool CDCAC::sampleOutsideWithInitial(const std::vector& infeasible, poly::Value& sample, std::size_t cur_variable) { - if (options::nlCadUseInitial() && cur_variable < d_initialAssignment.size()) + if (d_env.getOptions().arith.nlCadUseInitial + && cur_variable < d_initialAssignment.size()) { const poly::Value& suggested = d_initialAssignment[cur_variable]; for (const auto& i : infeasible) @@ -305,7 +307,7 @@ PolyVector CDCAC::requiredCoefficients(const poly::Polynomial& p) << requiredCoefficientsOriginal(p, d_assignment) << std::endl; } - switch (options::nlCadProjection()) + switch (d_env.getOptions().arith.nlCadProjection) { case options::NlCadProjectionMode::MCCALLUM: return requiredCoefficientsOriginal(p, d_assignment); diff --git a/src/theory/arith/nl/cad/cdcac.h b/src/theory/arith/nl/cad/cdcac.h index a75528953..b504998d8 100644 --- a/src/theory/arith/nl/cad/cdcac.h +++ b/src/theory/arith/nl/cad/cdcac.h @@ -25,6 +25,7 @@ #include +#include "smt/env.h" #include "theory/arith/nl/cad/cdcac_utils.h" #include "theory/arith/nl/cad/constraints.h" #include "theory/arith/nl/cad/proof_generator.h" @@ -47,9 +48,7 @@ class CDCAC { public: /** Initialize this method with the given variable ordering. */ - CDCAC(context::Context* ctx, - ProofNodeManager* pnm, - const std::vector& ordering = {}); + CDCAC(Env& env, const std::vector& ordering = {}); /** Reset this instance. */ void reset(); @@ -185,6 +184,9 @@ class CDCAC */ void pruneRedundantIntervals(std::vector& 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/cad_solver.cpp b/src/theory/arith/nl/cad_solver.cpp index 5d30d5db4..ebaeb9d61 100644 --- a/src/theory/arith/nl/cad_solver.cpp +++ b/src/theory/arith/nl/cad_solver.cpp @@ -27,13 +27,10 @@ namespace theory { namespace arith { namespace nl { -CadSolver::CadSolver(InferenceManager& im, - NlModel& model, - context::Context* ctx, - ProofNodeManager* pnm) +CadSolver::CadSolver(Env& env, InferenceManager& im, NlModel& model) : #ifdef CVC5_POLY_IMP - d_CAC(ctx, pnm), + d_CAC(env), #endif d_foundSatisfiability(false), d_im(im), @@ -44,9 +41,9 @@ CadSolver::CadSolver(InferenceManager& im, d_ranVariable = sm->mkDummySkolem( "__z", nm->realType(), "", NodeManager::SKOLEM_EXACT_NAME); #ifdef CVC5_POLY_IMP - ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr; - if (pc != nullptr) + if (env.isTheoryProofProducing()) { + ProofChecker* pc = env.getProofNodeManager()->getChecker(); // add checkers d_proofChecker.registerTo(pc); } diff --git a/src/theory/arith/nl/cad_solver.h b/src/theory/arith/nl/cad_solver.h index b9becec44..94bcb2907 100644 --- a/src/theory/arith/nl/cad_solver.h +++ b/src/theory/arith/nl/cad_solver.h @@ -43,10 +43,7 @@ class NlModel; class CadSolver { public: - CadSolver(InferenceManager& im, - NlModel& model, - context::Context* ctx, - ProofNodeManager* pnm); + CadSolver(Env& env, InferenceManager& im, NlModel& model); ~CadSolver(); /** diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp index 8200ff08e..eb5620a82 100644 --- a/src/theory/arith/nl/iand_solver.cpp +++ b/src/theory/arith/nl/iand_solver.cpp @@ -37,6 +37,7 @@ namespace nl { IAndSolver::IAndSolver(InferenceManager& im, ArithState& state, NlModel& model) : d_im(im), d_model(model), + d_astate(state), d_initRefine(state.getUserContext()) { NodeManager* nm = NodeManager::currentNM(); @@ -151,7 +152,7 @@ void IAndSolver::checkFullRefine() } // ************* additional lemma schemas go here - if (options::iandMode() == options::IandMode::SUM) + if (d_astate.options().smt.iandMode == options::IandMode::SUM) { Node lem = sumBasedLemma(i); // add lemmas based on sum mode Trace("iand-lemma") @@ -161,7 +162,7 @@ void IAndSolver::checkFullRefine() d_im.addPendingLemma( lem, InferenceId::ARITH_NL_IAND_SUM_REFINE, nullptr, true); } - else if (options::iandMode() == options::IandMode::BITWISE) + else if (d_astate.options().smt.iandMode == options::IandMode::BITWISE) { Node lem = bitwiseLemma(i); // check for violated bitwise axioms Trace("iand-lemma") @@ -244,7 +245,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 = options::BVAndIntegerGranularity(); + uint64_t granularity = d_astate.options().smt.BVAndIntegerGranularity; NodeManager* nm = NodeManager::currentNM(); Node lem = nm->mkNode( EQUAL, i, d_iandUtils.createSumNode(x, y, bvsize, granularity)); @@ -258,7 +259,7 @@ Node IAndSolver::bitwiseLemma(Node i) Node y = i[1]; unsigned bvsize = i.getOperator().getConst().d_size; - uint64_t granularity = options::BVAndIntegerGranularity(); + uint64_t granularity = d_astate.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 c80edbeb3..1be469259 100644 --- a/src/theory/arith/nl/iand_solver.h +++ b/src/theory/arith/nl/iand_solver.h @@ -85,6 +85,8 @@ class IAndSolver InferenceManager& d_im; /** Reference to the non-linear model object */ NlModel& d_model; + /** Reference to the arithmetic state */ + ArithState& d_astate; /** commonly used terms */ Node d_false; Node d_true; diff --git a/src/theory/arith/nl/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp index ed4a5318f..ca75a1a06 100644 --- a/src/theory/arith/nl/nl_model.cpp +++ b/src/theory/arith/nl/nl_model.cpp @@ -32,7 +32,7 @@ namespace theory { namespace arith { namespace nl { -NlModel::NlModel(context::Context* c) : d_used_approx(false) +NlModel::NlModel() : d_used_approx(false) { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); @@ -1263,7 +1263,8 @@ void NlModel::printModelValue(const char* c, Node n, unsigned prec) const void NlModel::getModelValueRepair( std::map& arithModel, std::map>& approximations, - std::map& witnesses) + std::map& witnesses, + bool witnessToValue) { Trace("nl-model") << "NlModel::getModelValueRepair:" << std::endl; // If we extended the model with entries x -> 0 for unconstrained values, @@ -1289,7 +1290,7 @@ void NlModel::getModelValueRepair( pred = nm->mkNode(AND, nm->mkNode(GEQ, v, l), nm->mkNode(GEQ, u, v)); Trace("nl-model") << v << " approximated as " << pred << std::endl; Node witness; - if (options::modelWitnessValue()) + if (witnessToValue) { // witness is the midpoint witness = nm->mkNode( diff --git a/src/theory/arith/nl/nl_model.h b/src/theory/arith/nl/nl_model.h index acf5ee7f5..526a93934 100644 --- a/src/theory/arith/nl/nl_model.h +++ b/src/theory/arith/nl/nl_model.h @@ -52,7 +52,7 @@ class NlModel friend class NonlinearExtension; public: - NlModel(context::Context* c); + NlModel(); ~NlModel(); /** * This method is called once at the beginning of a last call effort check, @@ -194,7 +194,8 @@ class NlModel void getModelValueRepair( std::map& arithModel, std::map>& approximations, - std::map& witnesses); + std::map& witnesses, + bool witnessToValue); private: /** The current model */ diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index df531fca7..c0ea3195a 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -19,6 +19,7 @@ #include "theory/arith/nl/nonlinear_extension.h" #include "options/arith_options.h" +#include "options/smt_options.h" #include "theory/arith/arith_state.h" #include "theory/arith/bound_inference.h" #include "theory/arith/inference_manager.h" @@ -48,7 +49,7 @@ NonlinearExtension::NonlinearExtension(TheoryArith& containing, containing.getSatContext(), containing.getUserContext(), d_im), - d_model(containing.getSatContext()), + d_model(), d_trSlv(d_im, d_model, d_astate.getEnv()), d_extState(d_im, d_model, d_astate.getEnv()), d_factoringSlv(&d_extState), @@ -56,10 +57,7 @@ NonlinearExtension::NonlinearExtension(TheoryArith& containing, d_monomialSlv(&d_extState), d_splitZeroSlv(&d_extState), d_tangentPlaneSlv(&d_extState), - d_cadSlv(d_im, - d_model, - state.getUserContext(), - d_astate.getEnv().getProofNodeManager()), + 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) @@ -121,11 +119,11 @@ void NonlinearExtension::getAssertions(std::vector& assertions) { Trace("nl-ext-assert-debug") << "Getting assertions..." << std::endl; bool useRelevance = false; - if (options::nlRlvMode() == options::NlRlvMode::INTERLEAVE) + if (options().arith.nlRlvMode == options::NlRlvMode::INTERLEAVE) { useRelevance = (d_checkCounter % 2); } - else if (options::nlRlvMode() == options::NlRlvMode::ALWAYS) + else if (options().arith.nlRlvMode == options::NlRlvMode::ALWAYS) { useRelevance = true; } @@ -228,7 +226,7 @@ bool NonlinearExtension::checkModel(const std::vector& assertions) // relevance here, since we may have discarded literals that are relevant // that are entailed based on the techniques in getAssertions. std::vector passertions = assertions; - if (options::nlExt() == options::NlExtMode::FULL) + if (options().arith.nlExt == options::NlExtMode::FULL) { // preprocess the assertions with the trancendental solver if (!d_trSlv.preprocessAssertionsCheckModel(passertions)) @@ -236,7 +234,7 @@ bool NonlinearExtension::checkModel(const std::vector& assertions) return false; } } - if (options::nlCad()) + if (options().arith.nlCad) { d_cadSlv.constructModelIfAvailable(passertions); } @@ -260,7 +258,7 @@ void NonlinearExtension::check(Theory::Effort e) if (e == Theory::EFFORT_FULL) { d_needsLastCall = true; - if (options::nlExtRewrites()) + if (options().arith.nlExtRewrites) { std::vector nred; if (!d_extTheory.doInferences(0, nred)) @@ -484,8 +482,8 @@ Result::Sat NonlinearExtension::modelBasedRefinement(const std::set& termS } // we are incomplete - if (options::nlExt() == options::NlExtMode::FULL - && options::nlExtIncPrecision() && d_model.usedApproximate()) + if (options().arith.nlExt == options::NlExtMode::FULL + && options().arith.nlExtIncPrecision && d_model.usedApproximate()) { d_trSlv.incrementTaylorDegree(); needsRecheck = true; @@ -529,7 +527,10 @@ void NonlinearExtension::interceptModel(std::map& arithModel, d_approximations.clear(); d_witnesses.clear(); // modify the model values - d_model.getModelValueRepair(arithModel, d_approximations, d_witnesses); + d_model.getModelValueRepair(arithModel, + d_approximations, + d_witnesses, + options().smt.modelWitnessValue); } } @@ -554,7 +555,7 @@ void NonlinearExtension::runStrategy(Theory::Effort effort, } if (!d_strategy.isStrategyInit()) { - d_strategy.initializeStrategy(); + d_strategy.initializeStrategy(options()); } auto steps = d_strategy.getStrategy(); diff --git a/src/theory/arith/nl/strategy.cpp b/src/theory/arith/nl/strategy.cpp index f20cf4221..b33e45129 100644 --- a/src/theory/arith/nl/strategy.cpp +++ b/src/theory/arith/nl/strategy.cpp @@ -105,22 +105,22 @@ bool StepGenerator::hasNext() const { return d_next < d_steps.size(); } InferStep StepGenerator::next() { return d_steps[d_next++]; } bool Strategy::isStrategyInit() const { return !d_interleaving.empty(); } -void Strategy::initializeStrategy() +void Strategy::initializeStrategy(const Options& options) { StepSequence one; - if (options::nlICP()) + if (options.arith.nlICP) { one << InferStep::ICP << InferStep::BREAK; } - if (options::nlExt() == options::NlExtMode::FULL - || options::nlExt() == options::NlExtMode::LIGHT) + if (options.arith.nlExt == options::NlExtMode::FULL + || options.arith.nlExt == options::NlExtMode::LIGHT) { one << InferStep::NL_INIT << InferStep::BREAK; } - if (options::nlExt() == options::NlExtMode::FULL) + if (options.arith.nlExt == options::NlExtMode::FULL) { one << InferStep::TRANS_INIT << InferStep::BREAK; - if (options::nlExtSplitZero()) + if (options.arith.nlExtSplitZero) { one << InferStep::NL_SPLIT_ZERO << InferStep::BREAK; } @@ -130,39 +130,39 @@ void Strategy::initializeStrategy() one << InferStep::IAND_INITIAL << InferStep::BREAK; one << InferStep::POW2_INIT; one << InferStep::POW2_INITIAL << InferStep::BREAK; - if (options::nlExt() == options::NlExtMode::FULL - || options::nlExt() == options::NlExtMode::LIGHT) + if (options.arith.nlExt == options::NlExtMode::FULL + || options.arith.nlExt == options::NlExtMode::LIGHT) { one << InferStep::NL_MONOMIAL_SIGN << InferStep::BREAK; one << InferStep::NL_MONOMIAL_MAGNITUDE0 << InferStep::BREAK; } - if (options::nlExt() == options::NlExtMode::FULL) + if (options.arith.nlExt == options::NlExtMode::FULL) { one << InferStep::TRANS_MONOTONIC << InferStep::BREAK; one << InferStep::NL_MONOMIAL_MAGNITUDE1 << InferStep::BREAK; one << InferStep::NL_MONOMIAL_MAGNITUDE2 << InferStep::BREAK; one << InferStep::NL_MONOMIAL_INFER_BOUNDS; - if (options::nlExtTangentPlanes() - && options::nlExtTangentPlanesInterleave()) + if (options.arith.nlExtTangentPlanes + && options.arith.nlExtTangentPlanesInterleave) { one << InferStep::NL_TANGENT_PLANES; } one << InferStep::BREAK; one << InferStep::FLUSH_WAITING_LEMMAS << InferStep::BREAK; - if (options::nlExtFactor()) + if (options.arith.nlExtFactor) { one << InferStep::NL_FACTORING << InferStep::BREAK; } - if (options::nlExtResBound()) + if (options.arith.nlExtResBound) { one << InferStep::NL_MONOMIAL_INFER_BOUNDS << InferStep::BREAK; } - if (options::nlExtTangentPlanes() - && !options::nlExtTangentPlanesInterleave()) + if (options.arith.nlExtTangentPlanes + && !options.arith.nlExtTangentPlanesInterleave) { one << InferStep::NL_TANGENT_PLANES_WAITING; } - if (options::nlExtTfTangentPlanes()) + if (options.arith.nlExtTfTangentPlanes) { one << InferStep::TRANS_TANGENT_PLANES; } @@ -170,11 +170,11 @@ void Strategy::initializeStrategy() } one << InferStep::IAND_FULL << InferStep::BREAK; one << InferStep::POW2_FULL << InferStep::BREAK; - if (options::nlCad()) + if (options.arith.nlCad) { one << InferStep::CAD_INIT; } - if (options::nlCad()) + if (options.arith.nlCad) { one << InferStep::CAD_FULL << InferStep::BREAK; } diff --git a/src/theory/arith/nl/strategy.h b/src/theory/arith/nl/strategy.h index e2fc6c1c6..d50108851 100644 --- a/src/theory/arith/nl/strategy.h +++ b/src/theory/arith/nl/strategy.h @@ -19,6 +19,8 @@ #include #include +#include "options/options.h" + namespace cvc5 { namespace theory { namespace arith { @@ -170,7 +172,7 @@ class Strategy /** Is this strategy initialized? */ bool isStrategyInit() const; /** Initialize this strategy */ - void initializeStrategy(); + void initializeStrategy(const Options& options); /** Retrieve the strategy for the given effort e */ StepGenerator getStrategy(); diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index aabf017a8..cb3f21da0 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -56,7 +56,7 @@ TheoryArith::TheoryArith(Env& env, OutputChannel& out, Valuation valuation) d_theoryState = &d_astate; d_inferManager = &d_im; - if (options::arithEqSolver()) + if (options().arith.arithEqSolver) { d_eqSolver.reset(new EqualitySolver(d_astate, d_im)); } diff --git a/test/unit/theory/theory_arith_cad_white.cpp b/test/unit/theory/theory_arith_cad_white.cpp index d7580a9cd..4c9b104c7 100644 --- a/test/unit/theory/theory_arith_cad_white.cpp +++ b/test/unit/theory/theory_arith_cad_white.cpp @@ -224,7 +224,9 @@ TEST_F(TestTheoryWhiteArithCAD, lazard_eval) TEST_F(TestTheoryWhiteArithCAD, test_cdcac_1) { - cad::CDCAC cac(nullptr, nullptr, {}); + Options opts; + Env env(NodeManager::currentNM(), &opts); + cad::CDCAC cac(env, {}); poly::Variable x = cac.getConstraints().varMapper()(make_real_variable("x")); poly::Variable y = cac.getConstraints().varMapper()(make_real_variable("y")); @@ -244,7 +246,9 @@ TEST_F(TestTheoryWhiteArithCAD, test_cdcac_1) TEST_F(TestTheoryWhiteArithCAD, test_cdcac_2) { - cad::CDCAC cac(nullptr, nullptr, {}); + Options opts; + Env env(NodeManager::currentNM(), &opts); + cad::CDCAC cac(env, {}); poly::Variable x = cac.getConstraints().varMapper()(make_real_variable("x")); poly::Variable y = cac.getConstraints().varMapper()(make_real_variable("y")); @@ -273,7 +277,9 @@ TEST_F(TestTheoryWhiteArithCAD, test_cdcac_2) TEST_F(TestTheoryWhiteArithCAD, test_cdcac_3) { - cad::CDCAC cac(nullptr, nullptr, {}); + Options opts; + Env env(NodeManager::currentNM(), &opts); + cad::CDCAC cac(env, {}); poly::Variable x = cac.getConstraints().varMapper()(make_real_variable("x")); poly::Variable y = cac.getConstraints().varMapper()(make_real_variable("y")); poly::Variable z = cac.getConstraints().varMapper()(make_real_variable("z")); @@ -294,7 +300,9 @@ TEST_F(TestTheoryWhiteArithCAD, test_cdcac_3) TEST_F(TestTheoryWhiteArithCAD, test_cdcac_4) { - cad::CDCAC cac(nullptr, nullptr, {}); + Options opts; + Env env(NodeManager::currentNM(), &opts); + cad::CDCAC cac(env, {}); poly::Variable x = cac.getConstraints().varMapper()(make_real_variable("x")); poly::Variable y = cac.getConstraints().varMapper()(make_real_variable("y")); poly::Variable z = cac.getConstraints().varMapper()(make_real_variable("z")); @@ -317,7 +325,9 @@ TEST_F(TestTheoryWhiteArithCAD, test_cdcac_4) void test_delta(const std::vector& a) { - cad::CDCAC cac(nullptr, nullptr, {}); + Options opts; + Env env(NodeManager::currentNM(), &opts); + cad::CDCAC cac(env, {}); cac.reset(); for (const Node& n : a) { -- 2.30.2