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