1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Gereon Kremer, Andrew Reynolds |
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 |
|
* Implementation of non-linear solver. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/arith/nl/strategy.h" |
17 |
|
|
18 |
|
#include <iostream> |
19 |
|
|
20 |
|
#include "base/check.h" |
21 |
|
#include "options/arith_options.h" |
22 |
|
|
23 |
|
namespace cvc5 { |
24 |
|
namespace theory { |
25 |
|
namespace arith { |
26 |
|
namespace nl { |
27 |
|
|
28 |
|
std::ostream& operator<<(std::ostream& os, InferStep step) |
29 |
|
{ |
30 |
|
switch (step) |
31 |
|
{ |
32 |
|
case InferStep::BREAK: return os << "BREAK"; |
33 |
|
case InferStep::FLUSH_WAITING_LEMMAS: return os << "FLUSH_WAITING_LEMMAS"; |
34 |
|
case InferStep::CAD_INIT: return os << "CAD_INIT"; |
35 |
|
case InferStep::CAD_FULL: return os << "CAD_FULL"; |
36 |
|
case InferStep::NL_FACTORING: return os << "NL_FACTORING"; |
37 |
|
case InferStep::IAND_INIT: return os << "IAND_INIT"; |
38 |
|
case InferStep::IAND_FULL: return os << "IAND_FULL"; |
39 |
|
case InferStep::IAND_INITIAL: return os << "IAND_INITIAL"; |
40 |
|
case InferStep::POW2_INIT: return os << "POW2_INIT"; |
41 |
|
case InferStep::POW2_FULL: return os << "POW2_FULL"; |
42 |
|
case InferStep::POW2_INITIAL: return os << "POW2_INITIAL"; |
43 |
|
case InferStep::ICP: return os << "ICP"; |
44 |
|
case InferStep::NL_INIT: return os << "NL_INIT"; |
45 |
|
case InferStep::NL_MONOMIAL_INFER_BOUNDS: |
46 |
|
return os << "NL_MONOMIAL_INFER_BOUNDS"; |
47 |
|
case InferStep::NL_MONOMIAL_MAGNITUDE0: |
48 |
|
return os << "NL_MONOMIAL_MAGNITUDE0"; |
49 |
|
case InferStep::NL_MONOMIAL_MAGNITUDE1: |
50 |
|
return os << "NL_MONOMIAL_MAGNITUDE1"; |
51 |
|
case InferStep::NL_MONOMIAL_MAGNITUDE2: |
52 |
|
return os << "NL_MONOMIAL_MAGNITUDE2"; |
53 |
|
case InferStep::NL_MONOMIAL_SIGN: return os << "NL_MONOMIAL_SIGN"; |
54 |
|
case InferStep::NL_RESOLUTION_BOUNDS: return os << "NL_RESOLUTION_BOUNDS"; |
55 |
|
case InferStep::NL_SPLIT_ZERO: return os << "NL_SPLIT_ZERO"; |
56 |
|
case InferStep::NL_TANGENT_PLANES: return os << "NL_TANGENT_PLANES"; |
57 |
|
case InferStep::NL_TANGENT_PLANES_WAITING: |
58 |
|
return os << "NL_TANGENT_PLANES_WAITING"; |
59 |
|
case InferStep::TRANS_INIT: return os << "TRANS_INIT"; |
60 |
|
case InferStep::TRANS_INITIAL: return os << "TRANS_INITIAL"; |
61 |
|
case InferStep::TRANS_MONOTONIC: return os << "TRANS_MONOTONIC"; |
62 |
|
case InferStep::TRANS_TANGENT_PLANES: return os << "TRANS_TANGENT_PLANES"; |
63 |
|
default: Unreachable(); return os << "UNKNOWN_STEP"; |
64 |
|
} |
65 |
|
} |
66 |
|
|
67 |
|
namespace { |
68 |
|
/** Puts a new InferStep into a StepSequence */ |
69 |
16339 |
inline StepSequence& operator<<(StepSequence& steps, InferStep s) |
70 |
|
{ |
71 |
16339 |
steps.emplace_back(s); |
72 |
16339 |
return steps; |
73 |
|
} |
74 |
|
} // namespace |
75 |
|
|
76 |
493 |
void Interleaving::add(const StepSequence& ss, std::size_t constant) |
77 |
|
{ |
78 |
493 |
d_branches.emplace_back(Branch{ss, constant}); |
79 |
493 |
d_size += constant; |
80 |
493 |
} |
81 |
|
void Interleaving::resetCounter() { d_counter = 0; } |
82 |
|
|
83 |
4009 |
const StepSequence& Interleaving::get() |
84 |
|
{ |
85 |
4009 |
Assert(!d_branches.empty()) |
86 |
|
<< "Can not get next sequence from an empty interleaving."; |
87 |
4009 |
std::size_t cnt = d_counter; |
88 |
|
// Increase the counter |
89 |
4009 |
d_counter = (d_counter + 1) % d_size; |
90 |
4009 |
for (const auto& branch : d_branches) |
91 |
|
{ |
92 |
4009 |
if (cnt < branch.d_interleavingConstant) |
93 |
|
{ |
94 |
|
// This is the current branch |
95 |
4009 |
return branch.d_steps; |
96 |
|
} |
97 |
|
cnt -= branch.d_interleavingConstant; |
98 |
|
} |
99 |
|
Assert(false) << "Something went wrong."; |
100 |
|
return d_branches[0].d_steps; |
101 |
|
} |
102 |
4009 |
bool Interleaving::empty() const { return d_branches.empty(); } |
103 |
|
|
104 |
65564 |
bool StepGenerator::hasNext() const { return d_next < d_steps.size(); } |
105 |
65136 |
InferStep StepGenerator::next() { return d_steps[d_next++]; } |
106 |
|
|
107 |
4009 |
bool Strategy::isStrategyInit() const { return !d_interleaving.empty(); } |
108 |
493 |
void Strategy::initializeStrategy(const Options& options) |
109 |
|
{ |
110 |
986 |
StepSequence one; |
111 |
493 |
if (options.arith.nlICP) |
112 |
|
{ |
113 |
2 |
one << InferStep::ICP << InferStep::BREAK; |
114 |
|
} |
115 |
493 |
if (options.arith.nlExt == options::NlExtMode::FULL |
116 |
39 |
|| options.arith.nlExt == options::NlExtMode::LIGHT) |
117 |
|
{ |
118 |
486 |
one << InferStep::NL_INIT << InferStep::BREAK; |
119 |
|
} |
120 |
493 |
if (options.arith.nlExt == options::NlExtMode::FULL) |
121 |
|
{ |
122 |
454 |
one << InferStep::TRANS_INIT << InferStep::BREAK; |
123 |
454 |
if (options.arith.nlExtSplitZero) |
124 |
|
{ |
125 |
|
one << InferStep::NL_SPLIT_ZERO << InferStep::BREAK; |
126 |
|
} |
127 |
454 |
one << InferStep::TRANS_INITIAL << InferStep::BREAK; |
128 |
|
} |
129 |
493 |
one << InferStep::IAND_INIT; |
130 |
493 |
one << InferStep::IAND_INITIAL << InferStep::BREAK; |
131 |
493 |
one << InferStep::POW2_INIT; |
132 |
493 |
one << InferStep::POW2_INITIAL << InferStep::BREAK; |
133 |
493 |
if (options.arith.nlExt == options::NlExtMode::FULL |
134 |
39 |
|| options.arith.nlExt == options::NlExtMode::LIGHT) |
135 |
|
{ |
136 |
486 |
one << InferStep::NL_MONOMIAL_SIGN << InferStep::BREAK; |
137 |
486 |
one << InferStep::NL_MONOMIAL_MAGNITUDE0 << InferStep::BREAK; |
138 |
|
} |
139 |
493 |
if (options.arith.nlExt == options::NlExtMode::FULL) |
140 |
|
{ |
141 |
454 |
one << InferStep::TRANS_MONOTONIC << InferStep::BREAK; |
142 |
454 |
one << InferStep::NL_MONOMIAL_MAGNITUDE1 << InferStep::BREAK; |
143 |
454 |
one << InferStep::NL_MONOMIAL_MAGNITUDE2 << InferStep::BREAK; |
144 |
454 |
one << InferStep::NL_MONOMIAL_INFER_BOUNDS; |
145 |
454 |
if (options.arith.nlExtTangentPlanes |
146 |
52 |
&& options.arith.nlExtTangentPlanesInterleave) |
147 |
|
{ |
148 |
|
one << InferStep::NL_TANGENT_PLANES; |
149 |
|
} |
150 |
454 |
one << InferStep::BREAK; |
151 |
454 |
one << InferStep::FLUSH_WAITING_LEMMAS << InferStep::BREAK; |
152 |
454 |
if (options.arith.nlExtFactor) |
153 |
|
{ |
154 |
454 |
one << InferStep::NL_FACTORING << InferStep::BREAK; |
155 |
|
} |
156 |
454 |
if (options.arith.nlExtResBound) |
157 |
|
{ |
158 |
|
one << InferStep::NL_MONOMIAL_INFER_BOUNDS << InferStep::BREAK; |
159 |
|
} |
160 |
454 |
if (options.arith.nlExtTangentPlanes |
161 |
52 |
&& !options.arith.nlExtTangentPlanesInterleave) |
162 |
|
{ |
163 |
52 |
one << InferStep::NL_TANGENT_PLANES_WAITING; |
164 |
|
} |
165 |
454 |
if (options.arith.nlExtTfTangentPlanes) |
166 |
|
{ |
167 |
452 |
one << InferStep::TRANS_TANGENT_PLANES; |
168 |
|
} |
169 |
454 |
one << InferStep::BREAK; |
170 |
|
} |
171 |
493 |
one << InferStep::IAND_FULL << InferStep::BREAK; |
172 |
493 |
one << InferStep::POW2_FULL << InferStep::BREAK; |
173 |
493 |
if (options.arith.nlCad) |
174 |
|
{ |
175 |
89 |
one << InferStep::CAD_INIT; |
176 |
|
} |
177 |
493 |
if (options.arith.nlCad) |
178 |
|
{ |
179 |
89 |
one << InferStep::CAD_FULL << InferStep::BREAK; |
180 |
|
} |
181 |
|
|
182 |
493 |
d_interleaving.add(one); |
183 |
493 |
} |
184 |
4009 |
StepGenerator Strategy::getStrategy() |
185 |
|
{ |
186 |
4009 |
return StepGenerator(d_interleaving.get()); |
187 |
|
} |
188 |
|
|
189 |
|
} // namespace nl |
190 |
|
} // namespace arith |
191 |
|
} // namespace theory |
192 |
29577 |
} // namespace cvc5 |