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::ICP: return os << "ICP"; |
41 |
|
case InferStep::NL_INIT: return os << "NL_INIT"; |
42 |
|
case InferStep::NL_MONOMIAL_INFER_BOUNDS: |
43 |
|
return os << "NL_MONOMIAL_INFER_BOUNDS"; |
44 |
|
case InferStep::NL_MONOMIAL_MAGNITUDE0: |
45 |
|
return os << "NL_MONOMIAL_MAGNITUDE0"; |
46 |
|
case InferStep::NL_MONOMIAL_MAGNITUDE1: |
47 |
|
return os << "NL_MONOMIAL_MAGNITUDE1"; |
48 |
|
case InferStep::NL_MONOMIAL_MAGNITUDE2: |
49 |
|
return os << "NL_MONOMIAL_MAGNITUDE2"; |
50 |
|
case InferStep::NL_MONOMIAL_SIGN: return os << "NL_MONOMIAL_SIGN"; |
51 |
|
case InferStep::NL_RESOLUTION_BOUNDS: return os << "NL_RESOLUTION_BOUNDS"; |
52 |
|
case InferStep::NL_SPLIT_ZERO: return os << "NL_SPLIT_ZERO"; |
53 |
|
case InferStep::NL_TANGENT_PLANES: return os << "NL_TANGENT_PLANES"; |
54 |
|
case InferStep::NL_TANGENT_PLANES_WAITING: |
55 |
|
return os << "NL_TANGENT_PLANES_WAITING"; |
56 |
|
case InferStep::TRANS_INIT: return os << "TRANS_INIT"; |
57 |
|
case InferStep::TRANS_INITIAL: return os << "TRANS_INITIAL"; |
58 |
|
case InferStep::TRANS_MONOTONIC: return os << "TRANS_MONOTONIC"; |
59 |
|
case InferStep::TRANS_TANGENT_PLANES: return os << "TRANS_TANGENT_PLANES"; |
60 |
|
default: Unreachable(); return os << "UNKNOWN_STEP"; |
61 |
|
} |
62 |
|
} |
63 |
|
|
64 |
|
namespace { |
65 |
|
/** Puts a new InferStep into a StepSequence */ |
66 |
12333 |
inline StepSequence& operator<<(StepSequence& steps, InferStep s) |
67 |
|
{ |
68 |
12333 |
steps.emplace_back(s); |
69 |
12333 |
return steps; |
70 |
|
} |
71 |
|
} // namespace |
72 |
|
|
73 |
437 |
void Interleaving::add(const StepSequence& ss, std::size_t constant) |
74 |
|
{ |
75 |
437 |
d_branches.emplace_back(Branch{ss, constant}); |
76 |
437 |
d_size += constant; |
77 |
437 |
} |
78 |
|
void Interleaving::resetCounter() { d_counter = 0; } |
79 |
|
|
80 |
2841 |
const StepSequence& Interleaving::get() |
81 |
|
{ |
82 |
2841 |
Assert(!d_branches.empty()) |
83 |
|
<< "Can not get next sequence from an empty interleaving."; |
84 |
2841 |
std::size_t cnt = d_counter; |
85 |
|
// Increase the counter |
86 |
2841 |
d_counter = (d_counter + 1) % d_size; |
87 |
2841 |
for (const auto& branch : d_branches) |
88 |
|
{ |
89 |
2841 |
if (cnt < branch.d_interleavingConstant) |
90 |
|
{ |
91 |
|
// This is the current branch |
92 |
2841 |
return branch.d_steps; |
93 |
|
} |
94 |
|
cnt -= branch.d_interleavingConstant; |
95 |
|
} |
96 |
|
Assert(false) << "Something went wrong."; |
97 |
|
return d_branches[0].d_steps; |
98 |
|
} |
99 |
2841 |
bool Interleaving::empty() const { return d_branches.empty(); } |
100 |
|
|
101 |
41644 |
bool StepGenerator::hasNext() const { return d_next < d_steps.size(); } |
102 |
41377 |
InferStep StepGenerator::next() { return d_steps[d_next++]; } |
103 |
|
|
104 |
2841 |
bool Strategy::isStrategyInit() const { return !d_interleaving.empty(); } |
105 |
437 |
void Strategy::initializeStrategy() |
106 |
|
{ |
107 |
874 |
StepSequence one; |
108 |
876 |
if (options::nlICP()) |
109 |
|
{ |
110 |
2 |
one << InferStep::ICP << InferStep::BREAK; |
111 |
|
} |
112 |
874 |
if (options::nlExt() == options::NlExtMode::FULL |
113 |
437 |
|| options::nlExt() == options::NlExtMode::LIGHT) |
114 |
|
{ |
115 |
429 |
one << InferStep::NL_INIT << InferStep::BREAK; |
116 |
|
} |
117 |
437 |
if (options::nlExt() == options::NlExtMode::FULL) |
118 |
|
{ |
119 |
403 |
one << InferStep::TRANS_INIT << InferStep::BREAK; |
120 |
806 |
if (options::nlExtSplitZero()) |
121 |
|
{ |
122 |
|
one << InferStep::NL_SPLIT_ZERO << InferStep::BREAK; |
123 |
|
} |
124 |
403 |
one << InferStep::TRANS_INITIAL << InferStep::BREAK; |
125 |
|
} |
126 |
437 |
one << InferStep::IAND_INIT; |
127 |
437 |
one << InferStep::IAND_INITIAL << InferStep::BREAK; |
128 |
874 |
if (options::nlExt() == options::NlExtMode::FULL |
129 |
437 |
|| options::nlExt() == options::NlExtMode::LIGHT) |
130 |
|
{ |
131 |
429 |
one << InferStep::NL_MONOMIAL_SIGN << InferStep::BREAK; |
132 |
429 |
one << InferStep::NL_MONOMIAL_MAGNITUDE0 << InferStep::BREAK; |
133 |
|
} |
134 |
437 |
if (options::nlExt() == options::NlExtMode::FULL) |
135 |
|
{ |
136 |
403 |
one << InferStep::TRANS_MONOTONIC << InferStep::BREAK; |
137 |
403 |
one << InferStep::NL_MONOMIAL_MAGNITUDE1 << InferStep::BREAK; |
138 |
403 |
one << InferStep::NL_MONOMIAL_MAGNITUDE2 << InferStep::BREAK; |
139 |
403 |
one << InferStep::NL_MONOMIAL_INFER_BOUNDS; |
140 |
806 |
if (options::nlExtTangentPlanes() |
141 |
403 |
&& options::nlExtTangentPlanesInterleave()) |
142 |
|
{ |
143 |
|
one << InferStep::NL_TANGENT_PLANES; |
144 |
|
} |
145 |
403 |
one << InferStep::BREAK; |
146 |
403 |
one << InferStep::FLUSH_WAITING_LEMMAS << InferStep::BREAK; |
147 |
806 |
if (options::nlExtFactor()) |
148 |
|
{ |
149 |
403 |
one << InferStep::NL_FACTORING << InferStep::BREAK; |
150 |
|
} |
151 |
806 |
if (options::nlExtResBound()) |
152 |
|
{ |
153 |
|
one << InferStep::NL_MONOMIAL_INFER_BOUNDS << InferStep::BREAK; |
154 |
|
} |
155 |
806 |
if (options::nlExtTangentPlanes() |
156 |
403 |
&& !options::nlExtTangentPlanesInterleave()) |
157 |
|
{ |
158 |
72 |
one << InferStep::NL_TANGENT_PLANES_WAITING; |
159 |
|
} |
160 |
847 |
if (options::nlExtTfTangentPlanes()) |
161 |
|
{ |
162 |
401 |
one << InferStep::TRANS_TANGENT_PLANES; |
163 |
|
} |
164 |
403 |
one << InferStep::BREAK; |
165 |
|
} |
166 |
437 |
one << InferStep::IAND_FULL << InferStep::BREAK; |
167 |
437 |
if (options::nlCad()) |
168 |
|
{ |
169 |
82 |
one << InferStep::CAD_INIT; |
170 |
|
} |
171 |
437 |
if (options::nlCad()) |
172 |
|
{ |
173 |
82 |
one << InferStep::CAD_FULL << InferStep::BREAK; |
174 |
|
} |
175 |
|
|
176 |
437 |
d_interleaving.add(one); |
177 |
437 |
} |
178 |
2841 |
StepGenerator Strategy::getStrategy() |
179 |
|
{ |
180 |
2841 |
return StepGenerator(d_interleaving.get()); |
181 |
|
} |
182 |
|
|
183 |
|
} // namespace nl |
184 |
|
} // namespace arith |
185 |
|
} // namespace theory |
186 |
30283 |
} // namespace cvc5 |