Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arith/nl/strategy.h	Lines:	4	4	100.0 %
Date:	2021-09-04	Branches:	0	0	0.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Gereon Kremer
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 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.
 * ****************************************************************************
 *
 * Strategies for the nonlinear extension.
 */

#ifndef CVC5__THEORY__ARITH__NL__STRATEGY_H
#define CVC5__THEORY__ARITH__NL__STRATEGY_H

#include <iosfwd>
#include <vector>

#include "options/options.h"

namespace cvc5 {
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,

  /** Initialize the POW2 solver */
  POW2_INIT,
  /** A full POW2 check */
  POW2_FULL,
  /** An initial POW2 check */
  POW2_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(const Options& options);
  /** 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 cvc5

#endif /* CVC5__THEORY__ARITH__NL__STRATEGY_H */


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Gereon Kremer
4		*
5		* This file is part of the cvc5 project.
6		*
7		* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8		* in the top-level source directory and their institutional affiliations.
9		* All rights reserved. See the file COPYING in the top-level source
10		* directory for licensing information.
11		* ****************************************************************************
12		*
13		* Strategies for the nonlinear extension.
14		*/
15
16		#ifndef CVC5__THEORY__ARITH__NL__STRATEGY_H
17		#define CVC5__THEORY__ARITH__NL__STRATEGY_H
18
19		#include <iosfwd>
20		#include <vector>
21
22		#include "options/options.h"
23
24		namespace cvc5 {
25		namespace theory {
26		namespace arith {
27		namespace nl {
28
29		/** The possible inference steps for the nonlinear extension */
30		enum class InferStep
31		{
32		/** Break if any lemma is pending */
33		BREAK,
34		/** Flush waiting lemmas to be pending */
35		FLUSH_WAITING_LEMMAS,
36
37		/** Initialize the CAD solver */
38		CAD_INIT,
39		/** A full CAD check */
40		CAD_FULL,
41
42		/** Initialize the IAND solver */
43		IAND_INIT,
44		/** A full IAND check */
45		IAND_FULL,
46		/** An initial IAND check */
47		IAND_INITIAL,
48
49		/** Initialize the POW2 solver */
50		POW2_INIT,
51		/** A full POW2 check */
52		POW2_FULL,
53		/** An initial POW2 check */
54		POW2_INITIAL,
55
56		/** An ICP check */
57
58		ICP,
59
60		/** Initialize the NL solver */
61		NL_INIT,
62		/** Nl factoring lemmas */
63		NL_FACTORING,
64		/** Nl lemmas for monomial bound inference */
65		NL_MONOMIAL_INFER_BOUNDS,
66		/** Nl lemmas for monomial magnitudes (class 0) */
67		NL_MONOMIAL_MAGNITUDE0,
68		/** Nl lemmas for monomial magnitudes (class 1) */
69		NL_MONOMIAL_MAGNITUDE1,
70		/** Nl lemmas for monomial magnitudes (class 2) */
71		NL_MONOMIAL_MAGNITUDE2,
72		/** Nl lemmas for monomial signs */
73		NL_MONOMIAL_SIGN,
74		/** Nl lemmas for resolution bounds */
75		NL_RESOLUTION_BOUNDS,
76		/** Nl splitting at zero */
77		NL_SPLIT_ZERO,
78		/** Nl tangent plane lemmas */
79		NL_TANGENT_PLANES,
80		/** Nl tangent plane lemmas as waiting lemmas */
81		NL_TANGENT_PLANES_WAITING,
82
83		/** Initialize the transcendental solver */
84		TRANS_INIT,
85		/** Initial transcendental lemmas */
86		TRANS_INITIAL,
87		/** Monotonicity lemmas from transcendental solver */
88		TRANS_MONOTONIC,
89		/** Tangent planes from transcendental solver */
90		TRANS_TANGENT_PLANES,
91		};
92
93		/** Streaming operator for InferStep */
94		std::ostream& operator<<(std::ostream& os, InferStep step);
95
96		/** A sequence of steps */
97		using StepSequence = std::vector<InferStep>;
98
99		/**
100		* Stores an interleaving of multiple StepSequences.
101		*
102		* Every Branch of the interleaving holds a StepSequence s_i and a constant c_i.
103		* Once initialized, the interleaving may be asked repeatedly for a
104		* StepSequence. Repeated calls cycle through the branches, but will return
105		* every branch repeatedly as specified by its constant.
106		*
107		* Let for example [(s_1, 1), (s_2, 2), (s_3, 1)], then the sequence returned by
108		* get() would be: s_1, s_2, s_2, s_3, s_1, s_2, s_2, s_3, ...
109		*/
110	10420	class Interleaving
111		{
112		public:
113		/** Add a new branch to this interleaving */
114		void add(const StepSequence& ss, std::size_t constant = 1);
115		/**
116		* Reset the counter to start from the first branch for the next get() call
117		*/
118		void resetCounter();
119		/** Retrieve the next branch */
120		const StepSequence& get();
121		/** Check whether this interleaving is empty */
122		bool empty() const;
123
124		private:
125		/** Represents a single branch in an interleaving */
126	1476	struct Branch
127		{
128		StepSequence d_steps;
129		std::size_t d_interleavingConstant;
130		};
131		/** The current counter of get() calls */
132		std::size_t d_counter = 0;
133		/** The overall size of interleaving (considering constants) */
134		std::size_t d_size = 0;
135		/** The branches */
136		std::vector<Branch> d_branches;
137		};
138
139		/**
140		* A small wrapper around a StepSequence.
141		*
142		* This class makes handling a StepSequence slightly more convenient.
143		* Also, it may help wrapping a more flexible strategy implementation in the
144		* future.
145		*/
146		class StepGenerator
147		{
148		public:
149	3949	StepGenerator(const StepSequence& ss) : d_steps(ss) {}
150		/** Check if there is another step */
151		bool hasNext() const;
152		/** Get the next step */
153		InferStep next();
154
155		private:
156		/** The StepSequence to process */
157		const StepSequence& d_steps;
158		/** The next step */
159		std::size_t d_next = 0;
160		};
161
162		/**
163		* A strategy for the nonlinear extension
164		*
165		* A strategy consists of multiple step sequences that are interleaved for every
166		* Theory::Effort. The initialization creates the strategy. Calling
167		* getStrategy() yields a StepGenerator that produces a sequence of InferSteps.
168		*/
169	10420	class Strategy
170		{
171		public:
172		/** Is this strategy initialized? */
173		bool isStrategyInit() const;
174		/** Initialize this strategy */
175		void initializeStrategy(const Options& options);
176		/** Retrieve the strategy for the given effort e */
177		StepGenerator getStrategy();
178
179		private:
180		/** The interleaving for this strategy */
181		Interleaving d_interleaving;
182		};
183
184		} // namespace nl
185		} // namespace arith
186		} // namespace theory
187		} // namespace cvc5
188
189		#endif /* CVC5__THEORY__ARITH__NL__STRATEGY_H */