From 3c200e9a6475d7b0e802cc56afe0f86eda1559c4 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Thu, 19 Aug 2021 10:29:17 -0700 Subject: [PATCH] Start using Options via Env in arithmetic (#7032) This PR refactors part of the arithmetic theory to use the options via the Env object. --- src/theory/arith/nl/ext/ext_state.cpp | 14 +- src/theory/arith/nl/ext/ext_state.h | 15 +- .../arith/nl/ext/monomial_bounds_check.cpp | 2 +- src/theory/arith/nl/ext/split_zero_check.cpp | 2 +- src/theory/arith/nl/nonlinear_extension.cpp | 25 +- src/theory/arith/nl/nonlinear_extension.h | 10 +- .../transcendental/transcendental_solver.cpp | 7 +- .../nl/transcendental/transcendental_solver.h | 7 +- .../transcendental/transcendental_state.cpp | 14 +- .../nl/transcendental/transcendental_state.h | 15 +- src/theory/arith/theory_arith.cpp | 6 +- src/theory/arith/theory_arith_private.cpp | 247 +++++++++++------- src/theory/arith/theory_arith_private.h | 9 +- src/theory/theory.h | 5 + src/theory/theory_state.h | 2 + 15 files changed, 211 insertions(+), 169 deletions(-) diff --git a/src/theory/arith/nl/ext/ext_state.cpp b/src/theory/arith/nl/ext/ext_state.cpp index 7db6c266f..b196f9990 100644 --- a/src/theory/arith/nl/ext/ext_state.cpp +++ b/src/theory/arith/nl/ext/ext_state.cpp @@ -30,20 +30,18 @@ namespace theory { namespace arith { namespace nl { -ExtState::ExtState(InferenceManager& im, - NlModel& model, - ProofNodeManager* pnm, - context::UserContext* c) - : d_im(im), d_model(model), d_pnm(pnm), d_ctx(c) +ExtState::ExtState(InferenceManager& im, NlModel& model, Env& env) + : d_im(im), d_model(model), d_env(env) { d_false = NodeManager::currentNM()->mkConst(false); d_true = NodeManager::currentNM()->mkConst(true); d_zero = NodeManager::currentNM()->mkConst(Rational(0)); d_one = NodeManager::currentNM()->mkConst(Rational(1)); d_neg_one = NodeManager::currentNM()->mkConst(Rational(-1)); - if (d_pnm != nullptr) + if (d_env.isTheoryProofProducing()) { - d_proof.reset(new CDProofSet(d_pnm, d_ctx, "nl-ext")); + d_proof.reset(new CDProofSet( + d_env.getProofNodeManager(), d_env.getUserContext(), "nl-ext")); } } @@ -105,7 +103,7 @@ bool ExtState::isProofEnabled() const { return d_proof.get() != nullptr; } CDProof* ExtState::getProof() { Assert(isProofEnabled()); - return d_proof->allocateProof(d_ctx); + return d_proof->allocateProof(d_env.getUserContext()); } } // namespace nl diff --git a/src/theory/arith/nl/ext/ext_state.h b/src/theory/arith/nl/ext/ext_state.h index 7c2cc1b9b..ac00f6f87 100644 --- a/src/theory/arith/nl/ext/ext_state.h +++ b/src/theory/arith/nl/ext/ext_state.h @@ -20,6 +20,7 @@ #include "expr/node.h" #include "proof/proof_set.h" +#include "smt/env.h" #include "theory/arith/nl/ext/monomial.h" namespace cvc5 { @@ -37,10 +38,7 @@ class NlModel; struct ExtState { - ExtState(InferenceManager& im, - NlModel& model, - ProofNodeManager* pnm, - context::UserContext* c); + ExtState(InferenceManager& im, NlModel& model, Env& env); void init(const std::vector& xts); @@ -63,13 +61,8 @@ struct ExtState InferenceManager& d_im; /** Reference to the non-linear model object */ NlModel& d_model; - /** - * Pointer to the current proof node manager. nullptr, if proofs are - * disabled. - */ - ProofNodeManager* d_pnm; - /** The user context. */ - context::UserContext* d_ctx; + /** Reference to the environment */ + Env& d_env; /** * A CDProofSet that hands out CDProof objects for lemmas. */ diff --git a/src/theory/arith/nl/ext/monomial_bounds_check.cpp b/src/theory/arith/nl/ext/monomial_bounds_check.cpp index 0deb2c99d..31bc4c662 100644 --- a/src/theory/arith/nl/ext/monomial_bounds_check.cpp +++ b/src/theory/arith/nl/ext/monomial_bounds_check.cpp @@ -207,7 +207,7 @@ void MonomialBoundsCheck::checkBounds(const std::vector& asserts, } // compute if bound is not satisfied, and store what is required // for a possible refinement - if (options::nlExtTangentPlanes()) + if (d_data->d_env.getOptions().arith.nlExtTangentPlanes) { if (is_false_lit) { diff --git a/src/theory/arith/nl/ext/split_zero_check.cpp b/src/theory/arith/nl/ext/split_zero_check.cpp index 6d9faa356..dcd6398b5 100644 --- a/src/theory/arith/nl/ext/split_zero_check.cpp +++ b/src/theory/arith/nl/ext/split_zero_check.cpp @@ -29,7 +29,7 @@ namespace arith { namespace nl { SplitZeroCheck::SplitZeroCheck(ExtState* data) - : d_data(data), d_zero_split(d_data->d_ctx) + : d_data(data), d_zero_split(d_data->d_env.getUserContext()) { } diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index 785127db5..df531fca7 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -37,27 +37,29 @@ namespace arith { namespace nl { NonlinearExtension::NonlinearExtension(TheoryArith& containing, - ArithState& state, - eq::EqualityEngine* ee, - ProofNodeManager* pnm) + ArithState& state) : d_containing(containing), + d_astate(state), d_im(containing.getInferenceManager()), d_needsLastCall(false), d_checkCounter(0), - d_extTheoryCb(ee), + d_extTheoryCb(state.getEqualityEngine()), d_extTheory(d_extTheoryCb, containing.getSatContext(), containing.getUserContext(), d_im), d_model(containing.getSatContext()), - d_trSlv(d_im, d_model, pnm, containing.getUserContext()), - d_extState(d_im, d_model, pnm, containing.getUserContext()), + d_trSlv(d_im, d_model, d_astate.getEnv()), + d_extState(d_im, d_model, d_astate.getEnv()), d_factoringSlv(&d_extState), d_monomialBoundsSlv(&d_extState), d_monomialSlv(&d_extState), d_splitZeroSlv(&d_extState), d_tangentPlaneSlv(&d_extState), - d_cadSlv(d_im, d_model, state.getUserContext(), pnm), + d_cadSlv(d_im, + d_model, + state.getUserContext(), + d_astate.getEnv().getProofNodeManager()), d_icpSlv(d_im), d_iandSlv(d_im, state, d_model), d_pow2Slv(d_im, state, d_model) @@ -73,9 +75,9 @@ NonlinearExtension::NonlinearExtension(TheoryArith& containing, d_one = NodeManager::currentNM()->mkConst(Rational(1)); d_neg_one = NodeManager::currentNM()->mkConst(Rational(-1)); - ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr; - if (pc != nullptr) + if (d_astate.getEnv().isTheoryProofProducing()) { + ProofChecker* pc = d_astate.getEnv().getProofNodeManager()->getChecker(); d_proofChecker.registerTo(pc); } } @@ -94,6 +96,11 @@ void NonlinearExtension::processSideEffect(const NlLemma& se) d_trSlv.processSideEffect(se); } +const Options& NonlinearExtension::options() const +{ + return d_containing.options(); +} + void NonlinearExtension::computeRelevantAssertions( const std::vector& assertions, std::vector& keep) { diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h index aae19df6e..6cbbfcdac 100644 --- a/src/theory/arith/nl/nonlinear_extension.h +++ b/src/theory/arith/nl/nonlinear_extension.h @@ -84,10 +84,7 @@ class NonlinearExtension typedef context::CDHashSet NodeSet; public: - NonlinearExtension(TheoryArith& containing, - ArithState& state, - eq::EqualityEngine* ee, - ProofNodeManager* pnm); + NonlinearExtension(TheoryArith& containing, ArithState& state); ~NonlinearExtension(); /** * Does non-context dependent setup for a node connected to a theory. @@ -145,6 +142,9 @@ class NonlinearExtension /** Process side effect se */ void processSideEffect(const NlLemma& se); + /** Obtain options object */ + const Options& options() const; + private: /** Model-based refinement * @@ -223,6 +223,8 @@ class NonlinearExtension Node d_true; // The theory of arithmetic containing this extension. TheoryArith& d_containing; + /** A reference to the arithmetic state object */ + ArithState& d_astate; InferenceManager& d_im; /** The statistics class */ NlStats d_stats; diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.cpp b/src/theory/arith/nl/transcendental/transcendental_solver.cpp index 0d5e5ad04..c7bb14b3f 100644 --- a/src/theory/arith/nl/transcendental/transcendental_solver.cpp +++ b/src/theory/arith/nl/transcendental/transcendental_solver.cpp @@ -39,11 +39,10 @@ namespace transcendental { TranscendentalSolver::TranscendentalSolver(InferenceManager& im, NlModel& m, - ProofNodeManager* pnm, - context::UserContext* c) - : d_tstate(im, m, pnm, c), d_expSlv(&d_tstate), d_sineSlv(&d_tstate) + Env& env) + : d_tstate(im, m, env), d_expSlv(&d_tstate), d_sineSlv(&d_tstate) { - d_taylor_degree = options::nlExtTfTaylorDegree(); + d_taylor_degree = d_tstate.d_env.getOptions().arith.nlExtTfTaylorDegree; } TranscendentalSolver::~TranscendentalSolver() {} diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.h b/src/theory/arith/nl/transcendental/transcendental_solver.h index 54bad2c1d..b63ebf29d 100644 --- a/src/theory/arith/nl/transcendental/transcendental_solver.h +++ b/src/theory/arith/nl/transcendental/transcendental_solver.h @@ -50,10 +50,7 @@ namespace transcendental { class TranscendentalSolver { public: - TranscendentalSolver(InferenceManager& im, - NlModel& m, - ProofNodeManager* pnm, - context::UserContext* c); + TranscendentalSolver(InferenceManager& im, NlModel& m, Env& env); ~TranscendentalSolver(); /** init last call @@ -187,7 +184,7 @@ class TranscendentalSolver * initially to options::nlExtTfTaylorDegree() and may be incremented * if the option options::nlExtTfIncPrecision() is enabled. */ - unsigned d_taylor_degree; + uint64_t d_taylor_degree; /** Common state for transcendental solver */ transcendental::TranscendentalState d_tstate; diff --git a/src/theory/arith/nl/transcendental/transcendental_state.cpp b/src/theory/arith/nl/transcendental/transcendental_state.cpp index db20713f1..19a334729 100644 --- a/src/theory/arith/nl/transcendental/transcendental_state.cpp +++ b/src/theory/arith/nl/transcendental/transcendental_state.cpp @@ -30,20 +30,20 @@ namespace transcendental { TranscendentalState::TranscendentalState(InferenceManager& im, NlModel& model, - ProofNodeManager* pnm, - context::UserContext* c) - : d_im(im), d_model(model), d_pnm(pnm), d_ctx(c) + Env& env) + : d_im(im), d_model(model), d_env(env) { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); d_zero = NodeManager::currentNM()->mkConst(Rational(0)); d_one = NodeManager::currentNM()->mkConst(Rational(1)); d_neg_one = NodeManager::currentNM()->mkConst(Rational(-1)); - if (d_pnm != nullptr) + if (d_env.isTheoryProofProducing()) { - d_proof.reset(new CDProofSet(d_pnm, d_ctx, "nl-trans")); + d_proof.reset(new CDProofSet( + d_env.getProofNodeManager(), d_env.getUserContext(), "nl-trans")); d_proofChecker.reset(new TranscendentalProofRuleChecker()); - d_proofChecker->registerTo(pnm->getChecker()); + d_proofChecker->registerTo(d_env.getProofNodeManager()->getChecker()); } } @@ -55,7 +55,7 @@ bool TranscendentalState::isProofEnabled() const CDProof* TranscendentalState::getProof() { Assert(isProofEnabled()); - return d_proof->allocateProof(d_ctx); + return d_proof->allocateProof(d_env.getUserContext()); } void TranscendentalState::init(const std::vector& xts, diff --git a/src/theory/arith/nl/transcendental/transcendental_state.h b/src/theory/arith/nl/transcendental/transcendental_state.h index 56cbec79a..65215c83c 100644 --- a/src/theory/arith/nl/transcendental/transcendental_state.h +++ b/src/theory/arith/nl/transcendental/transcendental_state.h @@ -18,6 +18,7 @@ #include "expr/node.h" #include "proof/proof_set.h" +#include "smt/env.h" #include "theory/arith/nl/nl_lemma_utils.h" #include "theory/arith/nl/transcendental/proof_checker.h" #include "theory/arith/nl/transcendental/taylor_generator.h" @@ -61,10 +62,7 @@ inline std::ostream& operator<<(std::ostream& os, Convexity c) { */ struct TranscendentalState { - TranscendentalState(InferenceManager& im, - NlModel& model, - ProofNodeManager* pnm, - context::UserContext* c); + TranscendentalState(InferenceManager& im, NlModel& model, Env& env); /** * Checks whether proofs are enabled. @@ -170,15 +168,10 @@ struct TranscendentalState InferenceManager& d_im; /** Reference to the non-linear model object */ NlModel& d_model; + /** Reference to the environment */ + Env& d_env; /** Utility to compute taylor approximations */ TaylorGenerator d_taylor; - /** - * Pointer to the current proof node manager. nullptr, if proofs are - * disabled. - */ - ProofNodeManager* d_pnm; - /** The user context. */ - context::UserContext* d_ctx; /** * A CDProofSet that hands out CDProof objects for lemmas. */ diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 37069d8b8..aabf017a8 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -44,8 +44,7 @@ TheoryArith::TheoryArith(Env& env, OutputChannel& out, Valuation valuation) d_ppre(getSatContext(), d_pnm), d_bab(d_astate, d_im, d_ppre, d_pnm), d_eqSolver(nullptr), - d_internal(new TheoryArithPrivate( - *this, getSatContext(), getUserContext(), d_bab, d_pnm)), + d_internal(new TheoryArithPrivate(*this, env, d_bab)), d_nonlinearExtension(nullptr), d_opElim(d_pnm, getLogicInfo()), d_arithPreproc(d_astate, d_im, d_pnm, d_opElim), @@ -102,8 +101,7 @@ void TheoryArith::finishInit() const LogicInfo& logicInfo = getLogicInfo(); if (logicInfo.isTheoryEnabled(THEORY_ARITH) && !logicInfo.isLinear()) { - d_nonlinearExtension.reset( - new nl::NonlinearExtension(*this, d_astate, d_equalityEngine, d_pnm)); + d_nonlinearExtension.reset(new nl::NonlinearExtension(*this, d_astate)); } if (d_eqSolver != nullptr) { diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 3102dc7b8..ea2887c44 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -86,19 +86,19 @@ static Node toSumNode(const ArithVariables& vars, const DenseMap& sum) static bool complexityBelow(const DenseMap& row, uint32_t cap); TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, - context::Context* c, - context::UserContext* u, - BranchAndBound& bab, - ProofNodeManager* pnm) + Env& env, + BranchAndBound& bab) : d_containing(containing), + d_env(env), d_foundNl(false), d_rowTracking(), d_bab(bab), - d_pnm(pnm), + d_pnm(d_env.isTheoryProofProducing() ? d_env.getProofNodeManager() + : nullptr), d_checker(), - d_pfGen(new EagerProofGenerator(d_pnm, u)), - d_constraintDatabase(c, - u, + d_pfGen(new EagerProofGenerator(d_pnm, d_env.getUserContext())), + d_constraintDatabase(d_env.getContext(), + d_env.getUserContext(), d_partialModel, d_congruenceManager, RaiseConflict(*this), @@ -107,15 +107,15 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, d_qflraStatus(Result::SAT_UNKNOWN), d_unknownsInARow(0), d_hasDoneWorkSinceCut(false), - d_learner(u), - d_assertionsThatDoNotMatchTheirLiterals(c), + d_learner(d_env.getUserContext()), + d_assertionsThatDoNotMatchTheirLiterals(d_env.getContext()), d_nextIntegerCheckVar(0), - d_constantIntegerVariables(c), - d_diseqQueue(c, false), + d_constantIntegerVariables(d_env.getContext()), + d_diseqQueue(d_env.getContext(), false), d_currentPropagationList(), - d_learnedBounds(c), - d_preregisteredNodes(u), - d_partialModel(c, DeltaComputeCallback(*this)), + d_learnedBounds(d_env.getContext()), + d_preregisteredNodes(d_env.getUserContext()), + d_partialModel(d_env.getContext(), DeltaComputeCallback(*this)), d_errorSet( d_partialModel, TableauSizes(&d_tableau), BoundCountingLookup(*this)), d_tableau(), @@ -123,22 +123,23 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, d_tableau, d_rowTracking, BasicVarModelUpdateCallBack(*this)), - d_diosolver(c), + d_diosolver(d_env.getContext()), d_restartsCounter(0), d_tableauSizeHasBeenModified(false), d_tableauResetDensity(1.6), d_tableauResetPeriod(10), - d_conflicts(c), - d_blackBoxConflict(c, Node::null()), - d_blackBoxConflictPf(c, std::shared_ptr(nullptr)), - d_congruenceManager(c, - u, + d_conflicts(d_env.getContext()), + d_blackBoxConflict(d_env.getContext(), Node::null()), + d_blackBoxConflictPf(d_env.getContext(), + std::shared_ptr(nullptr)), + d_congruenceManager(d_env.getContext(), + d_env.getUserContext(), d_constraintDatabase, SetupLiteralCallBack(*this), d_partialModel, RaiseEqualityEngineConflict(*this), d_pnm), - d_cmEnabled(c, options::arithCongMan()), + d_cmEnabled(d_env.getContext(), options().arith.arithCongMan), d_dualSimplex( d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)), @@ -150,22 +151,22 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)), d_pass1SDP(NULL), d_otherSDP(NULL), - d_lastContextIntegerAttempted(c, -1), + d_lastContextIntegerAttempted(d_env.getContext(), -1), d_DELTA_ZERO(0), - d_approxCuts(c), + d_approxCuts(d_env.getContext()), d_fullCheckCounter(0), - d_cutCount(c, 0), - d_cutInContext(c), - d_likelyIntegerInfeasible(c, false), - d_guessedCoeffSet(c, false), + d_cutCount(d_env.getContext(), 0), + d_cutInContext(d_env.getContext()), + d_likelyIntegerInfeasible(d_env.getContext(), false), + d_guessedCoeffSet(d_env.getContext(), false), d_guessedCoeffs(), d_treeLog(NULL), d_replayVariables(), d_replayConstraints(), d_lhsTmp(), d_approxStats(NULL), - d_attemptSolveIntTurnedOff(u, 0), + d_attemptSolveIntTurnedOff(d_env.getUserContext(), 0), d_dioSolveResources(0), d_solveIntMaybeHelp(0u), d_solveIntAttempts(0u), @@ -509,13 +510,13 @@ bool TheoryArithPrivate::getDioCuttingResource(){ if(d_dioSolveResources > 0){ d_dioSolveResources--; if(d_dioSolveResources == 0){ - d_dioSolveResources = -options::rrTurns(); + d_dioSolveResources = -options().arith.rrTurns; } return true; }else{ d_dioSolveResources++; if(d_dioSolveResources >= 0){ - d_dioSolveResources = options::dioSolverTurns(); + d_dioSolveResources = options().arith.dioSolverTurns; } return false; } @@ -1047,7 +1048,7 @@ Theory::PPAssertStatus TheoryArithPrivate::ppAssert( // Add the substitution if not recursive Assert(elim == Rewriter::rewrite(elim)); - if (right.size() > options::ppAssertMaxSubSize()) + if (right.size() > options().arith.ppAssertMaxSubSize) { Debug("simplify") << "TheoryArithPrivate::solve(): did not substitute due to the " @@ -1882,7 +1883,10 @@ bool TheoryArithPrivate::attemptSolveInteger(Theory::Effort effortLevel, bool em if(d_qflraStatus == Result::UNSAT){ return false; } if(emmmittedLemmaOrSplit){ return false; } - if(!options::useApprox()){ return false; } + if (!options().arith.useApprox) + { + return false; + } if(!ApproximateSimplex::enabled()){ return false; } if(Theory::fullEffort(effortLevel)){ @@ -1902,8 +1906,10 @@ bool TheoryArithPrivate::attemptSolveInteger(Theory::Effort effortLevel, bool em } } - - if(!options::trySolveIntStandardEffort()){ return false; } + if (!options().arith.trySolveIntStandardEffort) + { + return false; + } if (d_lastContextIntegerAttempted <= (level >> 2)) { @@ -2352,7 +2358,7 @@ std::vector TheoryArithPrivate::replayLogRec(ApproximateSimplex if(ci->reconstructed() && ci->proven()){ const DenseMap& row = ci->getReconstruction().lhs; - reject = !complexityBelow(row, options::replayRejectCutSize()); + reject = !complexityBelow(row, options().arith.replayRejectCutSize); } } if(conflictQueueEmpty()){ @@ -2400,8 +2406,9 @@ std::vector TheoryArithPrivate::replayLogRec(ApproximateSimplex /* check if the system is feasible under with the cuts */ if(conflictQueueEmpty()){ - Assert(options::replayEarlyCloseDepths() >= 1); - if(!nl.isBranch() || depth % options::replayEarlyCloseDepths() == 0 ){ + Assert(options().arith.replayEarlyCloseDepths >= 1); + if (!nl.isBranch() || depth % options().arith.replayEarlyCloseDepths == 0) + { TimerStat::CodeTimer codeTimer(d_statistics.d_replaySimplexTimer); //test for linear feasibility d_partialModel.stopQueueingBoundCounts(); @@ -2515,8 +2522,8 @@ std::vector TheoryArithPrivate::replayLogRec(ApproximateSimplex resolveOutPropagated(res, propagated); Debug("approx::replayLogRec") << "replayLogRec() ending" << std::endl; - - if(options::replayFailureLemma()){ + if (options().arith.replayFailureLemma) + { // must be done inside the sat context to get things // propagated at this level if(res.empty() && nid == getTreeLog().getRootId()){ @@ -2659,7 +2666,8 @@ bool TheoryArithPrivate::replayLemmas(ApproximateSimplex* approx){ Assert(cut->proven()); const DenseMap& row = cut->getReconstruction().lhs; - if(!complexityBelow(row, options::lemmaRejectCutSize())){ + if (!complexityBelow(row, options().arith.lemmaRejectCutSize)) + { ++(d_statistics.d_cutsRejectedDuringLemmas); continue; } @@ -2746,7 +2754,7 @@ void TheoryArithPrivate::solveInteger(Theory::Effort effortLevel){ } // if integers are attempted, - Assert(options::useApprox()); + Assert(options().arith.useApprox); Assert(ApproximateSimplex::enabled()); int level = getSatContext()->getLevel(); @@ -2769,8 +2777,9 @@ void TheoryArithPrivate::solveInteger(Theory::Effort effortLevel){ approx->setOptCoeffs(d_guessedCoeffs); } static const int32_t depthForLikelyInfeasible = 10; - int maxDepthPass1 = d_likelyIntegerInfeasible ? - depthForLikelyInfeasible : options::maxApproxDepth(); + int maxDepthPass1 = d_likelyIntegerInfeasible + ? depthForLikelyInfeasible + : options().arith.maxApproxDepth; approx->setBranchingDepth(maxDepthPass1); approx->setBranchOnVariableLimit(100); LinResult relaxRes = approx->solveRelaxation(); @@ -2833,7 +2842,7 @@ void TheoryArithPrivate::solveInteger(Theory::Effort effortLevel){ } } if(!(anyConflict() || !d_approxCuts.empty())){ - turnOffApproxFor(options::replayNumericFailurePenalty()); + turnOffApproxFor(options().arith.replayNumericFailurePenalty); } break; case BranchesExhausted: @@ -2873,11 +2882,16 @@ void TheoryArithPrivate::solveInteger(Theory::Effort effortLevel){ SimplexDecisionProcedure& TheoryArithPrivate::selectSimplex(bool pass1){ if(pass1){ if(d_pass1SDP == NULL){ - if(options::useFC()){ + if (options().arith.useFC) + { d_pass1SDP = (SimplexDecisionProcedure*)(&d_fcSimplex); - }else if(options::useSOI()){ + } + else if (options().arith.useSOI) + { d_pass1SDP = (SimplexDecisionProcedure*)(&d_soiSimplex); - }else{ + } + else + { d_pass1SDP = (SimplexDecisionProcedure*)(&d_dualSimplex); } } @@ -2885,13 +2899,18 @@ SimplexDecisionProcedure& TheoryArithPrivate::selectSimplex(bool pass1){ return *d_pass1SDP; }else{ if(d_otherSDP == NULL){ - if(options::useFC()){ - d_otherSDP = (SimplexDecisionProcedure*)(&d_fcSimplex); - }else if(options::useSOI()){ - d_otherSDP = (SimplexDecisionProcedure*)(&d_soiSimplex); - }else{ - d_otherSDP = (SimplexDecisionProcedure*)(&d_soiSimplex); - } + if (options().arith.useFC) + { + d_otherSDP = (SimplexDecisionProcedure*)(&d_fcSimplex); + } + else if (options().arith.useSOI) + { + d_otherSDP = (SimplexDecisionProcedure*)(&d_soiSimplex); + } + else + { + d_otherSDP = (SimplexDecisionProcedure*)(&d_soiSimplex); + } } Assert(d_otherSDP != NULL); return *d_otherSDP; @@ -2912,8 +2931,8 @@ void TheoryArithPrivate::importSolution(const ApproximateSimplex::Solution& solu } if(d_qflraStatus != Result::UNSAT){ - static const int32_t pass2Limit = 20; - int16_t oldCap = options::arithStandardCheckVarOrderPivots(); + static const int64_t pass2Limit = 20; + int64_t oldCap = options().arith.arithStandardCheckVarOrderPivots; Options::current().arith.arithStandardCheckVarOrderPivots = pass2Limit; SimplexDecisionProcedure& simplex = selectSimplex(false); d_qflraStatus = simplex.findModel(false); @@ -2964,20 +2983,19 @@ bool TheoryArithPrivate::solveRealRelaxation(Theory::Effort effortLevel){ d_partialModel.processBoundsQueue(utcb); d_linEq.startTrackingBoundCounts(); - bool noPivotLimit = Theory::fullEffort(effortLevel) || - !options::restrictedPivots(); + bool noPivotLimit = + Theory::fullEffort(effortLevel) || !options().arith.restrictedPivots; SimplexDecisionProcedure& simplex = selectSimplex(true); - bool useApprox = options::useApprox() && ApproximateSimplex::enabled() && getSolveIntegerResource(); + bool useApprox = options().arith.useApprox && ApproximateSimplex::enabled() + && getSolveIntegerResource(); Debug("TheoryArithPrivate::solveRealRelaxation") - << "solveRealRelaxation() approx" - << " " << options::useApprox() - << " " << ApproximateSimplex::enabled() - << " " << useApprox - << " " << safeToCallApprox() - << endl; + << "solveRealRelaxation() approx" + << " " << options().arith.useApprox << " " + << ApproximateSimplex::enabled() << " " << useApprox << " " + << safeToCallApprox() << endl; bool noPivotLimitPass1 = noPivotLimit && !useApprox; d_qflraStatus = simplex.findModel(noPivotLimitPass1); @@ -3136,7 +3154,7 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel) if(anyConflict()){ d_qflraStatus = Result::UNSAT; - if (options::revertArithModels() && d_previousStatus == Result::SAT) + if (options().arith.revertArithModels && d_previousStatus == Result::SAT) { ++d_statistics.d_revertsOnConflicts; Debug("arith::bt") << "clearing here " @@ -3211,10 +3229,14 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel) if(Debug.isOn("arith::consistency")){ Assert(entireStateIsConsistent("sat comit")); } - if(useSimplex && options::collectPivots()){ - if(options::useFC()){ + if (useSimplex && options().arith.collectPivots) + { + if (options().arith.useFC) + { d_statistics.d_satPivots << d_fcSimplex.getPivots(); - }else{ + } + else + { d_statistics.d_satPivots << d_dualSimplex.getPivots(); } } @@ -3229,10 +3251,14 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel) d_partialModel.commitAssignmentChanges(); d_statistics.d_maxUnknownsInARow.maxAssign(d_unknownsInARow); - if(useSimplex && options::collectPivots()){ - if(options::useFC()){ + if (useSimplex && options().arith.collectPivots) + { + if (options().arith.useFC) + { d_statistics.d_unknownPivots << d_fcSimplex.getPivots(); - }else{ + } + else + { d_statistics.d_unknownPivots << d_dualSimplex.getPivots(); } } @@ -3255,10 +3281,14 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel) emmittedConflictOrSplit = true; Debug("arith::conflict") << "simplex conflict" << endl; - if(useSimplex && options::collectPivots()){ - if(options::useFC()){ + if (useSimplex && options().arith.collectPivots) + { + if (options().arith.useFC) + { d_statistics.d_unsatPivots << d_fcSimplex.getPivots(); - }else{ + } + else + { d_statistics.d_unsatPivots << d_dualSimplex.getPivots(); } } @@ -3268,8 +3298,8 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel) } d_statistics.d_avgUnknownsInARow << d_unknownsInARow; - size_t nPivots = - options::useFC() ? d_fcSimplex.getPivots() : d_dualSimplex.getPivots(); + size_t nPivots = options().arith.useFC ? d_fcSimplex.getPivots() + : d_dualSimplex.getPivots(); for (std::size_t i = 0; i < nPivots; ++i) { d_containing.d_out->spendResource( @@ -3298,9 +3328,9 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel) // This should be fine if sat or unknown if (!emmittedConflictOrSplit - && (options::arithPropagationMode() + && (options().arith.arithPropagationMode == options::ArithPropagationMode::UNATE_PROP - || options::arithPropagationMode() + || options().arith.arithPropagationMode == options::ArithPropagationMode::BOTH_PROP)) { TimerStat::CodeTimer codeTimer0(d_statistics.d_newPropTime); @@ -3383,7 +3413,8 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel) if(!emmittedConflictOrSplit && Theory::fullEffort(effortLevel) && !hasIntegerModel()){ Node possibleConflict = Node::null(); - if(!emmittedConflictOrSplit && options::arithDioSolver()){ + if (!emmittedConflictOrSplit && options().arith.arithDioSolver) + { possibleConflict = callDioSolver(); if(possibleConflict != Node::null()){ revertOutOfConflict(); @@ -3395,7 +3426,9 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel) } } - if(!emmittedConflictOrSplit && d_hasDoneWorkSinceCut && options::arithDioSolver()){ + if (!emmittedConflictOrSplit && d_hasDoneWorkSinceCut + && options().arith.arithDioSolver) + { if(getDioCuttingResource()){ TrustNode possibleLemma = dioCutting(); if(!possibleLemma.isNull()){ @@ -3425,7 +3458,8 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel) } } - if(options::maxCutsInContext() <= d_cutCount){ + if (options().arith.maxCutsInContext <= d_cutCount) + { if(d_diosolver.hasMoreDecompositionLemmas()){ while(d_diosolver.hasMoreDecompositionLemmas()){ Node decompositionLemma = d_diosolver.nextDecompositionLemma(); @@ -3497,7 +3531,8 @@ std::vector TheoryArithPrivate::cutAllBounded() const{ vector lemmas; ArithVar max = d_partialModel.getNumberOfVariables(); - if(options::doCutAllBounded() && max > 0){ + if (options().arith.doCutAllBounded && max > 0) + { for(ArithVar iter = 0; iter != max; ++iter){ //Do not include slack variables const DeltaRational& d = d_partialModel.getAssignment(iter); @@ -3645,15 +3680,18 @@ TrustNode TheoryArithPrivate::explain(TNode n) void TheoryArithPrivate::propagate(Theory::Effort e) { // This uses model values for safety. Disable for now. if (d_qflraStatus == Result::SAT - && (options::arithPropagationMode() + && (options().arith.arithPropagationMode == options::ArithPropagationMode::BOUND_INFERENCE_PROP - || options::arithPropagationMode() + || options().arith.arithPropagationMode == options::ArithPropagationMode::BOTH_PROP) && hasAnyUpdates()) { - if(options::newProp()){ + if (options().arith.newProp) + { propagateCandidatesNew(); - }else{ + } + else + { propagateCandidates(); } } @@ -4022,8 +4060,10 @@ void TheoryArithPrivate::presolve(){ } vector lemmas; - if(!options::incrementalSolving()) { - switch(options::arithUnateLemmaMode()){ + if (!options().base.incrementalSolving) + { + switch (options().arith.arithUnateLemmaMode) + { case options::ArithUnateLemmaMode::NO: break; case options::ArithUnateLemmaMode::INEQUALITY: d_constraintDatabase.outputUnateInequalityLemmas(lemmas); @@ -4035,7 +4075,7 @@ void TheoryArithPrivate::presolve(){ d_constraintDatabase.outputUnateInequalityLemmas(lemmas); d_constraintDatabase.outputUnateEqualityLemmas(lemmas); break; - default: Unhandled() << options::arithUnateLemmaMode(); + default: Unhandled() << options().arith.arithUnateLemmaMode; } } @@ -4183,10 +4223,14 @@ void TheoryArithPrivate::propagateCandidates(){ DenseSet::const_iterator end = d_updatedBounds.end(); for(; i != end; ++i){ ArithVar var = *i; - if(d_tableau.isBasic(var) && - d_tableau.basicRowLength(var) <= options::arithPropagateMaxLength()){ + if (d_tableau.isBasic(var) + && d_tableau.basicRowLength(var) + <= options().arith.arithPropagateMaxLength) + { d_candidateBasics.softAdd(var); - }else{ + } + else + { Tableau::ColIterator basicIter = d_tableau.colIterator(var); for(; !basicIter.atEnd(); ++basicIter){ const Tableau::Entry& entry = *basicIter; @@ -4194,7 +4238,9 @@ void TheoryArithPrivate::propagateCandidates(){ ArithVar rowVar = d_tableau.rowIndexToBasic(ridx); Assert(entry.getColVar() == var); Assert(d_tableau.isBasic(rowVar)); - if(d_tableau.getRowLength(ridx) <= options::arithPropagateMaxLength()){ + if (d_tableau.getRowLength(ridx) + <= options().arith.arithPropagateMaxLength) + { d_candidateBasics.softAdd(rowVar); } } @@ -4428,7 +4474,8 @@ bool TheoryArithPrivate::rowImplicationCanBeApplied(RowIndex ridx, bool rowUp, C // * coeffs[0] is for implied // * coeffs[i+1] is for explain[i] d_linEq.propagateRow(explain, ridx, rowUp, implied, coeffs); - if(d_tableau.getRowLength(ridx) <= options::arithPropAsLemmaLength()){ + if (d_tableau.getRowLength(ridx) <= options().arith.arithPropAsLemmaLength) + { if (Debug.isOn("arith::prop::pf")) { for (const auto & constraint : explain) { Assert(constraint->hasProof()); @@ -4493,7 +4540,9 @@ bool TheoryArithPrivate::rowImplicationCanBeApplied(RowIndex ridx, bool rowUp, C { outputLemma(clause, InferenceId::ARITH_ROW_IMPL); } - }else{ + } + else + { Assert(!implied->negationHasProof()); implied->impliedByFarkas(explain, coeffs, false); implied->tryToPropagate(); @@ -4521,9 +4570,9 @@ bool TheoryArithPrivate::propagateCandidateRow(RowIndex ridx){ Debug("arith::prop") << "propagateCandidateRow " << instance << " attempt " << rowLength << " " << hasCount << endl; - if (rowLength >= options::arithPropagateMaxLength() + if (rowLength >= options().arith.arithPropagateMaxLength && Random::getRandom().pickWithProb( - 1.0 - double(options::arithPropagateMaxLength()) / rowLength)) + 1.0 - double(options().arith.arithPropagateMaxLength) / rowLength)) { return false; } diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index 4afe121b9..0cdc031e1 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -88,6 +88,9 @@ private: static const uint32_t RESET_START = 2; TheoryArith& d_containing; + Env& d_env; + + const Options& options() const { return d_env.getOptions(); } /** * Whether we encountered non-linear arithmetic at any time during solving. @@ -423,11 +426,7 @@ private: DeltaRational getDeltaValue(TNode term) const /* throw(DeltaRationalException, ModelException) */; public: - TheoryArithPrivate(TheoryArith& containing, - context::Context* c, - context::UserContext* u, - BranchAndBound& bab, - ProofNodeManager* pnm); + TheoryArithPrivate(TheoryArith& containing, Env& env, BranchAndBound& bab); ~TheoryArithPrivate(); //--------------------------------- initialization diff --git a/src/theory/theory.h b/src/theory/theory.h index 7c76c7ee6..bde00b908 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -449,6 +449,11 @@ class Theory { */ Env& getEnv() const { return d_env; } + /** + * Shorthand to access the options object. + */ + const Options& options() const { return getEnv().getOptions(); } + /** * Get the SAT context associated to this Theory. */ diff --git a/src/theory/theory_state.h b/src/theory/theory_state.h index 58a66ef46..cc58347bf 100644 --- a/src/theory/theory_state.h +++ b/src/theory/theory_state.h @@ -47,6 +47,8 @@ class TheoryState 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; -- 2.30.2