Head

GCC Code Coverage Report

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

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