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