1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Martin Brain, Andrew Reynolds, Andres Noetzli |
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 |
|
* Theory of floating-point arithmetic. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/fp/theory_fp.h" |
17 |
|
|
18 |
|
#include <set> |
19 |
|
#include <stack> |
20 |
|
#include <unordered_set> |
21 |
|
#include <vector> |
22 |
|
|
23 |
|
#include "base/configuration.h" |
24 |
|
#include "expr/skolem_manager.h" |
25 |
|
#include "options/fp_options.h" |
26 |
|
#include "smt/logic_exception.h" |
27 |
|
#include "theory/fp/fp_word_blaster.h" |
28 |
|
#include "theory/fp/theory_fp_rewriter.h" |
29 |
|
#include "theory/output_channel.h" |
30 |
|
#include "theory/theory_model.h" |
31 |
|
#include "util/floatingpoint.h" |
32 |
|
|
33 |
|
using namespace std; |
34 |
|
|
35 |
|
namespace cvc5 { |
36 |
|
namespace theory { |
37 |
|
namespace fp { |
38 |
|
|
39 |
|
namespace helper { |
40 |
14 |
Node buildConjunct(const std::vector<TNode> &assumptions) { |
41 |
14 |
if (assumptions.size() == 0) { |
42 |
|
return NodeManager::currentNM()->mkConst<bool>(true); |
43 |
|
|
44 |
14 |
} else if (assumptions.size() == 1) { |
45 |
|
return assumptions[0]; |
46 |
|
|
47 |
|
} else { |
48 |
|
// \todo see bv::utils::flattenAnd |
49 |
|
|
50 |
28 |
NodeBuilder conjunction(kind::AND); |
51 |
48 |
for (std::vector<TNode>::const_iterator it = assumptions.begin(); |
52 |
48 |
it != assumptions.end(); ++it) { |
53 |
34 |
conjunction << *it; |
54 |
|
} |
55 |
|
|
56 |
14 |
return conjunction; |
57 |
|
} |
58 |
|
} |
59 |
|
} // namespace helper |
60 |
|
|
61 |
|
/** Constructs a new instance of TheoryFp w.r.t. the provided contexts. */ |
62 |
15271 |
TheoryFp::TheoryFp(Env& env, OutputChannel& out, Valuation valuation) |
63 |
|
: Theory(THEORY_FP, env, out, valuation), |
64 |
|
d_notification(*this), |
65 |
15271 |
d_registeredTerms(userContext()), |
66 |
15271 |
d_wordBlaster(new FpWordBlaster(userContext())), |
67 |
|
d_expansionRequested(false), |
68 |
15271 |
d_abstractionMap(userContext()), |
69 |
|
d_rewriter(userContext()), |
70 |
|
d_state(env, valuation), |
71 |
|
d_im(env, *this, d_state, "theory::fp::", true), |
72 |
15271 |
d_wbFactsCache(userContext()), |
73 |
76355 |
d_true(d_env.getNodeManager()->mkConst(true)) |
74 |
|
{ |
75 |
|
// indicate we are using the default theory state and inference manager |
76 |
15271 |
d_theoryState = &d_state; |
77 |
15271 |
d_inferManager = &d_im; |
78 |
15271 |
} |
79 |
|
|
80 |
15271 |
TheoryRewriter* TheoryFp::getTheoryRewriter() { return &d_rewriter; } |
81 |
|
|
82 |
7987 |
ProofRuleChecker* TheoryFp::getProofChecker() { return nullptr; } |
83 |
|
|
84 |
15271 |
bool TheoryFp::needsEqualityEngine(EeSetupInfo& esi) |
85 |
|
{ |
86 |
15271 |
esi.d_notify = &d_notification; |
87 |
15271 |
esi.d_name = "theory::fp::ee"; |
88 |
15271 |
return true; |
89 |
|
} |
90 |
|
|
91 |
15271 |
void TheoryFp::finishInit() |
92 |
|
{ |
93 |
15271 |
Assert(d_equalityEngine != nullptr); |
94 |
|
// Kinds that are to be handled in the congruence closure |
95 |
|
|
96 |
15271 |
d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_ABS); |
97 |
15271 |
d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_NEG); |
98 |
15271 |
d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_ADD); |
99 |
|
// d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_SUB); // Removed |
100 |
15271 |
d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_MULT); |
101 |
15271 |
d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_DIV); |
102 |
15271 |
d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_FMA); |
103 |
15271 |
d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_SQRT); |
104 |
15271 |
d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_REM); |
105 |
15271 |
d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_RTI); |
106 |
|
// d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_MIN); // Removed |
107 |
|
// d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_MAX); // Removed |
108 |
15271 |
d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_MIN_TOTAL); |
109 |
15271 |
d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_MAX_TOTAL); |
110 |
|
|
111 |
|
// d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_EQ); // Removed |
112 |
15271 |
d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_LEQ); |
113 |
15271 |
d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_LT); |
114 |
|
// d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_GEQ); // Removed |
115 |
|
// d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_GT); // Removed |
116 |
15271 |
d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_ISN); |
117 |
15271 |
d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_ISSN); |
118 |
15271 |
d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_ISZ); |
119 |
15271 |
d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_ISINF); |
120 |
15271 |
d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_ISNAN); |
121 |
15271 |
d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_ISNEG); |
122 |
15271 |
d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_ISPOS); |
123 |
|
|
124 |
15271 |
d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR); |
125 |
15271 |
d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT); |
126 |
15271 |
d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_TO_FP_REAL); |
127 |
15271 |
d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR); |
128 |
15271 |
d_equalityEngine->addFunctionKind( |
129 |
|
kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR); |
130 |
|
// d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_TO_FP_GENERIC); // |
131 |
|
// Needed in parsing, should be rewritten away |
132 |
|
|
133 |
|
// d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_TO_UBV); // Removed |
134 |
|
// d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_TO_SBV); // Removed |
135 |
|
// d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_TO_REAL); // Removed |
136 |
15271 |
d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_TO_UBV_TOTAL); |
137 |
15271 |
d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_TO_SBV_TOTAL); |
138 |
15271 |
d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_TO_REAL_TOTAL); |
139 |
|
|
140 |
15271 |
d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_COMPONENT_NAN); |
141 |
15271 |
d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_COMPONENT_INF); |
142 |
15271 |
d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_COMPONENT_ZERO); |
143 |
15271 |
d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_COMPONENT_SIGN); |
144 |
15271 |
d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_COMPONENT_EXPONENT); |
145 |
15271 |
d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND); |
146 |
15271 |
d_equalityEngine->addFunctionKind(kind::ROUNDINGMODE_BITBLAST); |
147 |
15271 |
} |
148 |
|
|
149 |
3705 |
TrustNode TheoryFp::ppRewrite(TNode node, std::vector<SkolemLemma>& lems) |
150 |
|
{ |
151 |
3705 |
Trace("fp-ppRewrite") << "TheoryFp::ppRewrite(): " << node << std::endl; |
152 |
|
// first, see if we need to expand definitions |
153 |
7410 |
TrustNode texp = d_rewriter.expandDefinition(node); |
154 |
3705 |
if (!texp.isNull()) |
155 |
|
{ |
156 |
12 |
return texp; |
157 |
|
} |
158 |
|
|
159 |
7386 |
Node res = node; |
160 |
|
|
161 |
|
|
162 |
3693 |
if (res != node) |
163 |
|
{ |
164 |
|
Trace("fp-ppRewrite") << "TheoryFp::ppRewrite(): node " << node |
165 |
|
<< " rewritten to " << res << std::endl; |
166 |
|
return TrustNode::mkTrustRewrite(node, res, nullptr); |
167 |
|
} |
168 |
|
|
169 |
3693 |
return TrustNode::null(); |
170 |
|
} |
171 |
|
|
172 |
49 |
bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete) |
173 |
|
{ |
174 |
98 |
Trace("fp-refineAbstraction") << "TheoryFp::refineAbstraction(): " << abstract |
175 |
49 |
<< " vs. " << concrete << std::endl; |
176 |
49 |
Kind k = concrete.getKind(); |
177 |
49 |
if (k == kind::FLOATINGPOINT_TO_REAL_TOTAL) |
178 |
|
{ |
179 |
|
// Get the values |
180 |
12 |
Assert(m->hasTerm(abstract)); |
181 |
12 |
Assert(m->hasTerm(concrete[0])); |
182 |
12 |
Assert(m->hasTerm(concrete[1])); |
183 |
|
|
184 |
24 |
Node abstractValue = m->getValue(abstract); |
185 |
24 |
Node floatValue = m->getValue(concrete[0]); |
186 |
24 |
Node undefValue = m->getValue(concrete[1]); |
187 |
|
|
188 |
12 |
Assert(!abstractValue.isNull()); |
189 |
12 |
Assert(!floatValue.isNull()); |
190 |
12 |
Assert(!undefValue.isNull()); |
191 |
12 |
Assert(abstractValue.isConst()); |
192 |
12 |
Assert(floatValue.isConst()); |
193 |
12 |
Assert(undefValue.isConst()); |
194 |
|
|
195 |
|
// Work out the actual value for those args |
196 |
12 |
NodeManager *nm = NodeManager::currentNM(); |
197 |
|
|
198 |
|
Node evaluate = |
199 |
24 |
nm->mkNode(kind::FLOATINGPOINT_TO_REAL_TOTAL, floatValue, undefValue); |
200 |
24 |
Node concreteValue = rewrite(evaluate); |
201 |
12 |
Assert(concreteValue.isConst()); |
202 |
|
|
203 |
24 |
Trace("fp-refineAbstraction") |
204 |
24 |
<< "TheoryFp::refineAbstraction(): " << concrete[0] << " = " |
205 |
12 |
<< floatValue << std::endl |
206 |
24 |
<< "TheoryFp::refineAbstraction(): " << concrete[1] << " = " |
207 |
12 |
<< undefValue << std::endl |
208 |
12 |
<< "TheoryFp::refineAbstraction(): " << abstract << " = " |
209 |
12 |
<< abstractValue << std::endl |
210 |
12 |
<< "TheoryFp::refineAbstraction(): " << concrete << " = " |
211 |
12 |
<< concreteValue << std::endl; |
212 |
|
|
213 |
12 |
if (abstractValue != concreteValue) |
214 |
|
{ |
215 |
|
// Need refinement lemmas |
216 |
|
// only in the normal and subnormal case |
217 |
2 |
Assert(floatValue.getConst<FloatingPoint>().isNormal() |
218 |
|
|| floatValue.getConst<FloatingPoint>().isSubnormal()); |
219 |
|
|
220 |
|
Node defined = nm->mkNode( |
221 |
|
kind::AND, |
222 |
4 |
nm->mkNode(kind::NOT, |
223 |
4 |
nm->mkNode(kind::FLOATINGPOINT_ISNAN, concrete[0])), |
224 |
4 |
nm->mkNode(kind::NOT, |
225 |
12 |
nm->mkNode(kind::FLOATINGPOINT_ISINF, concrete[0]))); |
226 |
|
// First the "forward" constraints |
227 |
|
Node fg = nm->mkNode( |
228 |
|
kind::IMPLIES, |
229 |
|
defined, |
230 |
8 |
nm->mkNode( |
231 |
|
kind::EQUAL, |
232 |
4 |
nm->mkNode(kind::FLOATINGPOINT_GEQ, concrete[0], floatValue), |
233 |
8 |
nm->mkNode(kind::GEQ, abstract, concreteValue))); |
234 |
2 |
handleLemma(fg, InferenceId::FP_PREPROCESS); |
235 |
|
|
236 |
|
Node fl = nm->mkNode( |
237 |
|
kind::IMPLIES, |
238 |
|
defined, |
239 |
8 |
nm->mkNode( |
240 |
|
kind::EQUAL, |
241 |
4 |
nm->mkNode(kind::FLOATINGPOINT_LEQ, concrete[0], floatValue), |
242 |
8 |
nm->mkNode(kind::LEQ, abstract, concreteValue))); |
243 |
2 |
handleLemma(fl, InferenceId::FP_PREPROCESS); |
244 |
|
|
245 |
|
// Then the backwards constraints |
246 |
|
Node floatAboveAbstract = rewrite( |
247 |
12 |
nm->mkNode(kind::FLOATINGPOINT_TO_FP_REAL, |
248 |
4 |
nm->mkConst(FloatingPointToFPReal( |
249 |
4 |
concrete[0].getType().getConst<FloatingPointSize>())), |
250 |
4 |
nm->mkConst(RoundingMode::ROUND_TOWARD_POSITIVE), |
251 |
6 |
abstractValue)); |
252 |
|
|
253 |
|
Node bg = nm->mkNode( |
254 |
|
kind::IMPLIES, |
255 |
|
defined, |
256 |
8 |
nm->mkNode( |
257 |
|
kind::EQUAL, |
258 |
4 |
nm->mkNode( |
259 |
|
kind::FLOATINGPOINT_GEQ, concrete[0], floatAboveAbstract), |
260 |
8 |
nm->mkNode(kind::GEQ, abstract, abstractValue))); |
261 |
2 |
handleLemma(bg, InferenceId::FP_PREPROCESS); |
262 |
|
|
263 |
|
Node floatBelowAbstract = rewrite( |
264 |
12 |
nm->mkNode(kind::FLOATINGPOINT_TO_FP_REAL, |
265 |
4 |
nm->mkConst(FloatingPointToFPReal( |
266 |
4 |
concrete[0].getType().getConst<FloatingPointSize>())), |
267 |
4 |
nm->mkConst(RoundingMode::ROUND_TOWARD_NEGATIVE), |
268 |
6 |
abstractValue)); |
269 |
|
|
270 |
|
Node bl = nm->mkNode( |
271 |
|
kind::IMPLIES, |
272 |
|
defined, |
273 |
8 |
nm->mkNode( |
274 |
|
kind::EQUAL, |
275 |
4 |
nm->mkNode( |
276 |
|
kind::FLOATINGPOINT_LEQ, concrete[0], floatBelowAbstract), |
277 |
8 |
nm->mkNode(kind::LEQ, abstract, abstractValue))); |
278 |
2 |
handleLemma(bl, InferenceId::FP_PREPROCESS); |
279 |
|
// TODO : see if the overflow conditions could be improved #1914 |
280 |
|
|
281 |
2 |
return true; |
282 |
|
} |
283 |
|
else |
284 |
|
{ |
285 |
|
// No refinement needed |
286 |
10 |
return false; |
287 |
|
} |
288 |
|
} |
289 |
37 |
else if (k == kind::FLOATINGPOINT_TO_FP_REAL) |
290 |
|
{ |
291 |
|
// Get the values |
292 |
37 |
Assert(m->hasTerm(abstract)); |
293 |
37 |
Assert(m->hasTerm(concrete[0])); |
294 |
37 |
Assert(m->hasTerm(concrete[1])); |
295 |
|
|
296 |
74 |
Node abstractValue = m->getValue(abstract); |
297 |
74 |
Node rmValue = m->getValue(concrete[0]); |
298 |
74 |
Node realValue = m->getValue(concrete[1]); |
299 |
|
|
300 |
37 |
Assert(!abstractValue.isNull()); |
301 |
37 |
Assert(!rmValue.isNull()); |
302 |
37 |
Assert(!realValue.isNull()); |
303 |
37 |
Assert(abstractValue.isConst()); |
304 |
37 |
Assert(rmValue.isConst()); |
305 |
37 |
Assert(realValue.isConst()); |
306 |
|
|
307 |
|
// Work out the actual value for those args |
308 |
37 |
NodeManager *nm = NodeManager::currentNM(); |
309 |
|
|
310 |
|
Node evaluate = |
311 |
|
nm->mkNode(kind::FLOATINGPOINT_TO_FP_REAL, |
312 |
74 |
nm->mkConst(FloatingPointToFPReal( |
313 |
74 |
concrete.getType().getConst<FloatingPointSize>())), |
314 |
|
rmValue, |
315 |
148 |
realValue); |
316 |
74 |
Node concreteValue = rewrite(evaluate); |
317 |
37 |
Assert(concreteValue.isConst()); |
318 |
|
|
319 |
74 |
Trace("fp-refineAbstraction") |
320 |
74 |
<< "TheoryFp::refineAbstraction(): " << concrete[0] << " = " << rmValue |
321 |
37 |
<< std::endl |
322 |
74 |
<< "TheoryFp::refineAbstraction(): " << concrete[1] << " = " |
323 |
37 |
<< realValue << std::endl |
324 |
37 |
<< "TheoryFp::refineAbstraction(): " << abstract << " = " |
325 |
37 |
<< abstractValue << std::endl |
326 |
37 |
<< "TheoryFp::refineAbstraction(): " << concrete << " = " |
327 |
37 |
<< concreteValue << std::endl; |
328 |
|
|
329 |
37 |
if (abstractValue != concreteValue) |
330 |
|
{ |
331 |
31 |
Assert(!abstractValue.getConst<FloatingPoint>().isNaN()); |
332 |
31 |
Assert(!concreteValue.getConst<FloatingPoint>().isNaN()); |
333 |
|
|
334 |
62 |
Node correctRoundingMode = nm->mkNode(kind::EQUAL, concrete[0], rmValue); |
335 |
|
// TODO : Generalise to all rounding modes #1914 |
336 |
|
|
337 |
|
// First the "forward" constraints |
338 |
|
Node fg = nm->mkNode( |
339 |
|
kind::IMPLIES, |
340 |
|
correctRoundingMode, |
341 |
124 |
nm->mkNode( |
342 |
|
kind::EQUAL, |
343 |
62 |
nm->mkNode(kind::GEQ, concrete[1], realValue), |
344 |
124 |
nm->mkNode(kind::FLOATINGPOINT_GEQ, abstract, concreteValue))); |
345 |
31 |
handleLemma(fg, InferenceId::FP_PREPROCESS); |
346 |
|
|
347 |
|
Node fl = nm->mkNode( |
348 |
|
kind::IMPLIES, |
349 |
|
correctRoundingMode, |
350 |
124 |
nm->mkNode( |
351 |
|
kind::EQUAL, |
352 |
62 |
nm->mkNode(kind::LEQ, concrete[1], realValue), |
353 |
124 |
nm->mkNode(kind::FLOATINGPOINT_LEQ, abstract, concreteValue))); |
354 |
31 |
handleLemma(fl, InferenceId::FP_PREPROCESS); |
355 |
|
|
356 |
|
// Then the backwards constraints |
357 |
31 |
if (!abstractValue.getConst<FloatingPoint>().isInfinite()) |
358 |
|
{ |
359 |
|
Node realValueOfAbstract = |
360 |
62 |
rewrite(nm->mkNode(kind::FLOATINGPOINT_TO_REAL_TOTAL, |
361 |
|
abstractValue, |
362 |
124 |
nm->mkConst(Rational(0U)))); |
363 |
|
|
364 |
|
Node bg = nm->mkNode( |
365 |
|
kind::IMPLIES, |
366 |
|
correctRoundingMode, |
367 |
124 |
nm->mkNode( |
368 |
|
kind::EQUAL, |
369 |
62 |
nm->mkNode(kind::GEQ, concrete[1], realValueOfAbstract), |
370 |
124 |
nm->mkNode(kind::FLOATINGPOINT_GEQ, abstract, abstractValue))); |
371 |
31 |
handleLemma(bg, InferenceId::FP_PREPROCESS); |
372 |
|
|
373 |
|
Node bl = nm->mkNode( |
374 |
|
kind::IMPLIES, |
375 |
|
correctRoundingMode, |
376 |
124 |
nm->mkNode( |
377 |
|
kind::EQUAL, |
378 |
62 |
nm->mkNode(kind::LEQ, concrete[1], realValueOfAbstract), |
379 |
124 |
nm->mkNode(kind::FLOATINGPOINT_LEQ, abstract, abstractValue))); |
380 |
31 |
handleLemma(bl, InferenceId::FP_PREPROCESS); |
381 |
|
} |
382 |
|
|
383 |
31 |
return true; |
384 |
|
} |
385 |
|
else |
386 |
|
{ |
387 |
|
// No refinement needed |
388 |
6 |
return false; |
389 |
|
} |
390 |
|
} |
391 |
|
else |
392 |
|
{ |
393 |
|
Unreachable() << "Unknown abstraction"; |
394 |
|
} |
395 |
|
|
396 |
|
return false; |
397 |
|
} |
398 |
|
|
399 |
3024 |
void TheoryFp::wordBlastAndEquateTerm(TNode node) |
400 |
|
{ |
401 |
6048 |
Trace("fp-wordBlastTerm") |
402 |
3024 |
<< "TheoryFp::wordBlastTerm(): " << node << std::endl; |
403 |
|
|
404 |
3024 |
size_t oldSize = d_wordBlaster->d_additionalAssertions.size(); |
405 |
|
|
406 |
6048 |
Node wordBlasted(d_wordBlaster->wordBlast(node)); |
407 |
|
|
408 |
3024 |
size_t newSize = d_wordBlaster->d_additionalAssertions.size(); |
409 |
|
|
410 |
3024 |
if (wordBlasted != node) |
411 |
|
{ |
412 |
1612 |
Debug("fp-wordBlastTerm") |
413 |
806 |
<< "TheoryFp::wordBlastTerm(): before " << node << std::endl; |
414 |
1612 |
Debug("fp-wordBlastTerm") |
415 |
806 |
<< "TheoryFp::wordBlastTerm(): after " << wordBlasted << std::endl; |
416 |
|
} |
417 |
|
|
418 |
3024 |
Assert(oldSize <= newSize); |
419 |
|
|
420 |
3404 |
while (oldSize < newSize) |
421 |
|
{ |
422 |
380 |
Node addA = d_wordBlaster->d_additionalAssertions[oldSize]; |
423 |
|
|
424 |
380 |
Debug("fp-wordBlastTerm") |
425 |
190 |
<< "TheoryFp::wordBlastTerm(): additional assertion " << addA |
426 |
190 |
<< std::endl; |
427 |
|
|
428 |
190 |
NodeManager* nm = NodeManager::currentNM(); |
429 |
|
|
430 |
190 |
handleLemma( |
431 |
380 |
nm->mkNode(kind::EQUAL, addA, nm->mkConst(::cvc5::BitVector(1U, 1U))), |
432 |
|
InferenceId::FP_EQUATE_TERM); |
433 |
|
|
434 |
190 |
++oldSize; |
435 |
|
} |
436 |
|
|
437 |
|
// Equate the floating-point atom and the wordBlasted one. |
438 |
|
// Also adds the bit-vectors to the bit-vector solver. |
439 |
3024 |
if (node.getType().isBoolean()) |
440 |
|
{ |
441 |
1253 |
if (wordBlasted != node) |
442 |
|
{ |
443 |
802 |
Assert(wordBlasted.getType().isBitVector()); |
444 |
|
|
445 |
802 |
NodeManager* nm = NodeManager::currentNM(); |
446 |
|
|
447 |
802 |
handleLemma( |
448 |
1604 |
nm->mkNode(kind::EQUAL, |
449 |
|
node, |
450 |
1604 |
nm->mkNode(kind::EQUAL, |
451 |
|
wordBlasted, |
452 |
1604 |
nm->mkConst(::cvc5::BitVector(1U, 1U)))), |
453 |
|
InferenceId::FP_EQUATE_TERM); |
454 |
|
} |
455 |
|
else |
456 |
|
{ |
457 |
451 |
Assert((node.getKind() == kind::EQUAL)); |
458 |
|
} |
459 |
|
} |
460 |
1771 |
else if (node.getType().isBitVector()) |
461 |
|
{ |
462 |
1073 |
if (wordBlasted != node) |
463 |
|
{ |
464 |
4 |
Assert(wordBlasted.getType().isBitVector()); |
465 |
|
|
466 |
4 |
handleLemma( |
467 |
8 |
NodeManager::currentNM()->mkNode(kind::EQUAL, node, wordBlasted), |
468 |
|
InferenceId::FP_EQUATE_TERM); |
469 |
|
} |
470 |
|
} |
471 |
|
|
472 |
6048 |
return; |
473 |
|
} |
474 |
|
|
475 |
10270 |
void TheoryFp::registerTerm(TNode node) |
476 |
|
{ |
477 |
10270 |
Trace("fp-registerTerm") << "TheoryFp::registerTerm(): " << node << std::endl; |
478 |
|
|
479 |
10270 |
Kind k = node.getKind(); |
480 |
10270 |
Assert(k != kind::FLOATINGPOINT_TO_FP_GENERIC && k != kind::FLOATINGPOINT_SUB |
481 |
|
&& k != kind::FLOATINGPOINT_EQ && k != kind::FLOATINGPOINT_GEQ |
482 |
|
&& k != kind::FLOATINGPOINT_GT); |
483 |
|
|
484 |
|
// Add to the equality engine, always. This is required to ensure |
485 |
|
// getEqualityStatus works as expected when theory combination is enabled. |
486 |
10270 |
if (k == kind::EQUAL) |
487 |
|
{ |
488 |
7076 |
d_equalityEngine->addTriggerPredicate(node); |
489 |
|
} |
490 |
|
else |
491 |
|
{ |
492 |
3194 |
d_equalityEngine->addTerm(node); |
493 |
|
} |
494 |
|
|
495 |
|
// if not registered in this user context |
496 |
10270 |
if (isRegistered(node)) |
497 |
|
{ |
498 |
14455 |
return; |
499 |
|
} |
500 |
|
|
501 |
3049 |
CVC5_UNUSED bool success = d_registeredTerms.insert(node); |
502 |
3049 |
Assert(success); |
503 |
|
|
504 |
|
// Give the expansion of classifications in terms of equalities |
505 |
|
// This should make equality reasoning slightly more powerful. |
506 |
3049 |
if ((k == kind::FLOATINGPOINT_ISNAN) || (k == kind::FLOATINGPOINT_ISZ) |
507 |
3008 |
|| (k == kind::FLOATINGPOINT_ISINF)) |
508 |
|
{ |
509 |
100 |
NodeManager* nm = NodeManager::currentNM(); |
510 |
100 |
FloatingPointSize s = node[0].getType().getConst<FloatingPointSize>(); |
511 |
200 |
Node equalityAlias = Node::null(); |
512 |
|
|
513 |
100 |
if (k == kind::FLOATINGPOINT_ISNAN) |
514 |
|
{ |
515 |
32 |
equalityAlias = nm->mkNode( |
516 |
64 |
kind::EQUAL, node[0], nm->mkConst(FloatingPoint::makeNaN(s))); |
517 |
|
} |
518 |
68 |
else if (k == kind::FLOATINGPOINT_ISZ) |
519 |
|
{ |
520 |
27 |
equalityAlias = nm->mkNode( |
521 |
|
kind::OR, |
522 |
18 |
nm->mkNode(kind::EQUAL, |
523 |
|
node[0], |
524 |
18 |
nm->mkConst(FloatingPoint::makeZero(s, true))), |
525 |
18 |
nm->mkNode(kind::EQUAL, |
526 |
|
node[0], |
527 |
18 |
nm->mkConst(FloatingPoint::makeZero(s, false)))); |
528 |
|
} |
529 |
59 |
else if (k == kind::FLOATINGPOINT_ISINF) |
530 |
|
{ |
531 |
59 |
equalityAlias = |
532 |
236 |
nm->mkNode(kind::OR, |
533 |
118 |
nm->mkNode(kind::EQUAL, |
534 |
|
node[0], |
535 |
118 |
nm->mkConst(FloatingPoint::makeInf(s, true))), |
536 |
118 |
nm->mkNode(kind::EQUAL, |
537 |
|
node[0], |
538 |
118 |
nm->mkConst(FloatingPoint::makeInf(s, false)))); |
539 |
|
} |
540 |
|
else |
541 |
|
{ |
542 |
|
Unreachable() << "Only isNaN, isInf and isZero have aliases"; |
543 |
|
} |
544 |
|
|
545 |
100 |
handleLemma(nm->mkNode(kind::EQUAL, node, equalityAlias), |
546 |
100 |
InferenceId::FP_REGISTER_TERM); |
547 |
|
} |
548 |
2949 |
else if (k == kind::FLOATINGPOINT_TO_REAL_TOTAL) |
549 |
|
{ |
550 |
|
// Purify (fp.to_real x) |
551 |
8 |
NodeManager* nm = NodeManager::currentNM(); |
552 |
8 |
SkolemManager* sm = nm->getSkolemManager(); |
553 |
16 |
Node sk = sm->mkPurifySkolem(node, "to_real", "fp purify skolem"); |
554 |
8 |
handleLemma(node.eqNode(sk), InferenceId::FP_REGISTER_TERM); |
555 |
8 |
d_abstractionMap.insert(sk, node); |
556 |
|
|
557 |
|
Node pd = |
558 |
|
nm->mkNode(kind::IMPLIES, |
559 |
32 |
nm->mkNode(kind::OR, |
560 |
16 |
nm->mkNode(kind::FLOATINGPOINT_ISNAN, node[0]), |
561 |
16 |
nm->mkNode(kind::FLOATINGPOINT_ISINF, node[0])), |
562 |
32 |
nm->mkNode(kind::EQUAL, node, node[1])); |
563 |
8 |
handleLemma(pd, InferenceId::FP_REGISTER_TERM); |
564 |
|
|
565 |
|
Node z = |
566 |
|
nm->mkNode(kind::IMPLIES, |
567 |
16 |
nm->mkNode(kind::FLOATINGPOINT_ISZ, node[0]), |
568 |
32 |
nm->mkNode(kind::EQUAL, node, nm->mkConst(Rational(0U)))); |
569 |
8 |
handleLemma(z, InferenceId::FP_REGISTER_TERM); |
570 |
8 |
return; |
571 |
|
|
572 |
|
// TODO : bounds on the output from largest floats, #1914 |
573 |
|
} |
574 |
2941 |
else if (k == kind::FLOATINGPOINT_TO_FP_REAL) |
575 |
|
{ |
576 |
|
// Purify ((_ to_fp eb sb) rm x) |
577 |
5 |
NodeManager* nm = NodeManager::currentNM(); |
578 |
5 |
SkolemManager* sm = nm->getSkolemManager(); |
579 |
10 |
Node sk = sm->mkPurifySkolem(node, "to_real_fp", "fp purify skolem"); |
580 |
5 |
handleLemma(node.eqNode(sk), InferenceId::FP_REGISTER_TERM); |
581 |
5 |
d_abstractionMap.insert(sk, node); |
582 |
|
|
583 |
|
Node nnan = |
584 |
10 |
nm->mkNode(kind::NOT, nm->mkNode(kind::FLOATINGPOINT_ISNAN, node)); |
585 |
5 |
handleLemma(nnan, InferenceId::FP_REGISTER_TERM); |
586 |
|
|
587 |
|
Node z = nm->mkNode( |
588 |
|
kind::IMPLIES, |
589 |
10 |
nm->mkNode(kind::EQUAL, node[1], nm->mkConst(Rational(0U))), |
590 |
10 |
nm->mkNode(kind::EQUAL, |
591 |
|
node, |
592 |
10 |
nm->mkConst(FloatingPoint::makeZero( |
593 |
30 |
node.getType().getConst<FloatingPointSize>(), false)))); |
594 |
5 |
handleLemma(z, InferenceId::FP_REGISTER_TERM); |
595 |
5 |
return; |
596 |
|
|
597 |
|
// TODO : rounding-mode specific bounds on floats that don't give infinity |
598 |
|
// BEWARE of directed rounding! #1914 |
599 |
|
} |
600 |
|
|
601 |
|
/* When not word-blasting lazier, we word-blast every term on |
602 |
|
* registration. */ |
603 |
3036 |
if (!options().fp.fpLazyWb) |
604 |
|
{ |
605 |
2996 |
wordBlastAndEquateTerm(node); |
606 |
|
} |
607 |
|
} |
608 |
|
|
609 |
23618 |
bool TheoryFp::isRegistered(TNode node) |
610 |
|
{ |
611 |
23618 |
return d_registeredTerms.find(node) != d_registeredTerms.end(); |
612 |
|
} |
613 |
|
|
614 |
3979 |
void TheoryFp::preRegisterTerm(TNode node) |
615 |
|
{ |
616 |
3979 |
if (!options().fp.fpExp) |
617 |
|
{ |
618 |
2646 |
TypeNode tn = node.getType(); |
619 |
1323 |
if (tn.isFloatingPoint()) |
620 |
|
{ |
621 |
380 |
unsigned exp_sz = tn.getFloatingPointExponentSize(); |
622 |
380 |
unsigned sig_sz = tn.getFloatingPointSignificandSize(); |
623 |
380 |
if (!((exp_sz == 8 && sig_sz == 24) || (exp_sz == 11 && sig_sz == 53))) |
624 |
|
{ |
625 |
|
std::stringstream ss; |
626 |
|
ss << "FP term " << node << " with type whose size is " << exp_sz << "/" |
627 |
|
<< sig_sz |
628 |
|
<< " is not supported, only Float32 (8/24) or Float64 (11/53) types " |
629 |
|
"are supported in default mode. Try the experimental solver via " |
630 |
|
"--fp-exp. Note: There are known issues with the experimental " |
631 |
|
"solver, use at your own risk."; |
632 |
|
throw LogicException(ss.str()); |
633 |
|
} |
634 |
|
} |
635 |
|
} |
636 |
7958 |
Trace("fp-preRegisterTerm") |
637 |
3979 |
<< "TheoryFp::preRegisterTerm(): " << node << std::endl; |
638 |
3979 |
registerTerm(node); |
639 |
3979 |
return; |
640 |
|
} |
641 |
|
|
642 |
1267 |
void TheoryFp::handleLemma(Node node, InferenceId id) |
643 |
|
{ |
644 |
1267 |
Trace("fp") << "TheoryFp::handleLemma(): asserting " << node << std::endl; |
645 |
1267 |
if (rewrite(node) != d_true) |
646 |
|
{ |
647 |
|
/* We only send non-trivial lemmas. */ |
648 |
1265 |
d_im.lemma(node, id); |
649 |
|
} |
650 |
1267 |
} |
651 |
|
|
652 |
8711 |
bool TheoryFp::propagateLit(TNode node) |
653 |
|
{ |
654 |
8711 |
Trace("fp") << "TheoryFp::propagateLit(): propagate " << node << std::endl; |
655 |
8711 |
return d_im.propagateLit(node); |
656 |
|
} |
657 |
|
|
658 |
20 |
void TheoryFp::conflictEqConstantMerge(TNode t1, TNode t2) |
659 |
|
{ |
660 |
40 |
Trace("fp") << "TheoryFp::conflictEqConstantMerge(): conflict detected" |
661 |
20 |
<< std::endl; |
662 |
20 |
d_im.conflictEqConstantMerge(t1, t2); |
663 |
20 |
} |
664 |
|
|
665 |
8329 |
bool TheoryFp::needsCheckLastEffort() |
666 |
|
{ |
667 |
|
// only need to check if we have added to the abstraction map, otherwise |
668 |
|
// postCheck below is a no-op. |
669 |
8329 |
return !d_abstractionMap.empty(); |
670 |
|
} |
671 |
|
|
672 |
31921 |
void TheoryFp::postCheck(Effort level) |
673 |
|
{ |
674 |
|
/* Resolve the abstractions for the conversion lemmas */ |
675 |
31921 |
if (level == EFFORT_LAST_CALL) |
676 |
|
{ |
677 |
74 |
Trace("fp-abstraction") |
678 |
37 |
<< "TheoryFp::check(): checking abstractions" << std::endl; |
679 |
37 |
TheoryModel* m = getValuation().getModel(); |
680 |
37 |
bool lemmaAdded = false; |
681 |
|
|
682 |
86 |
for (const auto& [abstract, concrete] : d_abstractionMap) |
683 |
|
{ |
684 |
98 |
Trace("fp-abstraction") |
685 |
49 |
<< "TheoryFp::check(): Abstraction: " << abstract << std::endl; |
686 |
49 |
if (m->hasTerm(abstract)) |
687 |
|
{ // Is actually used in the model |
688 |
98 |
Trace("fp-abstraction") |
689 |
49 |
<< "TheoryFp::check(): ... relevant" << std::endl; |
690 |
49 |
lemmaAdded |= refineAbstraction(m, abstract, concrete); |
691 |
|
} |
692 |
|
else |
693 |
|
{ |
694 |
|
Trace("fp-abstraction") |
695 |
|
<< "TheoryFp::check(): ... not relevant" << std::endl; |
696 |
|
} |
697 |
|
} |
698 |
|
} |
699 |
|
|
700 |
31921 |
Trace("fp") << "TheoryFp::check(): completed" << std::endl; |
701 |
|
/* Checking should be handled by the bit-vector engine */ |
702 |
31921 |
} |
703 |
|
|
704 |
9015 |
bool TheoryFp::preNotifyFact( |
705 |
|
TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal) |
706 |
|
{ |
707 |
|
/* Word-blast lazier if configured. */ |
708 |
18030 |
if (options().fp.fpLazyWb |
709 |
18030 |
&& d_wbFactsCache.find(atom) == d_wbFactsCache.end()) |
710 |
|
{ |
711 |
8 |
d_wbFactsCache.insert(atom); |
712 |
8 |
wordBlastAndEquateTerm(atom); |
713 |
|
} |
714 |
|
|
715 |
9015 |
if (atom.getKind() == kind::EQUAL) |
716 |
|
{ |
717 |
6291 |
Assert(!(atom[0].getType().isFloatingPoint() |
718 |
|
|| atom[0].getType().isRoundingMode()) |
719 |
|
|| isRegistered(atom[0])); |
720 |
6291 |
Assert(!(atom[1].getType().isFloatingPoint() |
721 |
|
|| atom[1].getType().isRoundingMode()) |
722 |
|
|| isRegistered(atom[1])); |
723 |
6291 |
registerTerm(atom); // Needed for float equalities |
724 |
|
} |
725 |
|
else |
726 |
|
{ |
727 |
|
// A system-wide invariant; predicates are registered before they are |
728 |
|
// asserted |
729 |
2724 |
Assert(isRegistered(atom)); |
730 |
|
|
731 |
2724 |
if (!d_equalityEngine->isFunctionKind(atom.getKind())) |
732 |
|
{ |
733 |
|
return true; |
734 |
|
} |
735 |
|
} |
736 |
9015 |
return false; |
737 |
|
} |
738 |
|
|
739 |
1115 |
void TheoryFp::notifySharedTerm(TNode n) |
740 |
|
{ |
741 |
|
/* Word-blast lazier if configured. */ |
742 |
1115 |
if (options().fp.fpLazyWb && d_wbFactsCache.find(n) == d_wbFactsCache.end()) |
743 |
|
{ |
744 |
20 |
d_wbFactsCache.insert(n); |
745 |
20 |
wordBlastAndEquateTerm(n); |
746 |
|
} |
747 |
1115 |
} |
748 |
|
|
749 |
14 |
TrustNode TheoryFp::explain(TNode n) |
750 |
|
{ |
751 |
14 |
Trace("fp") << "TheoryFp::explain(): explain " << n << std::endl; |
752 |
|
|
753 |
|
// All things we assert directly (and not via bit-vector) should |
754 |
|
// come from the equality engine so this should be sufficient... |
755 |
28 |
std::vector<TNode> assumptions; |
756 |
|
|
757 |
14 |
bool polarity = n.getKind() != kind::NOT; |
758 |
28 |
TNode atom = polarity ? n : n[0]; |
759 |
14 |
if (atom.getKind() == kind::EQUAL) { |
760 |
14 |
d_equalityEngine->explainEquality(atom[0], atom[1], polarity, assumptions); |
761 |
|
} else { |
762 |
|
d_equalityEngine->explainPredicate(atom, polarity, assumptions); |
763 |
|
} |
764 |
|
|
765 |
28 |
Node exp = helper::buildConjunct(assumptions); |
766 |
28 |
return TrustNode::mkTrustPropExp(n, exp, nullptr); |
767 |
|
} |
768 |
|
|
769 |
|
Node TheoryFp::getModelValue(TNode var) { |
770 |
|
return d_wordBlaster->getValue(d_valuation, var); |
771 |
|
} |
772 |
|
|
773 |
7274 |
bool TheoryFp::collectModelInfo(TheoryModel* m, |
774 |
|
const std::set<Node>& relevantTerms) |
775 |
|
{ |
776 |
|
// this override behavior to not assert equality engine |
777 |
7274 |
return collectModelValues(m, relevantTerms); |
778 |
|
} |
779 |
|
|
780 |
7274 |
bool TheoryFp::collectModelValues(TheoryModel* m, |
781 |
|
const std::set<Node>& relevantTerms) |
782 |
|
{ |
783 |
14548 |
Trace("fp-collectModelInfo") |
784 |
7274 |
<< "TheoryFp::collectModelInfo(): begin" << std::endl; |
785 |
7274 |
if (Trace.isOn("fp-collectModelInfo")) { |
786 |
|
for (std::set<Node>::const_iterator i(relevantTerms.begin()); |
787 |
|
i != relevantTerms.end(); ++i) { |
788 |
|
Trace("fp-collectModelInfo") |
789 |
|
<< "TheoryFp::collectModelInfo(): relevantTerms " << *i << std::endl; |
790 |
|
} |
791 |
|
} |
792 |
|
|
793 |
14548 |
std::unordered_set<TNode> visited; |
794 |
14548 |
std::vector<TNode> working; |
795 |
14548 |
std::set<TNode> relevantVariables; |
796 |
18897 |
for (const Node& n : relevantTerms) |
797 |
|
{ |
798 |
11623 |
working.emplace_back(n); |
799 |
|
} |
800 |
|
|
801 |
50216 |
while (!working.empty()) { |
802 |
33362 |
TNode current = working.back(); |
803 |
21471 |
working.pop_back(); |
804 |
|
|
805 |
21471 |
if (visited.find(current) != visited.end()) |
806 |
|
{ |
807 |
|
// Ignore things that have already been explored |
808 |
9580 |
continue; |
809 |
|
} |
810 |
11891 |
visited.insert(current); |
811 |
|
|
812 |
23782 |
TypeNode t = current.getType(); |
813 |
|
|
814 |
11891 |
if ((t.isRoundingMode() || t.isFloatingPoint()) && this->isLeaf(current)) |
815 |
|
{ |
816 |
4311 |
relevantVariables.insert(current); |
817 |
|
} |
818 |
|
|
819 |
11891 |
working.insert(working.end(), current.begin(), current.end()); |
820 |
|
} |
821 |
|
|
822 |
11585 |
for (const TNode& node : relevantVariables) |
823 |
|
{ |
824 |
8622 |
Trace("fp-collectModelInfo") |
825 |
4311 |
<< "TheoryFp::collectModelInfo(): relevantVariable " << node |
826 |
4311 |
<< std::endl; |
827 |
|
|
828 |
8622 |
Node wordBlasted = d_wordBlaster->getValue(d_valuation, node); |
829 |
|
// We only assign the value if the FpWordBlaster actually has one, that is, |
830 |
|
// if FpWordBlaster::getValue() does not return a null node. |
831 |
4311 |
if (!wordBlasted.isNull() && !m->assertEquality(node, wordBlasted, true)) |
832 |
|
{ |
833 |
|
Trace("fp-collectModelInfo") |
834 |
|
<< "TheoryFp::collectModelInfo(): ... not converted" << std::endl; |
835 |
|
return false; |
836 |
|
} |
837 |
|
|
838 |
12933 |
if (Configuration::isAssertionBuild() && isLeaf(node) && !node.isConst() |
839 |
9369 |
&& node.getType().isFloatingPoint()) |
840 |
|
{ |
841 |
|
// Check that the equality engine has asssigned values to all the |
842 |
|
// components of `node` except `(sign node)` (the sign component is |
843 |
|
// assignable, meaning that the model builder can pick an arbitrary value |
844 |
|
// for it if it hasn't been assigned in the equality engine). |
845 |
740 |
NodeManager* nm = NodeManager::currentNM(); |
846 |
1480 |
Node compNaN = nm->mkNode(kind::FLOATINGPOINT_COMPONENT_NAN, node); |
847 |
1480 |
Node compInf = nm->mkNode(kind::FLOATINGPOINT_COMPONENT_INF, node); |
848 |
1480 |
Node compZero = nm->mkNode(kind::FLOATINGPOINT_COMPONENT_ZERO, node); |
849 |
|
Node compExponent = |
850 |
1480 |
nm->mkNode(kind::FLOATINGPOINT_COMPONENT_EXPONENT, node); |
851 |
|
Node compSignificand = |
852 |
1480 |
nm->mkNode(kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND, node); |
853 |
|
|
854 |
740 |
eq::EqualityEngine* ee = m->getEqualityEngine(); |
855 |
740 |
Assert(ee->hasTerm(compNaN) && ee->getRepresentative(compNaN).isConst()); |
856 |
740 |
Assert(ee->hasTerm(compInf) && ee->getRepresentative(compInf).isConst()); |
857 |
740 |
Assert(ee->hasTerm(compZero) |
858 |
|
&& ee->getRepresentative(compZero).isConst()); |
859 |
740 |
Assert(ee->hasTerm(compExponent) |
860 |
|
&& ee->getRepresentative(compExponent).isConst()); |
861 |
740 |
Assert(ee->hasTerm(compSignificand)); |
862 |
740 |
Assert(ee->getRepresentative(compSignificand).isConst()); |
863 |
|
|
864 |
|
// At most one of the flags (NaN, inf, zero) can be set |
865 |
1480 |
Node one = nm->mkConst(BitVector(1U, 1U)); |
866 |
740 |
size_t numFlags = 0; |
867 |
740 |
numFlags += ee->getRepresentative(compNaN) == one ? 1 : 0; |
868 |
740 |
numFlags += ee->getRepresentative(compInf) == one ? 1 : 0; |
869 |
740 |
numFlags += ee->getRepresentative(compZero) == one ? 1 : 0; |
870 |
740 |
Assert(numFlags <= 1); |
871 |
|
} |
872 |
|
} |
873 |
|
|
874 |
7274 |
return true; |
875 |
|
} |
876 |
|
|
877 |
7490 |
bool TheoryFp::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, |
878 |
|
bool value) { |
879 |
14980 |
Debug("fp-eq") |
880 |
7490 |
<< "TheoryFp::eqNotifyTriggerPredicate(): call back as predicate " |
881 |
7490 |
<< predicate << " is " << value << std::endl; |
882 |
|
|
883 |
7490 |
if (value) { |
884 |
1729 |
return d_theorySolver.propagateLit(predicate); |
885 |
|
} |
886 |
5761 |
return d_theorySolver.propagateLit(predicate.notNode()); |
887 |
|
} |
888 |
|
|
889 |
1221 |
bool TheoryFp::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, |
890 |
|
TNode t2, bool value) { |
891 |
2442 |
Debug("fp-eq") << "TheoryFp::eqNotifyTriggerTermEquality(): call back as " |
892 |
1221 |
<< t1 << (value ? " = " : " != ") << t2 << std::endl; |
893 |
|
|
894 |
1221 |
if (value) { |
895 |
1021 |
return d_theorySolver.propagateLit(t1.eqNode(t2)); |
896 |
|
} |
897 |
200 |
return d_theorySolver.propagateLit(t1.eqNode(t2).notNode()); |
898 |
|
} |
899 |
|
|
900 |
20 |
void TheoryFp::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2) { |
901 |
40 |
Debug("fp-eq") << "TheoryFp::eqNotifyConstantTermMerge(): call back as " << t1 |
902 |
20 |
<< " = " << t2 << std::endl; |
903 |
20 |
d_theorySolver.conflictEqConstantMerge(t1, t2); |
904 |
20 |
} |
905 |
|
|
906 |
|
} // namespace fp |
907 |
|
} // namespace theory |
908 |
31125 |
} // namespace cvc5 |