1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Gereon Kremer |
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 |
|
* Implement intersection of intervals for propagation. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/arith/nl/icp/intersection.h" |
17 |
|
|
18 |
|
#ifdef CVC5_POLY_IMP |
19 |
|
|
20 |
|
#include <iostream> |
21 |
|
|
22 |
|
#include <poly/polyxx.h> |
23 |
|
|
24 |
|
#include "base/check.h" |
25 |
|
#include "base/output.h" |
26 |
|
#include "theory/arith/nl/poly_conversion.h" |
27 |
|
|
28 |
|
namespace cvc5 { |
29 |
|
namespace theory { |
30 |
|
namespace arith { |
31 |
|
namespace nl { |
32 |
|
namespace icp { |
33 |
|
|
34 |
88 |
PropagationResult intersect_interval_with(poly::Interval& cur, |
35 |
|
const poly::Interval& res, |
36 |
|
std::size_t size_threshold) |
37 |
|
{ |
38 |
176 |
Trace("nl-icp") << cur << " := " << cur << " intersected with " << res |
39 |
88 |
<< std::endl; |
40 |
|
|
41 |
176 |
if (bitsize(get_lower(res)) > size_threshold |
42 |
88 |
|| bitsize(get_upper(res)) > size_threshold) |
43 |
|
{ |
44 |
50 |
Trace("nl-icp") << "Reached bitsize threshold" << std::endl; |
45 |
50 |
return PropagationResult::NOT_CHANGED; |
46 |
|
} |
47 |
|
|
48 |
|
// Basic idea to organize this function: |
49 |
|
// The bounds for res have 5 positions: |
50 |
|
// 1 < 2 (lower(cur)) < 3 < 4 (upper(cur)) < 5 |
51 |
|
|
52 |
38 |
if (get_upper(res) < get_lower(cur)) |
53 |
|
{ |
54 |
|
// upper(res) at 1 |
55 |
|
Trace("nl-icp") << "res < cur -> conflict" << std::endl; |
56 |
|
return PropagationResult::CONFLICT; |
57 |
|
} |
58 |
38 |
if (get_upper(res) == get_lower(cur)) |
59 |
|
{ |
60 |
|
// upper(res) at 2 |
61 |
|
if (get_upper_open(res) || get_lower_open(cur)) |
62 |
|
{ |
63 |
|
Trace("nl-icp") << "meet at lower, but one is open -> conflict" |
64 |
|
<< std::endl; |
65 |
|
return PropagationResult::CONFLICT; |
66 |
|
} |
67 |
|
if (!is_point(cur)) |
68 |
|
{ |
69 |
|
Trace("nl-icp") << "contracts to point interval at lower" << std::endl; |
70 |
|
cur = poly::Interval(get_upper(res)); |
71 |
|
return PropagationResult::CONTRACTED; |
72 |
|
} |
73 |
|
return PropagationResult::NOT_CHANGED; |
74 |
|
} |
75 |
38 |
Assert(get_upper(res) > get_lower(cur)) |
76 |
|
<< "Comparison operator does weird stuff."; |
77 |
38 |
if (get_upper(res) < get_upper(cur)) |
78 |
|
{ |
79 |
|
// upper(res) at 3 |
80 |
2 |
if (get_lower(res) < get_lower(cur)) |
81 |
|
{ |
82 |
|
// lower(res) at 1 |
83 |
|
Trace("nl-icp") << "lower(cur) .. upper(res)" << std::endl; |
84 |
|
cur.set_upper(get_upper(res), get_upper_open(res)); |
85 |
|
return PropagationResult::CONTRACTED; |
86 |
|
} |
87 |
2 |
if (get_lower(res) == get_lower(cur)) |
88 |
|
{ |
89 |
|
// lower(res) at 2 |
90 |
|
Trace("nl-icp") << "meet at lower, lower(cur) .. upper(res)" << std::endl; |
91 |
|
cur = poly::Interval(get_lower(cur), |
92 |
|
get_lower_open(cur) || get_lower_open(res), |
93 |
|
get_upper(res), |
94 |
|
get_upper_open(res)); |
95 |
|
if (get_lower_open(cur) && !get_lower_open(res)) |
96 |
|
{ |
97 |
|
return PropagationResult::CONTRACTED; |
98 |
|
} |
99 |
|
return PropagationResult::CONTRACTED_WITHOUT_CURRENT; |
100 |
|
} |
101 |
2 |
Assert(get_lower(res) > get_lower(cur)) |
102 |
|
<< "Comparison operator does weird stuff."; |
103 |
|
// lower(res) at 3 |
104 |
2 |
Trace("nl-icp") << "cur covers res" << std::endl; |
105 |
2 |
cur = res; |
106 |
2 |
return PropagationResult::CONTRACTED_WITHOUT_CURRENT; |
107 |
|
} |
108 |
36 |
if (get_upper(res) == get_upper(cur)) |
109 |
|
{ |
110 |
|
// upper(res) at 4 |
111 |
18 |
if (get_lower(res) < get_lower(cur)) |
112 |
|
{ |
113 |
|
// lower(res) at 1 |
114 |
14 |
Trace("nl-icp") << "res covers cur but meet at upper" << std::endl; |
115 |
14 |
if (get_upper_open(res) && !get_upper_open(cur)) |
116 |
|
{ |
117 |
2 |
cur.set_upper(get_upper(cur), true); |
118 |
2 |
return PropagationResult::CONTRACTED; |
119 |
|
} |
120 |
12 |
return PropagationResult::NOT_CHANGED; |
121 |
|
} |
122 |
4 |
if (get_lower(res) == get_lower(cur)) |
123 |
|
{ |
124 |
|
// lower(res) at 2 |
125 |
4 |
Trace("nl-icp") << "same bounds but check openness" << std::endl; |
126 |
4 |
bool changed = false; |
127 |
4 |
if (get_lower_open(res) && !get_lower_open(cur)) |
128 |
|
{ |
129 |
|
changed = true; |
130 |
|
cur.set_lower(get_lower(cur), true); |
131 |
|
} |
132 |
4 |
if (get_upper_open(res) && !get_upper_open(cur)) |
133 |
|
{ |
134 |
|
changed = true; |
135 |
|
cur.set_upper(get_upper(cur), true); |
136 |
|
} |
137 |
4 |
if (changed) |
138 |
|
{ |
139 |
|
if ((get_lower_open(res) || !get_upper_open(cur)) |
140 |
|
&& (get_upper_open(res) || !get_upper_open(cur))) |
141 |
|
{ |
142 |
|
return PropagationResult::CONTRACTED_WITHOUT_CURRENT; |
143 |
|
} |
144 |
|
return PropagationResult::CONTRACTED; |
145 |
|
} |
146 |
4 |
return PropagationResult::NOT_CHANGED; |
147 |
|
} |
148 |
|
Assert(get_lower(res) > get_lower(cur)) |
149 |
|
<< "Comparison operator does weird stuff."; |
150 |
|
// lower(res) at 3 |
151 |
|
Trace("nl-icp") << "cur covers res but meet at upper" << std::endl; |
152 |
|
cur = poly::Interval(get_lower(res), |
153 |
|
get_lower_open(res), |
154 |
|
get_upper(res), |
155 |
|
get_upper_open(cur) || get_upper_open(res)); |
156 |
|
if (get_upper_open(cur) && !get_upper_open(res)) |
157 |
|
{ |
158 |
|
return PropagationResult::CONTRACTED; |
159 |
|
} |
160 |
|
return PropagationResult::CONTRACTED_WITHOUT_CURRENT; |
161 |
|
} |
162 |
|
|
163 |
18 |
Assert(get_upper(res) > get_upper(cur)) |
164 |
|
<< "Comparison operator does weird stuff."; |
165 |
|
// upper(res) at 5 |
166 |
|
|
167 |
18 |
if (get_lower(res) < get_lower(cur)) |
168 |
|
{ |
169 |
|
// lower(res) at 1 |
170 |
10 |
Trace("nl-icp") << "res covers cur" << std::endl; |
171 |
10 |
return PropagationResult::NOT_CHANGED; |
172 |
|
} |
173 |
8 |
if (get_lower(res) == get_lower(cur)) |
174 |
|
{ |
175 |
|
// lower(res) at 2 |
176 |
8 |
Trace("nl-icp") << "res covers cur but meet at lower" << std::endl; |
177 |
8 |
if (get_lower_open(res) && is_point(cur)) |
178 |
|
{ |
179 |
|
return PropagationResult::CONFLICT; |
180 |
|
} |
181 |
8 |
else if (get_lower_open(res) && !get_lower_open(cur)) |
182 |
|
{ |
183 |
|
cur.set_lower(get_lower(cur), true); |
184 |
|
return PropagationResult::CONTRACTED; |
185 |
|
} |
186 |
8 |
return PropagationResult::NOT_CHANGED; |
187 |
|
} |
188 |
|
Assert(get_lower(res) > get_lower(cur)) |
189 |
|
<< "Comparison operator does weird stuff."; |
190 |
|
if (get_lower(res) < get_upper(cur)) |
191 |
|
{ |
192 |
|
// lower(res) at 3 |
193 |
|
Trace("nl-icp") << "lower(res) .. upper(cur)" << std::endl; |
194 |
|
cur.set_lower(get_lower(res), get_lower_open(res)); |
195 |
|
return PropagationResult::CONTRACTED; |
196 |
|
} |
197 |
|
if (get_lower(res) == get_upper(cur)) |
198 |
|
{ |
199 |
|
// lower(res) at 4 |
200 |
|
if (get_lower_open(res) || get_upper_open(cur)) |
201 |
|
{ |
202 |
|
Trace("nl-icp") << "meet at upper, but one is open -> conflict" |
203 |
|
<< std::endl; |
204 |
|
return PropagationResult::CONFLICT; |
205 |
|
} |
206 |
|
if (!is_point(cur)) |
207 |
|
{ |
208 |
|
Trace("nl-icp") << "contracts to point interval at upper" << std::endl; |
209 |
|
cur = poly::Interval(get_lower(res)); |
210 |
|
return PropagationResult::CONTRACTED; |
211 |
|
} |
212 |
|
return PropagationResult::NOT_CHANGED; |
213 |
|
} |
214 |
|
|
215 |
|
Assert(get_lower(res) > get_upper(cur)); |
216 |
|
// lower(res) at 5 |
217 |
|
Trace("nl-icp") << "res > cur -> conflict" << std::endl; |
218 |
|
return PropagationResult::CONFLICT; |
219 |
|
} |
220 |
|
|
221 |
|
} // namespace icp |
222 |
|
} // namespace nl |
223 |
|
} // namespace arith |
224 |
|
} // namespace theory |
225 |
28191 |
} // namespace cvc5 |
226 |
|
|
227 |
|
#endif |