This PR adds a flexible strategy for the nonlinear extension that replaces the handwritten code in checkLastCall().
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
return ret;
}
-void NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
- const std::vector<Node>& false_asserts,
- const std::vector<Node>& 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;
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();
Trace("nl-ext") << "NonlinearExtension::presolve" << std::endl;
}
+void NonlinearExtension::runStrategy(Theory::Effort effort,
+ const std::vector<Node>& assertions,
+ const std::vector<Node>& false_asserts,
+ const std::vector<Node>& 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
#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"
*/
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<Node>& assertions,
- const std::vector<Node>& false_asserts,
- const std::vector<Node>& xts);
-
/** get assertions
*
* Let M be the set of assertions known by THEORY_ARITH. This function adds a
*/
void sendLemmas(const std::vector<NlLemma>& 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<Node>& assertions,
+ const std::vector<Node>& false_asserts,
+ const std::vector<Node>& xts);
+
/** commonly used terms */
Node d_zero;
Node d_one;
* 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.
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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 <map>
+#include <vector>
+
+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<InferStep>;
+
+/**
+ * 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<Branch> 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 */
projects / cvc5.git / commitdiff