From 71f54fc41ee068707de387c2a6379b8996aaf744 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Wed, 30 Sep 2020 17:39:58 +0200 Subject: [PATCH] Add strategy for nonlinear extension (#5160) This PR adds a flexible strategy for the nonlinear extension that replaces the handwritten code in checkLastCall(). --- src/CMakeLists.txt | 2 + src/theory/arith/nl/nonlinear_extension.cpp | 298 ++++++-------------- src/theory/arith/nl/nonlinear_extension.h | 36 +-- src/theory/arith/nl/strategy.cpp | 174 ++++++++++++ src/theory/arith/nl/strategy.h | 178 ++++++++++++ 5 files changed, 464 insertions(+), 224 deletions(-) create mode 100644 src/theory/arith/nl/strategy.cpp create mode 100644 src/theory/arith/nl/strategy.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 30f5f80c1..c0f53e455 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -369,6 +369,8 @@ libcvc4_add_sources( theory/arith/nl/poly_conversion.h theory/arith/nl/stats.cpp theory/arith/nl/stats.h + theory/arith/nl/strategy.cpp + theory/arith/nl/strategy.h theory/arith/nl/transcendental_solver.cpp theory/arith/nl/transcendental_solver.h theory/arith/normal_form.cpp diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index a166a5609..8b7d8f4f5 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -369,212 +369,6 @@ bool NonlinearExtension::checkModel(const std::vector& assertions, return ret; } -void NonlinearExtension::checkLastCall(const std::vector& assertions, - const std::vector& false_asserts, - const std::vector& xts) -{ - ++(d_stats.d_checkRuns); - - if (Trace.isOn("nl-ext")) - { - for (const auto& a : assertions) - { - Trace("nl-ext") << "Input assertion: " << a << std::endl; - } - } - - if (options::nlICP()) - { - d_icpSlv.reset(assertions); - d_icpSlv.check(); - - if (d_im.hasUsed()) - { - Trace("nl-ext") << " ...finished with " - << d_im.numPendingLemmas() + d_im.numSentLemmas() - << " new lemmas from ICP." << std::endl; - return; - } - Trace("nl-ext") << "Done with ICP" << std::endl; - } - - if (options::nlExt()) - { - // initialize the non-linear solver - d_nlSlv.initLastCall(assertions, false_asserts, xts); - // initialize the trancendental function solver - d_trSlv.initLastCall(assertions, false_asserts, xts); - } - - // init last call with IAND - d_iandSlv.initLastCall(assertions, false_asserts, xts); - - if (d_im.hasUsed()) - { - std::size_t count = d_im.numPendingLemmas() + d_im.numSentLemmas(); - Trace("nl-ext") << " ...finished with " << count - << " new lemmas during registration." << std::endl; - return; - } - - //----------------------------------- possibly split on zero - if (options::nlExt() && options::nlExtSplitZero()) - { - Trace("nl-ext") << "Get zero split lemmas..." << std::endl; - d_nlSlv.checkSplitZero(); - if (d_im.hasUsed()) - { - Trace("nl-ext") << " ...finished with " << d_im.numPendingLemmas() << " new lemmas." - << std::endl; - return; - } - } - - //-----------------------------------initial lemmas for transcendental - if (options::nlExt()) - { - // functions - d_trSlv.checkTranscendentalInitialRefine(); - if (d_im.hasUsed()) - { - std::size_t count = d_im.numPendingLemmas() + d_im.numSentLemmas(); - Trace("nl-ext") << " ...finished with " << count << " new lemmas." - << std::endl; - return; - } - } - //-----------------------------------initial lemmas for iand - d_iandSlv.checkInitialRefine(); - if (d_im.hasUsed()) - { - Trace("nl-ext") << " ...finished with " << d_im.numPendingLemmas() << " new lemmas." - << std::endl; - return; - } - - // main calls to nlExt - if (options::nlExt()) - { - //---------------------------------lemmas based on sign (comparison to zero) - d_nlSlv.checkMonomialSign(); - if (d_im.hasUsed()) - { - Trace("nl-ext") << " ...finished with " << d_im.numPendingLemmas() << " new lemmas." - << std::endl; - return; - } - - //-----------------------------------monotonicity of transdental functions - d_trSlv.checkTranscendentalMonotonic(); - if (d_im.hasUsed()) - { - std::size_t count = d_im.numPendingLemmas() + d_im.numSentLemmas(); - Trace("nl-ext") << " ...finished with " << count << " new lemmas." - << std::endl; - return; - } - - //------------------------lemmas based on magnitude of non-zero monomials - for (unsigned c = 0; c < 3; c++) - { - // c is effort level - d_nlSlv.checkMonomialMagnitude(c); - if (d_im.hasUsed()) - { - Trace("nl-ext") << " ...finished with " << d_im.numPendingLemmas() - << " new lemmas." << std::endl; - return; - } - } - - //-----------------------------------inferred bounds lemmas - // e.g. x >= t => y*x >= y*t - d_nlSlv.checkMonomialInferBounds(assertions, false_asserts); - Trace("nl-ext") << "Bound lemmas : " << d_im.numPendingLemmas() << ", " << d_im.numWaitingLemmas() << std::endl; - // prioritize lemmas that do not introduce new monomials - if (options::nlExtTangentPlanes() - && options::nlExtTangentPlanesInterleave()) - { - d_nlSlv.checkTangentPlanes(false); - } - - if (d_im.hasUsed()) - { - Trace("nl-ext") << " ...finished with " << d_im.numPendingLemmas() << " new lemmas." - << std::endl; - return; - } - - // from inferred bound inferences : now do ones that introduce new terms - d_im.flushWaitingLemmas(); - if (d_im.hasUsed()) - { - Trace("nl-ext") << " ...finished with " << d_im.numPendingLemmas() - << " new (monomial-introducing) lemmas." << std::endl; - return; - } - - //------------------------------------factoring lemmas - // x*y + x*z >= t => exists k. k = y + z ^ x*k >= t - if (options::nlExtFactor()) - { - d_nlSlv.checkFactoring(assertions, false_asserts); - if (d_im.hasUsed()) - { - Trace("nl-ext") << " ...finished with " << d_im.numPendingLemmas() - << " new lemmas." << std::endl; - return; - } - } - - //------------------------------------resolution bound inferences - // e.g. ( y>=0 ^ s <= x*z ^ x*y <= t ) => y*s <= z*t - if (options::nlExtResBound()) - { - d_nlSlv.checkMonomialInferResBounds(); - if (d_im.hasUsed()) - { - Trace("nl-ext") << " ...finished with " << d_im.numPendingLemmas() - << " new lemmas." << std::endl; - return; - } - } - - //------------------------------------tangent planes - if (options::nlExtTangentPlanes() - && !options::nlExtTangentPlanesInterleave()) - { - d_nlSlv.checkTangentPlanes(true); - } - if (options::nlExtTfTangentPlanes()) - { - d_trSlv.checkTranscendentalTangentPlanes(); - } - } - if (options::nlCad()) - { - d_cadSlv.initLastCall(assertions); - d_cadSlv.checkFull(); - if (!d_im.hasUsed()) - { - Trace("nl-cad") << "nl-cad found SAT!" << std::endl; - } - else - { - // checkFull() only adds a single conflict - return; - } - } - // run the full refinement in the IAND solver - d_iandSlv.checkFullRefine(); - - Trace("nl-ext") << " ...finished with " << d_im.numWaitingLemmas() << " waiting lemmas." - << std::endl; - Trace("nl-ext") << " ...finished with " << d_im.numPendingLemmas() << " lemmas." - << std::endl; - return; -} - void NonlinearExtension::check(Theory::Effort e) { Trace("nl-ext") << std::endl; @@ -722,7 +516,7 @@ bool NonlinearExtension::modelBasedRefinement() if (!false_asserts.empty() || num_shared_wrong_value > 0) { complete_status = num_shared_wrong_value > 0 ? -1 : 0; - checkLastCall(assertions, false_asserts, xts); + runStrategy(Theory::Effort::EFFORT_FULL, assertions, false_asserts, xts); if (d_im.hasSentLemma() || d_im.hasPendingLemma()) { d_im.clearWaitingLemmas(); @@ -860,6 +654,96 @@ void NonlinearExtension::presolve() Trace("nl-ext") << "NonlinearExtension::presolve" << std::endl; } +void NonlinearExtension::runStrategy(Theory::Effort effort, + const std::vector& assertions, + const std::vector& false_asserts, + const std::vector& xts) +{ + ++(d_stats.d_checkRuns); + + if (Trace.isOn("nl-ext")) + { + for (const auto& a : assertions) + { + Trace("nl-ext") << "Input assertion: " << a << std::endl; + } + } + if (!d_strategy.isStrategyInit()) + { + d_strategy.initializeStrategy(); + } + + auto steps = d_strategy.getStrategy(); + bool stop = false; + while (!stop && steps.hasNext()) + { + InferStep step = steps.next(); + Trace("nl-ext") << "Step " << step << std::endl; + switch (step) + { + case InferStep::BREAK: stop = d_im.hasPendingLemma(); break; + case InferStep::FLUSH_WAITING_LEMMAS: d_im.flushWaitingLemmas(); break; + case InferStep::CAD_FULL: d_cadSlv.checkFull(); break; + case InferStep::CAD_INIT: d_cadSlv.initLastCall(assertions); break; + case InferStep::NL_FACTORING: + d_nlSlv.checkFactoring(assertions, false_asserts); + break; + case InferStep::IAND_INIT: + d_iandSlv.initLastCall(assertions, false_asserts, xts); + break; + case InferStep::IAND_FULL: d_iandSlv.checkFullRefine(); break; + case InferStep::IAND_INITIAL: d_iandSlv.checkInitialRefine(); break; + case InferStep::ICP: + d_icpSlv.reset(assertions); + d_icpSlv.check(); + break; + case InferStep::NL_INIT: + d_nlSlv.initLastCall(assertions, false_asserts, xts); + break; + case InferStep::NL_MONOMIAL_INFER_BOUNDS: + d_nlSlv.checkMonomialInferBounds(assertions, false_asserts); + break; + case InferStep::NL_MONOMIAL_MAGNITUDE0: + d_nlSlv.checkMonomialMagnitude(0); + break; + case InferStep::NL_MONOMIAL_MAGNITUDE1: + d_nlSlv.checkMonomialMagnitude(1); + break; + case InferStep::NL_MONOMIAL_MAGNITUDE2: + d_nlSlv.checkMonomialMagnitude(2); + break; + case InferStep::NL_MONOMIAL_SIGN: d_nlSlv.checkMonomialSign(); break; + case InferStep::NL_RESOLUTION_BOUNDS: + d_nlSlv.checkMonomialInferResBounds(); + break; + case InferStep::NL_SPLIT_ZERO: d_nlSlv.checkSplitZero(); break; + case InferStep::NL_TANGENT_PLANES: + d_nlSlv.checkTangentPlanes(false); + break; + case InferStep::NL_TANGENT_PLANES_WAITING: + d_nlSlv.checkTangentPlanes(true); + break; + case InferStep::TRANS_INIT: + d_trSlv.initLastCall(assertions, false_asserts, xts); + break; + case InferStep::TRANS_INITIAL: + d_trSlv.checkTranscendentalInitialRefine(); + break; + case InferStep::TRANS_MONOTONIC: + d_trSlv.checkTranscendentalMonotonic(); + break; + case InferStep::TRANS_TANGENT_PLANES: + d_trSlv.checkTranscendentalTangentPlanes(); + break; + } + } + + Trace("nl-ext") << " ...finished with " << d_im.numWaitingLemmas() + << " waiting lemmas." << std::endl; + Trace("nl-ext") << " ...finished with " << d_im.numPendingLemmas() + << " pending lemmas." << std::endl; +} + } // namespace nl } // namespace arith } // namespace theory diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h index f0e61435f..309caa519 100644 --- a/src/theory/arith/nl/nonlinear_extension.h +++ b/src/theory/arith/nl/nonlinear_extension.h @@ -35,6 +35,7 @@ #include "theory/arith/nl/nl_model.h" #include "theory/arith/nl/nl_solver.h" #include "theory/arith/nl/stats.h" +#include "theory/arith/nl/strategy.h" #include "theory/arith/nl/transcendental_solver.h" #include "theory/arith/theory_arith.h" #include "theory/ext_theory.h" @@ -148,23 +149,6 @@ class NonlinearExtension */ bool modelBasedRefinement(); - /** check last call - * - * Check assertions for consistency in the effort LAST_CALL with a subset of - * the assertions, false_asserts, that evaluate to false in the current model. - * - * xts : the list of (non-reduced) extended terms in the current context. - * - * This method adds lemmas to d_im directly. - * - * If the set lems is non-empty, then no further processing is - * necessary. The last call effort check should terminate and these - * lemmas should be sent. - */ - void checkLastCall(const std::vector& assertions, - const std::vector& false_asserts, - const std::vector& xts); - /** get assertions * * Let M be the set of assertions known by THEORY_ARITH. This function adds a @@ -224,6 +208,20 @@ class NonlinearExtension */ void sendLemmas(const std::vector& out); + /** run check strategy + * + * Check assertions for consistency in the effort LAST_CALL with a subset of + * the assertions, false_asserts, that evaluate to false in the current model. + * + * xts : the list of (non-reduced) extended terms in the current context. + * + * This method adds lemmas to d_im directly. + */ + void runStrategy(Theory::Effort effort, + const std::vector& assertions, + const std::vector& false_asserts, + const std::vector& xts); + /** commonly used terms */ Node d_zero; Node d_one; @@ -275,6 +273,10 @@ class NonlinearExtension * constraints involving integer and. */ IAndSolver d_iandSlv; + + /** The strategy for the nonlinear extension. */ + Strategy d_strategy; + /** * The approximations computed during collectModelInfo. For details, see * NlModel::getModelValueRepair. diff --git a/src/theory/arith/nl/strategy.cpp b/src/theory/arith/nl/strategy.cpp new file mode 100644 index 000000000..c209a1715 --- /dev/null +++ b/src/theory/arith/nl/strategy.cpp @@ -0,0 +1,174 @@ +/********************* */ +/*! \file strategy.cpp + ** \verbatim + ** Top contributors (to current version): + ** Gereon Kremer + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of non-linear solver + **/ + +#include "theory/arith/nl/strategy.h" + +#include "base/check.h" +#include "options/arith_options.h" + +namespace CVC4 { +namespace theory { +namespace arith { +namespace nl { + +std::ostream& operator<<(std::ostream& os, InferStep step) +{ + switch (step) + { + case InferStep::BREAK: return os << "BREAK"; + case InferStep::FLUSH_WAITING_LEMMAS: return os << "FLUSH_WAITING_LEMMAS"; + case InferStep::CAD_INIT: return os << "CAD_INIT"; + case InferStep::CAD_FULL: return os << "CAD_FULL"; + case InferStep::NL_FACTORING: return os << "NL_FACTORING"; + case InferStep::IAND_INIT: return os << "IAND_INIT"; + case InferStep::IAND_FULL: return os << "IAND_FULL"; + case InferStep::IAND_INITIAL: return os << "IAND_INITIAL"; + case InferStep::ICP: return os << "ICP"; + case InferStep::NL_INIT: return os << "NL_INIT"; + case InferStep::NL_MONOMIAL_INFER_BOUNDS: + return os << "NL_MONOMIAL_INFER_BOUNDS"; + case InferStep::NL_MONOMIAL_MAGNITUDE0: + return os << "NL_MONOMIAL_MAGNITUDE0"; + case InferStep::NL_MONOMIAL_MAGNITUDE1: + return os << "NL_MONOMIAL_MAGNITUDE1"; + case InferStep::NL_MONOMIAL_MAGNITUDE2: + return os << "NL_MONOMIAL_MAGNITUDE2"; + case InferStep::NL_MONOMIAL_SIGN: return os << "NL_MONOMIAL_SIGN"; + case InferStep::NL_RESOLUTION_BOUNDS: return os << "NL_RESOLUTION_BOUNDS"; + case InferStep::NL_SPLIT_ZERO: return os << "NL_SPLIT_ZERO"; + case InferStep::NL_TANGENT_PLANES: return os << "NL_TANGENT_PLANES"; + case InferStep::NL_TANGENT_PLANES_WAITING: + return os << "NL_TANGENT_PLANES_WAITING"; + case InferStep::TRANS_INIT: return os << "TRANS_INIT"; + case InferStep::TRANS_INITIAL: return os << "TRANS_INITIAL"; + case InferStep::TRANS_MONOTONIC: return os << "TRANS_MONOTONIC"; + case InferStep::TRANS_TANGENT_PLANES: return os << "TRANS_TANGENT_PLANES"; + default: Unreachable(); return os << "UNKNOWN_STEP"; + } +} + +namespace { +/** Puts a new InferStep into a StepSequence */ +inline StepSequence& operator<<(StepSequence& steps, InferStep s) +{ + steps.emplace_back(s); + return steps; +} +} // namespace + +void Interleaving::add(const StepSequence& ss, std::size_t constant) +{ + d_branches.emplace_back(Branch{ss, constant}); + d_size += constant; +} +void Interleaving::resetCounter() { d_counter = 0; } + +const StepSequence& Interleaving::get() +{ + Assert(!d_branches.empty()) + << "Can not get next sequence from an empty interleaving."; + std::size_t cnt = d_counter; + // Increase the counter + d_counter = (d_counter + 1) % d_size; + for (const auto& branch : d_branches) + { + if (cnt < branch.d_interleavingConstant) + { + // This is the current branch + return branch.d_steps; + } + cnt -= branch.d_interleavingConstant; + } + Assert(false) << "Something went wrong."; + return d_branches[0].d_steps; +} +bool Interleaving::empty() const { return d_branches.empty(); } + +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() +{ + StepSequence one; + if (options::nlICP()) + { + one << InferStep::ICP << InferStep::BREAK; + } + if (options::nlExt()) + { + one << InferStep::NL_INIT << InferStep::TRANS_INIT << InferStep::BREAK; + if (options::nlExtSplitZero()) + { + one << InferStep::NL_SPLIT_ZERO << InferStep::BREAK; + } + one << InferStep::TRANS_INITIAL << InferStep::BREAK; + } + one << InferStep::IAND_INIT; + one << InferStep::IAND_INITIAL << InferStep::BREAK; + if (options::nlExt()) + { + one << InferStep::NL_MONOMIAL_SIGN << InferStep::BREAK; + one << InferStep::TRANS_MONOTONIC << InferStep::BREAK; + one << InferStep::NL_MONOMIAL_MAGNITUDE0 << 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()) + { + one << InferStep::NL_TANGENT_PLANES; + } + one << InferStep::BREAK; + one << InferStep::FLUSH_WAITING_LEMMAS << InferStep::BREAK; + if (options::nlExtFactor()) + { + one << InferStep::NL_FACTORING << InferStep::BREAK; + } + if (options::nlExtResBound()) + { + one << InferStep::NL_MONOMIAL_INFER_BOUNDS << InferStep::BREAK; + } + if (options::nlExtTangentPlanes() + && !options::nlExtTangentPlanesInterleave()) + { + one << InferStep::NL_TANGENT_PLANES_WAITING; + } + if (options::nlExtTfTangentPlanes()) + { + one << InferStep::TRANS_TANGENT_PLANES; + } + one << InferStep::BREAK; + } + one << InferStep::IAND_FULL << InferStep::BREAK; + if (options::nlCad()) + { + one << InferStep::CAD_INIT; + } + if (options::nlCad()) + { + one << InferStep::CAD_FULL << InferStep::BREAK; + } + + d_interleaving.add(one); +} +StepGenerator Strategy::getStrategy() +{ + return StepGenerator(d_interleaving.get()); +} + +} // namespace nl +} // namespace arith +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/arith/nl/strategy.h b/src/theory/arith/nl/strategy.h new file mode 100644 index 000000000..d7604f501 --- /dev/null +++ b/src/theory/arith/nl/strategy.h @@ -0,0 +1,178 @@ +/********************* */ +/*! \file strategy.h + ** \verbatim + ** Top contributors (to current version): + ** Gereon Kremer + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Strategies for the nonlinear extension + **/ + +#ifndef CVC4__THEORY__ARITH__NL__STRATEGY_H +#define CVC4__THEORY__ARITH__NL__STRATEGY_H + +#include +#include + +namespace CVC4 { +namespace theory { +namespace arith { +namespace nl { + +/** The possible inference steps for the nonlinear extension */ +enum class InferStep +{ + /** Break if any lemma is pending */ + BREAK, + /** Flush waiting lemmas to be pending */ + FLUSH_WAITING_LEMMAS, + + /** Initialize the CAD solver */ + CAD_INIT, + /** A full CAD check */ + CAD_FULL, + + /** Initialize the IAND solver */ + IAND_INIT, + /** A full IAND check */ + IAND_FULL, + /** An initial IAND check */ + IAND_INITIAL, + + /** An ICP check */ + ICP, + + /** Initialize the NL solver */ + NL_INIT, + /** Nl factoring lemmas */ + NL_FACTORING, + /** Nl lemmas for monomial bound inference */ + NL_MONOMIAL_INFER_BOUNDS, + /** Nl lemmas for monomial magnitudes (class 0) */ + NL_MONOMIAL_MAGNITUDE0, + /** Nl lemmas for monomial magnitudes (class 1) */ + NL_MONOMIAL_MAGNITUDE1, + /** Nl lemmas for monomial magnitudes (class 2) */ + NL_MONOMIAL_MAGNITUDE2, + /** Nl lemmas for monomial signs */ + NL_MONOMIAL_SIGN, + /** Nl lemmas for resolution bounds */ + NL_RESOLUTION_BOUNDS, + /** Nl splitting at zero */ + NL_SPLIT_ZERO, + /** Nl tangent plane lemmas */ + NL_TANGENT_PLANES, + /** Nl tangent plane lemmas as waiting lemmas */ + NL_TANGENT_PLANES_WAITING, + + /** Initialize the transcendental solver */ + TRANS_INIT, + /** Initial transcendental lemmas */ + TRANS_INITIAL, + /** Monotonicity lemmas from transcendental solver */ + TRANS_MONOTONIC, + /** Tangent planes from transcendental solver */ + TRANS_TANGENT_PLANES, +}; + +/** Streaming operator for InferStep */ +std::ostream& operator<<(std::ostream& os, InferStep step); + +/** A sequence of steps */ +using StepSequence = std::vector; + +/** + * Stores an interleaving of multiple StepSequences. + * + * Every Branch of the interleaving holds a StepSequence s_i and a constant c_i. + * Once initialized, the interleaving may be asked repeatedly for a + * StepSequence. Repeated calls cycle through the branches, but will return + * every branch repeatedly as specified by its constant. + * + * Let for example [(s_1, 1), (s_2, 2), (s_3, 1)], then the sequence returned by + * get() would be: s_1, s_2, s_2, s_3, s_1, s_2, s_2, s_3, ... + */ +class Interleaving +{ + public: + /** Add a new branch to this interleaving */ + void add(const StepSequence& ss, std::size_t constant = 1); + /** + * Reset the counter to start from the first branch for the next get() call + */ + void resetCounter(); + /** Retrieve the next branch */ + const StepSequence& get(); + /** Check whether this interleaving is empty */ + bool empty() const; + + private: + /** Represents a single branch in an interleaving */ + struct Branch + { + StepSequence d_steps; + std::size_t d_interleavingConstant; + }; + /** The current counter of get() calls */ + std::size_t d_counter = 0; + /** The overall size of interleaving (considering constants) */ + std::size_t d_size = 0; + /** The branches */ + std::vector d_branches; +}; + +/** + * A small wrapper around a StepSequence. + * + * This class makes handling a StepSequence slightly more convenient. + * Also, it may help wrapping a more flexible strategy implementation in the + * future. + */ +class StepGenerator +{ + public: + StepGenerator(const StepSequence& ss) : d_steps(ss) {} + /** Check if there is another step */ + bool hasNext() const; + /** Get the next step */ + InferStep next(); + + private: + /** The StepSequence to process */ + const StepSequence& d_steps; + /** The next step */ + std::size_t d_next = 0; +}; + +/** + * A strategy for the nonlinear extension + * + * A strategy consists of multiple step sequences that are interleaved for every + * Theory::Effort. The initialization creates the strategy. Calling + * getStrategy() yields a StepGenerator that produces a sequence of InferSteps. + */ +class Strategy +{ + public: + /** Is this strategy initialized? */ + bool isStrategyInit() const; + /** Initialize this strategy */ + void initializeStrategy(); + /** Retrieve the strategy for the given effort e */ + StepGenerator getStrategy(); + + private: + /** The interleaving for this strategy */ + Interleaving d_interleaving; +}; + +} // namespace nl +} // namespace arith +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__ARITH__NL__STRATEGY_H */ -- 2.30.2