Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arith/nl/strategy.h	Lines:	4	4	100.0 %
Date:	2021-08-01	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>

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