GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/nl/strategy.h Lines: 4 4 100.0 %
Date: 2021-03-22 Branches: 0 0 0.0 %

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