1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
|
/********************* */
/*! \file strategy.h
** \verbatim
** Top contributors (to current version):
** Gereon Kremer
** This file is part of the CVC4 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.\endverbatim
**
** \brief Strategies for the nonlinear extension
**/
#ifndef CVC4__THEORY__ARITH__NL__STRATEGY_H
#define CVC4__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 /* CVC4__THEORY__ARITH__NL__STRATEGY_H */
|
