From d4544c5484e85ae75387124c3826531474e15c26 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Fri, 17 Sep 2021 20:03:37 +0200 Subject: [PATCH] Minor cleanup related to EnvObj (#7206) This PR does a bit of cleanup in the nonlinear arithmetic code related to the usage of EnvObj. --- src/theory/arith/nl/cad/cdcac.cpp | 12 ++++++------ src/theory/arith/theory_arith_private.h | 2 -- 2 files changed, 6 insertions(+), 8 deletions(-) diff --git a/src/theory/arith/nl/cad/cdcac.cpp b/src/theory/arith/nl/cad/cdcac.cpp index 9b7678388..ecb62b554 100644 --- a/src/theory/arith/nl/cad/cdcac.cpp +++ b/src/theory/arith/nl/cad/cdcac.cpp @@ -47,7 +47,7 @@ CDCAC::CDCAC(Env& env, const std::vector& ordering) if (d_env.isTheoryProofProducing()) { d_proof.reset( - new CADProofGenerator(d_env.getContext(), d_env.getProofNodeManager())); + new CADProofGenerator(context(), d_env.getProofNodeManager())); } } @@ -76,7 +76,7 @@ void CDCAC::computeVariableOrdering() void CDCAC::retrieveInitialAssignment(NlModel& model, const Node& ran_variable) { - if (!d_env.getOptions().arith.nlCadUseInitial) return; + if (!options().arith.nlCadUseInitial) return; d_initialAssignment.clear(); Trace("cdcac") << "Retrieving initial assignment:" << std::endl; for (const auto& var : d_variableOrdering) @@ -102,7 +102,7 @@ std::vector CDCAC::getUnsatIntervals(std::size_t cur_variable) { std::vector res; LazardEvaluation le; - if (d_env.getOptions().arith.nlCadLifting + if (options().arith.nlCadLifting == options::NlCadLiftingMode::LAZARD) { for (size_t vid = 0; vid < cur_variable; ++vid) @@ -127,7 +127,7 @@ 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 (d_env.getOptions().arith.nlCadLifting + if (options().arith.nlCadLifting == options::NlCadLiftingMode::LAZARD) { intervals = le.infeasibleRegions(p, sc); @@ -172,7 +172,7 @@ bool CDCAC::sampleOutsideWithInitial(const std::vector& infeasible, poly::Value& sample, std::size_t cur_variable) { - if (d_env.getOptions().arith.nlCadUseInitial + if (options().arith.nlCadUseInitial && cur_variable < d_initialAssignment.size()) { const poly::Value& suggested = d_initialAssignment[cur_variable]; @@ -306,7 +306,7 @@ PolyVector CDCAC::requiredCoefficients(const poly::Polynomial& p) << requiredCoefficientsOriginal(p, d_assignment) << std::endl; } - switch (d_env.getOptions().arith.nlCadProjection) + switch (options().arith.nlCadProjection) { case options::NlCadProjectionMode::MCCALLUM: return requiredCoefficientsOriginal(p, d_assignment); diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index 221c0a781..fe941a7fb 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -89,8 +89,6 @@ class TheoryArithPrivate : protected EnvObj TheoryArith& d_containing; - const Options& options() const { return d_env.getOptions(); } - /** * Whether we encountered non-linear arithmetic at any time during solving. */ -- 2.30.2