Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * The Evaluator class.
11 : : */
12 : :
13 : : #include "theory/evaluator.h"
14 : :
15 : : #include <cmath>
16 : :
17 : : #include "theory/builtin/theory_builtin_rewriter.h"
18 : : #include "theory/bv/theory_bv_utils.h"
19 : : #include "theory/rewriter.h"
20 : : #include "theory/strings/theory_strings_utils.h"
21 : : #include "theory/theory.h"
22 : : #include "theory/uf/function_const.h"
23 : : #include "util/integer.h"
24 : :
25 : : using namespace cvc5::internal::kind;
26 : :
27 : : namespace cvc5::internal {
28 : : namespace theory {
29 : :
30 : 7713046 : EvalResult::EvalResult(const EvalResult& other)
31 : : {
32 : 7713046 : d_tag = other.d_tag;
33 [ + + ][ + + ]: 7713046 : switch (d_tag)
[ + + ][ - ]
34 : : {
35 : 2374910 : case BOOL: d_bool = other.d_bool; break;
36 : 254699 : case BITVECTOR:
37 : 254699 : new (&d_bv) BitVector;
38 : 254699 : d_bv = other.d_bv;
39 : 254699 : break;
40 : 2546681 : case RATIONAL:
41 : 2546681 : new (&d_rat) Rational;
42 : 2546681 : d_rat = other.d_rat;
43 : 2546681 : break;
44 : 27248 : case STRING:
45 : 27248 : new (&d_str) String;
46 : 27248 : d_str = other.d_str;
47 : 27248 : break;
48 : 59 : case UVALUE: new (&d_av) UninterpretedSortValue(other.d_av); break;
49 : 2509449 : case INVALID: break;
50 : : }
51 : 7713046 : }
52 : :
53 : 44184667 : EvalResult& EvalResult::operator=(const EvalResult& other)
54 : : {
55 [ + - ]: 44184667 : if (this != &other)
56 : : {
57 : 44184667 : d_tag = other.d_tag;
58 [ + + ][ + + ]: 44184667 : switch (d_tag)
[ + + ][ - ]
59 : : {
60 : 14244324 : case BOOL: d_bool = other.d_bool; break;
61 : 1329568 : case BITVECTOR:
62 : 1329568 : new (&d_bv) BitVector;
63 : 1329568 : d_bv = other.d_bv;
64 : 1329568 : break;
65 : 4926445 : case RATIONAL:
66 : 4926445 : new (&d_rat) Rational;
67 : 4926445 : d_rat = other.d_rat;
68 : 4926445 : break;
69 : 217999 : case STRING:
70 : 217999 : new (&d_str) String;
71 : 217999 : d_str = other.d_str;
72 : 217999 : break;
73 : 169 : case UVALUE: new (&d_av) UninterpretedSortValue(other.d_av); break;
74 : 23466162 : case INVALID: break;
75 : : }
76 : : }
77 : 44184667 : return *this;
78 : : }
79 : :
80 : 93404221 : EvalResult::~EvalResult()
81 : : {
82 [ + + ][ + + ]: 93404221 : switch (d_tag)
[ + ]
83 : : {
84 : 2887950 : case BITVECTOR:
85 : : {
86 : 2887950 : d_bv.~BitVector();
87 : 2887950 : break;
88 : : }
89 : 12386517 : case RATIONAL:
90 : : {
91 : 12386517 : d_rat.~Rational();
92 : 12386517 : break;
93 : : }
94 : 463072 : case STRING:
95 : : {
96 : 463072 : d_str.~String();
97 : 463072 : break;
98 : : }
99 : 397 : case UVALUE:
100 : : {
101 : 397 : d_av.~UninterpretedSortValue();
102 : 397 : break;
103 : : }
104 : 77666285 : default: break;
105 : : }
106 : 93404221 : }
107 : :
108 : 10008413 : Node EvalResult::toNode(const TypeNode& tn) const
109 : : {
110 : 10008413 : NodeManager* nm = tn.getNodeManager();
111 [ + + ][ + + ]: 10008413 : switch (d_tag)
[ + + ]
112 : : {
113 : 3460403 : case EvalResult::BOOL: return nm->mkConst(d_bool);
114 : 844646 : case EvalResult::BITVECTOR: return nm->mkConst(d_bv);
115 : 2959592 : case EvalResult::RATIONAL:
116 [ - + ][ - + ]: 2959592 : Assert(!tn.isNull());
[ - - ]
117 : 2959592 : return nm->mkConstRealOrInt(tn, d_rat);
118 : 234885 : case EvalResult::STRING: return nm->mkConst(d_str);
119 : 149 : case EvalResult::UVALUE: return nm->mkConst(d_av);
120 : 2508738 : default:
121 : : {
122 [ + - ]: 5017476 : Trace("evaluator") << "Missing conversion from " << d_tag << " to node"
123 : 2508738 : << std::endl;
124 : 2508738 : return Node();
125 : : }
126 : : }
127 : : }
128 : :
129 : 1639276 : Evaluator::Evaluator(Rewriter* rr, uint32_t alphaCard)
130 : 1639276 : : d_rr(rr), d_alphaCard(alphaCard)
131 : : {
132 : 1639276 : }
133 : :
134 : 2362645 : Node Evaluator::eval(TNode n,
135 : : const std::vector<Node>& args,
136 : : const std::vector<Node>& vals) const
137 : : {
138 : 2362645 : std::unordered_map<Node, Node> visited;
139 : 4725290 : return eval(n, args, vals, visited);
140 : 2362645 : }
141 : 4060769 : Node Evaluator::eval(TNode n,
142 : : const std::vector<Node>& args,
143 : : const std::vector<Node>& vals,
144 : : const std::unordered_map<Node, Node>& visited) const
145 : : {
146 [ + - ]: 8121538 : Trace("evaluator") << "Evaluating " << n << " under substitution " << args
147 : 4060769 : << " " << vals << " with visited size = " << visited.size()
148 : 4060769 : << std::endl;
149 : 4060769 : std::unordered_map<TNode, Node> evalAsNode;
150 : 4060769 : std::unordered_map<TNode, EvalResult> results;
151 : : // add visited to results
152 [ + + ]: 4082543 : for (const std::pair<const Node, Node>& p : visited)
153 : : {
154 [ + - ]: 21774 : Trace("evaluator") << "Add " << p.first << " == " << p.second << std::endl;
155 : 21774 : results[p.first] = evalInternal(p.second, args, vals, evalAsNode, results);
156 [ + + ]: 21774 : if (results[p.first].d_tag == EvalResult::INVALID)
157 : : {
158 : : // could not evaluate, use the evalAsNode map
159 : 711 : std::unordered_map<TNode, Node>::iterator itn = evalAsNode.find(p.second);
160 [ - + ][ - + ]: 711 : Assert(itn != evalAsNode.end());
[ - - ]
161 : 711 : Node val = itn->second;
162 [ + - ]: 711 : if (d_rr != nullptr)
163 : : {
164 : 711 : val = d_rr->rewrite(val);
165 : : }
166 : 711 : evalAsNode[p.first] = val;
167 : 711 : }
168 : : }
169 [ + - ]: 4060769 : Trace("evaluator") << "Run eval internal..." << std::endl;
170 : : Node ret =
171 : 8121538 : evalInternal(n, args, vals, evalAsNode, results).toNode(n.getType());
172 : : // if we failed to evaluate
173 [ + + ]: 4060769 : if (d_rr != nullptr)
174 : : {
175 [ + + ]: 959285 : if (ret.isNull())
176 : : {
177 : : // should be stored in the evaluation-as-node map
178 : 33069 : std::unordered_map<TNode, Node>::iterator itn = evalAsNode.find(n);
179 [ - + ][ - + ]: 33069 : Assert(itn != evalAsNode.end());
[ - - ]
180 : 33069 : ret = itn->second;
181 : : }
182 : : // always rewrite, which can change if the evaluation was not a constant
183 : 959285 : ret = d_rr->rewrite(ret);
184 : : }
185 : : // should be the same as substitution + rewriting, or possibly null if
186 : : // d_rr is nullptr or non-constant
187 : 4060769 : Assert(ret.isNull() || !ret.isConst() || d_rr == nullptr
188 : : || ret
189 : : == d_rr->rewrite(n.substitute(
190 : : args.begin(), args.end(), vals.begin(), vals.end())));
191 : 8121538 : return ret;
192 : 4060769 : }
193 : :
194 : 4158886 : EvalResult Evaluator::evalInternal(
195 : : TNode n,
196 : : const std::vector<Node>& args,
197 : : const std::vector<Node>& vals,
198 : : std::unordered_map<TNode, Node>& evalAsNode,
199 : : std::unordered_map<TNode, EvalResult>& results) const
200 : : {
201 : 4158886 : std::vector<TNode> queue;
202 : 4158886 : queue.emplace_back(n);
203 : 4158886 : std::unordered_map<TNode, EvalResult>::iterator itr;
204 : :
205 [ + + ]: 74784039 : while (queue.size() != 0)
206 : : {
207 : 70625153 : TNode currNode = queue.back();
208 : :
209 [ + + ]: 70625153 : if (results.find(currNode) != results.end())
210 : : {
211 : 1831488 : queue.pop_back();
212 : 1831488 : continue;
213 : : }
214 : :
215 : 68793665 : bool doProcess = true;
216 : 68793665 : bool isVar = false;
217 : 68793665 : bool doEval = true;
218 [ + + ]: 68793665 : if (currNode.isVar())
219 : : {
220 : : // we do not evaluate if we are a variable, instead we look for the
221 : : // variable in args below
222 : 8720042 : isVar = true;
223 : 8720042 : doEval = false;
224 : : }
225 [ + + ]: 60073623 : else if (currNode.getMetaKind() == kind::metakind::PARAMETERIZED)
226 : : {
227 : 3384595 : TNode op = currNode.getOperator();
228 : : // Certain nodes are parameterized with constant operators, including
229 : : // bitvector extract. These operators do not need to be evaluated.
230 [ + + ]: 3384595 : if (!op.isConst())
231 : : {
232 : 1226854 : itr = results.find(op);
233 [ + + ]: 1226854 : if (itr == results.end())
234 : : {
235 : 344753 : queue.emplace_back(op);
236 : 344753 : doProcess = false;
237 : : }
238 [ + - ]: 882101 : else if (itr->second.d_tag == EvalResult::INVALID)
239 : : {
240 : 882101 : doEval = false;
241 : : }
242 : : }
243 [ + + ]: 2157741 : else if (currNode.getKind() == Kind::APPLY_INDEXED_SYMBOLIC)
244 : : {
245 : : // we require special handling below to deal with symbolic indexed
246 : : // operators.
247 : 130221 : doEval = false;
248 : : }
249 : 3384595 : }
250 [ + + ]: 194377204 : for (const auto& currNodeChild : currNode)
251 : : {
252 : 125583539 : itr = results.find(currNodeChild);
253 [ + + ]: 125583539 : if (itr == results.end())
254 : : {
255 : 41489955 : queue.emplace_back(currNodeChild);
256 : 41489955 : doProcess = false;
257 : : }
258 [ + + ]: 84093584 : else if (itr->second.d_tag == EvalResult::INVALID)
259 : : {
260 : : // we cannot evaluate since there was an invalid child
261 : 36972025 : doEval = false;
262 : : }
263 : 125583539 : }
264 [ + - ]: 137587330 : Trace("evaluator") << "Evaluator: visit " << currNode
265 : 0 : << ", process = " << doProcess
266 : 68793665 : << ", evaluate = " << doEval << std::endl;
267 : :
268 [ + + ]: 68793665 : if (doProcess)
269 : : {
270 : 44162106 : queue.pop_back();
271 : :
272 : 44162106 : Node currNodeVal = currNode;
273 : : // whether we need to reconstruct the current node in the case of failure
274 : 44162106 : bool needsReconstruct = true;
275 : :
276 : : // The code below should either:
277 : : // (1) store a valid EvalResult into results[currNode], or
278 : : // (2) store an invalid EvalResult into results[currNode] and
279 : : // store the result of substitution + rewriting currNode { args -> vals }
280 : : // into evalAsNode[currNode].
281 : :
282 : : // If we did not successfully evaluate all children, or are a variable
283 [ + + ]: 44162106 : if (!doEval)
284 : : {
285 [ + + ]: 27773370 : if (isVar)
286 : : {
287 : 8720042 : const auto& it = std::find(args.begin(), args.end(), currNode);
288 [ + + ]: 8720042 : if (it == args.end())
289 : : {
290 : : // variable with no substitution is itself
291 : 4393004 : evalAsNode[currNode] = currNode;
292 : 4393004 : results[currNode] = EvalResult();
293 : 4393004 : continue;
294 : : }
295 : 4327038 : ptrdiff_t pos = std::distance(args.begin(), it);
296 : 4327038 : currNodeVal = vals[pos];
297 : : // Don't need to rewrite since range of substitution should already
298 : : // be normalized.
299 : : }
300 : : else
301 : : {
302 : : // Reconstruct the node with a combination of the children that
303 : : // successfully evaluated, and the children that did not.
304 [ + - ]: 19053328 : Trace("evaluator") << "Evaluator: collect arguments" << std::endl;
305 : 19053328 : currNodeVal = reconstruct(currNodeVal, results, evalAsNode);
306 [ + + ]: 19053328 : if (d_rr != nullptr)
307 : : {
308 : : // Rewrite the result now, if we use the rewriter. We will see below
309 : : // if we are able to turn it into a valid EvalResult.
310 : 456437 : currNodeVal = d_rr->rewrite(currNodeVal);
311 : : }
312 [ + + ]: 18596891 : else if (currNodeVal.getKind() == Kind::APPLY_INDEXED_SYMBOLIC)
313 : : {
314 : : // To evaluate a symbolic indexed application, we reconstruct
315 : : // the node here, and verify that all its arguments are constant
316 : : // using rewriteApplyIndexedSymbolic.
317 : : // If successful, we evaluate the result in a separate recursive
318 : : // call, which will only recurse once.
319 : : Node rr =
320 : : builtin::TheoryBuiltinRewriter::rewriteApplyIndexedSymbolic(
321 : 55050 : currNodeVal);
322 [ + + ]: 55050 : if (rr != currNodeVal)
323 : : {
324 : 10743 : Node rre = eval(rr, args, vals);
325 : : // only take value if we successfully evaluated, otherwise
326 : : // it will remain APPLY_INDEXED_SYMBOLIC and fail below.
327 [ + + ]: 10743 : if (!rre.isNull())
328 : : {
329 : 10011 : currNodeVal = rre;
330 : : }
331 : 10743 : }
332 : 55050 : }
333 : : }
334 : 23380366 : needsReconstruct = false;
335 [ + - ]: 46760732 : Trace("evaluator") << "Evaluator: now after substitution + rewriting: "
336 : 23380366 : << currNodeVal << std::endl;
337 : 23380366 : if (currNodeVal.getNumChildren() > 0
338 [ + + ][ + + ]: 23380366 : && currNodeVal.getKind() != Kind::BITVECTOR_SIZE)
[ + + ]
339 : : {
340 : : // We may continue with a valid EvalResult at this point only if
341 : : // we have no children. We must otherwise fail here since some of
342 : : // our children may not have successful evaluations.
343 : : // bvsize is a rare exception to this, where the evaluation does
344 : : // not depend on the value of the argument.
345 : 18970722 : results[currNode] = EvalResult();
346 : 18970722 : evalAsNode[currNode] = currNodeVal;
347 : 18970722 : continue;
348 : : }
349 : : // Otherwise, we may be able to turn the overall result into an
350 : : // valid EvalResult and continue. We fallthrough and continue with the
351 : : // block of code below.
352 : : }
353 : :
354 [ + - ]: 20798380 : Trace("evaluator") << "Current node val : " << currNodeVal << std::endl;
355 : :
356 [ + + ][ + + ]: 20798380 : switch (currNodeVal.getKind())
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + - ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ]
357 : : {
358 : : // APPLY_UF is a special case where we look up the operator and apply
359 : : // beta reduction if possible
360 : 76343 : case Kind::APPLY_UF:
361 : : {
362 [ + - ]: 76343 : Trace("evaluator") << "Evaluate " << currNode << std::endl;
363 : 76343 : TNode op = currNode.getOperator();
364 [ + - ]: 76343 : if (op.getKind() == Kind::FUNCTION_ARRAY_CONST)
365 : : {
366 : : // If we have a function constant as the operator, it was not
367 : : // processed. We require converting to a lambda now.
368 : 76343 : op = uf::FunctionConst::toLambda(op);
369 : : }
370 : : else
371 : : {
372 : 0 : Assert(evalAsNode.find(op) != evalAsNode.end());
373 : : // no function can be a valid EvalResult
374 : 0 : op = evalAsNode[op];
375 : : }
376 [ + - ]: 76343 : Trace("evaluator") << "Operator evaluated to " << op << std::endl;
377 [ - + ]: 76343 : if (op.getKind() != Kind::LAMBDA)
378 : : {
379 : : // this node is not evaluatable due to operator, must add to
380 : : // evalAsNode
381 : 0 : results[currNode] = EvalResult();
382 : 0 : evalAsNode[currNode] = reconstruct(currNode, results, evalAsNode);
383 : 0 : continue;
384 : : }
385 : : // Create a copy of the current substitutions
386 : 76343 : std::vector<Node> lambdaArgs(args);
387 : 76343 : std::vector<Node> lambdaVals(vals);
388 : :
389 : : // Add the values for the arguments of the lambda as substitutions at
390 : : // the beginning of the vector to shadow variables from outer scopes
391 : : // with the same name
392 [ + + ]: 209556 : for (const auto& lambdaArg : op[0])
393 : : {
394 : 133213 : lambdaArgs.insert(lambdaArgs.begin(), lambdaArg);
395 : 209556 : }
396 : :
397 [ + + ]: 209556 : for (const auto& lambdaVal : currNode)
398 : : {
399 : 133213 : lambdaVals.insert(lambdaVals.begin(),
400 : 266426 : results[lambdaVal].toNode(lambdaVal.getType()));
401 : 133213 : }
402 : :
403 : : // Lambdas are evaluated in a recursive fashion because each
404 : : // evaluation requires different substitutions. We use a fresh cache
405 : : // since the evaluation of op[1] is under a new substitution and
406 : : // thus should not be cached. We could alternatively copy evalAsNode
407 : : // to evalAsNodeC but favor avoiding this copy for performance
408 : : // reasons.
409 : 76343 : std::unordered_map<TNode, Node> evalAsNodeC;
410 : 76343 : std::unordered_map<TNode, EvalResult> resultsC;
411 : 152686 : results[currNode] = evalInternal(
412 : 76343 : op[1], lambdaArgs, lambdaVals, evalAsNodeC, resultsC);
413 [ + - ]: 152686 : Trace("evaluator") << "Evaluated via arguments to "
414 : 76343 : << results[currNode].d_tag << std::endl;
415 [ - + ]: 76343 : if (results[currNode].d_tag == EvalResult::INVALID)
416 : : {
417 : : // evaluation was invalid, we take the node of op[1] as the result
418 : 0 : evalAsNode[currNode] = evalAsNodeC[op[1]];
419 [ - - ]: 0 : Trace("evaluator")
420 : 0 : << "Take node evaluation: " << evalAsNodeC[op[1]] << std::endl;
421 : : }
422 [ + - ]: 76343 : }
423 : 76343 : break;
424 : 3834131 : case Kind::CONST_BOOLEAN:
425 : 3834131 : results[currNode] = EvalResult(currNodeVal.getConst<bool>());
426 : 3834131 : break;
427 : :
428 : 2375538 : case Kind::NOT:
429 : : {
430 : 2375538 : results[currNode] = EvalResult(!(results[currNode[0]].d_bool));
431 : 2375538 : break;
432 : : }
433 : :
434 : 1311049 : case Kind::AND:
435 : : {
436 : 1311049 : bool res = results[currNode[0]].d_bool;
437 [ + + ]: 2728796 : for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
438 : : {
439 [ + + ][ + + ]: 1417747 : res = res && results[currNode[i]].d_bool;
[ + + ][ - - ]
440 : : }
441 : 1311049 : results[currNode] = EvalResult(res);
442 : 1311049 : break;
443 : : }
444 : :
445 : 1644968 : case Kind::OR:
446 : : {
447 : 1644968 : bool res = results[currNode[0]].d_bool;
448 [ + + ]: 7934917 : for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
449 : : {
450 [ + + ][ + + ]: 6289949 : res = res || results[currNode[i]].d_bool;
[ + + ][ - - ]
451 : : }
452 : 1644968 : results[currNode] = EvalResult(res);
453 : 1644968 : break;
454 : : }
455 : 501 : case Kind::IMPLIES:
456 : : {
457 : : bool res =
458 : 501 : !results[currNode[0]].d_bool || results[currNode[1]].d_bool;
459 : 501 : results[currNode] = EvalResult(res);
460 : 501 : break;
461 : : }
462 : 23429 : case Kind::XOR:
463 : : {
464 : 23429 : bool res = results[currNode[0]].d_bool;
465 [ + + ]: 46858 : for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
466 : : {
467 : 23429 : res = res != results[currNode[i]].d_bool;
468 : : }
469 : 23429 : results[currNode] = EvalResult(res);
470 : 23429 : break;
471 : : }
472 : :
473 : 3284952 : case Kind::CONST_RATIONAL:
474 : : case Kind::CONST_INTEGER:
475 : : {
476 : 3284952 : const Rational& r = currNodeVal.getConst<Rational>();
477 : 3284952 : results[currNode] = EvalResult(r);
478 : 3284952 : break;
479 : : }
480 : 169 : case Kind::UNINTERPRETED_SORT_VALUE:
481 : : {
482 : : const UninterpretedSortValue& av =
483 : 169 : currNodeVal.getConst<UninterpretedSortValue>();
484 : 169 : results[currNode] = EvalResult(av);
485 : 169 : break;
486 : : }
487 : 793444 : case Kind::ADD:
488 : : {
489 : 793444 : Rational res = results[currNode[0]].d_rat;
490 [ + + ]: 2072336 : for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
491 : : {
492 : 1278892 : res = res + results[currNode[i]].d_rat;
493 : : }
494 : 793444 : results[currNode] = EvalResult(res);
495 : 793444 : break;
496 : 793444 : }
497 : :
498 : 52458 : case Kind::SUB:
499 : : {
500 : 52458 : const Rational& x = results[currNode[0]].d_rat;
501 : 52458 : const Rational& y = results[currNode[1]].d_rat;
502 : 52458 : results[currNode] = EvalResult(x - y);
503 : 52458 : break;
504 : : }
505 : :
506 : 13774 : case Kind::NEG:
507 : : {
508 : 13774 : const Rational& x = results[currNode[0]].d_rat;
509 : 13774 : results[currNode] = EvalResult(-x);
510 : 13774 : break;
511 : : }
512 : 605625 : case Kind::MULT:
513 : : case Kind::NONLINEAR_MULT:
514 : : {
515 : 605625 : Rational res = results[currNode[0]].d_rat;
516 [ + + ]: 1211927 : for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
517 : : {
518 : 606302 : res = res * results[currNode[i]].d_rat;
519 : : }
520 : 605625 : results[currNode] = EvalResult(res);
521 : 605625 : break;
522 : 605625 : }
523 : 76058 : case Kind::DIVISION:
524 : : case Kind::DIVISION_TOTAL:
525 : : case Kind::INTS_DIVISION:
526 : : case Kind::INTS_DIVISION_TOTAL:
527 : : case Kind::INTS_MODULUS:
528 : : case Kind::INTS_MODULUS_TOTAL:
529 : : {
530 : 76058 : Rational res = results[currNode[0]].d_rat;
531 : 76058 : bool divbyzero = false;
532 : 76058 : Kind k = currNodeVal.getKind();
533 [ + + ][ + + ]: 76058 : bool isReal = (k == Kind::DIVISION || k == Kind::DIVISION_TOTAL);
534 : 76058 : bool isMod =
535 [ + + ][ + + ]: 76058 : (k == Kind::INTS_MODULUS || k == Kind::INTS_MODULUS_TOTAL);
536 [ + + ]: 151329 : for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
537 : : {
538 [ + + ]: 76058 : if (results[currNode[i]].d_rat.isZero())
539 : : {
540 [ + + ][ + + ]: 807 : if (k == Kind::DIVISION_TOTAL || k == Kind::INTS_DIVISION_TOTAL)
541 : : {
542 : 20 : res = Rational(0);
543 : 20 : continue;
544 : : }
545 [ - + ]: 787 : else if (k == Kind::INTS_MODULUS_TOTAL)
546 : : {
547 : : // result is unchanged
548 : 0 : continue;
549 : : }
550 : : else
551 : : {
552 [ + - ]: 1574 : Trace("evaluator")
553 : 787 : << "Division/modulus by zero not supported" << std::endl;
554 : 787 : divbyzero = true;
555 : 787 : results[currNode] = EvalResult();
556 : 787 : break;
557 : : }
558 : : }
559 [ + + ]: 75251 : if (isReal)
560 : : {
561 : 65206 : res = res / results[currNode[i]].d_rat;
562 : : }
563 : : else
564 : : {
565 : 10045 : Integer a = res.getNumerator();
566 : 10045 : Integer b = results[currNode[i]].d_rat.getNumerator();
567 [ + + ]: 20090 : res = Rational(isMod ? a.euclidianDivideRemainder(b)
568 : 10045 : : a.euclidianDivideQuotient(b));
569 : 10045 : }
570 : : }
571 [ + + ]: 76058 : if (divbyzero)
572 : : {
573 : 787 : processUnhandled(
574 : : currNode, currNodeVal, evalAsNode, results, needsReconstruct);
575 : : }
576 : : else
577 : : {
578 : 75271 : results[currNode] = EvalResult(res);
579 : : }
580 : 76058 : break;
581 : 76058 : }
582 : 510499 : case Kind::GEQ:
583 : : {
584 : 510499 : const Rational& x = results[currNode[0]].d_rat;
585 : 510499 : const Rational& y = results[currNode[1]].d_rat;
586 : 510499 : results[currNode] = EvalResult(x >= y);
587 : 510499 : break;
588 : : }
589 : 6060 : case Kind::LEQ:
590 : : {
591 : 6060 : const Rational& x = results[currNode[0]].d_rat;
592 : 6060 : const Rational& y = results[currNode[1]].d_rat;
593 : 6060 : results[currNode] = EvalResult(x <= y);
594 : 6060 : break;
595 : : }
596 : 12344 : case Kind::GT:
597 : : {
598 : 12344 : const Rational& x = results[currNode[0]].d_rat;
599 : 12344 : const Rational& y = results[currNode[1]].d_rat;
600 : 12344 : results[currNode] = EvalResult(x > y);
601 : 12344 : break;
602 : : }
603 : 91070 : case Kind::LT:
604 : : {
605 : 91070 : const Rational& x = results[currNode[0]].d_rat;
606 : 91070 : const Rational& y = results[currNode[1]].d_rat;
607 : 91070 : results[currNode] = EvalResult(x < y);
608 : 91070 : break;
609 : : }
610 : 1146 : case Kind::ABS:
611 : : {
612 : 1146 : const Rational& x = results[currNode[0]].d_rat;
613 : 1146 : results[currNode] = EvalResult(x.abs());
614 : 1146 : break;
615 : : }
616 : 22268 : case Kind::TO_REAL:
617 : : {
618 : : // casting to real is a no-op
619 : 22268 : const Rational& x = results[currNode[0]].d_rat;
620 : 22268 : results[currNode] = EvalResult(x);
621 : 22268 : break;
622 : : }
623 : 512 : case Kind::TO_INTEGER:
624 : : {
625 : : // casting to int takes the floor
626 : 512 : const Rational& x = results[currNode[0]].d_rat.floor();
627 : 512 : results[currNode] = EvalResult(x);
628 : 512 : break;
629 : 512 : }
630 : 4 : case Kind::IS_INTEGER:
631 : : {
632 : 4 : const Rational& x = results[currNode[0]].d_rat;
633 : 4 : results[currNode] = EvalResult(x.isIntegral());
634 : 4 : break;
635 : : }
636 : 12691 : case Kind::POW2:
637 : : {
638 : 12691 : const Rational& x = results[currNode[0]].d_rat;
639 : 12691 : bool valid = false;
640 [ + + ]: 12691 : if (x.sgn() < 0)
641 : : {
642 : 23 : results[currNode] = EvalResult(Rational(0));
643 : 23 : valid = true;
644 : : }
645 [ + + ]: 12668 : else if (x.getNumerator().fitsUnsignedInt())
646 : : {
647 : 12652 : uint32_t value = x.getNumerator().toUnsignedInt();
648 [ + - ]: 12652 : if (value <= 256)
649 : : {
650 : 12652 : valid = true;
651 : 12652 : results[currNode] = EvalResult(Rational(Integer(2).pow(value)));
652 : : }
653 : : }
654 [ + + ]: 12691 : if (!valid)
655 : : {
656 : 16 : processUnhandled(
657 : : currNode, currNodeVal, evalAsNode, results, needsReconstruct);
658 : : }
659 : 12691 : break;
660 : : }
661 : 196 : case Kind::INTS_ISPOW2:
662 : : {
663 : 196 : const Rational& x = results[currNode[0]].d_rat;
664 : 196 : results[currNode] = EvalResult(x.getNumerator().isPow2());
665 : 196 : break;
666 : : }
667 : 647 : case Kind::INTS_LOG2:
668 : : {
669 : 647 : const Rational& x = results[currNode[0]].d_rat;
670 [ - + ]: 647 : if (x.sgn() < 0)
671 : : {
672 : 0 : results[currNode] = EvalResult(Rational(0));
673 : : }
674 : : else
675 : : {
676 : 647 : results[currNode] =
677 : 1294 : EvalResult(Rational(x.getNumerator().length() - 1));
678 : : }
679 : 647 : break;
680 : : }
681 : 204172 : case Kind::CONST_STRING:
682 : 204172 : results[currNode] = EvalResult(currNodeVal.getConst<String>());
683 : 204172 : break;
684 : :
685 : 5657 : case Kind::STRING_CONCAT:
686 : : {
687 : 5657 : String res = results[currNode[0]].d_str;
688 [ + + ]: 18770 : for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
689 : : {
690 : 13113 : res = res.concat(results[currNode[i]].d_str);
691 : : }
692 : 5657 : results[currNode] = EvalResult(res);
693 : 5657 : break;
694 : 5657 : }
695 : :
696 : 13623 : case Kind::STRING_LENGTH:
697 : : {
698 : 13623 : const String& s = results[currNode[0]].d_str;
699 : 13623 : results[currNode] = EvalResult(Rational(s.size()));
700 : 13623 : break;
701 : : }
702 : :
703 : 7324 : case Kind::STRING_SUBSTR:
704 : : {
705 : 7324 : const String& s = results[currNode[0]].d_str;
706 : 7324 : Integer s_len(s.size());
707 : 7324 : Integer i = results[currNode[1]].d_rat.getNumerator();
708 : 7324 : Integer j = results[currNode[2]].d_rat.getNumerator();
709 : :
710 [ + + ][ + + ]: 7324 : if (i.strictlyNegative() || j.strictlyNegative() || i >= s_len)
[ + + ][ + + ]
711 : : {
712 : 1041 : results[currNode] = EvalResult(String(""));
713 : : }
714 [ + + ]: 6283 : else if (i + j > s_len)
715 : : {
716 : 484 : results[currNode] =
717 : 968 : EvalResult(s.suffix((s_len - i).toUnsignedInt()));
718 : : }
719 : : else
720 : : {
721 : 5799 : results[currNode] =
722 : 11598 : EvalResult(s.substr(i.toUnsignedInt(), j.toUnsignedInt()));
723 : : }
724 : 7324 : break;
725 : 7324 : }
726 : 0 : case Kind::SEQ_NTH:
727 : : {
728 : : // only strings evaluate
729 : 0 : Assert(currNode[0].getType().isString());
730 : 0 : const String& s = results[currNode[0]].d_str;
731 : 0 : Integer s_len(s.size());
732 : 0 : Integer i = results[currNode[1]].d_rat.getNumerator();
733 : 0 : if (i.strictlyNegative() || i >= s_len)
734 : : {
735 : 0 : results[currNode] = EvalResult(Rational(-1));
736 : : }
737 : : else
738 : : {
739 : 0 : results[currNode] =
740 : 0 : EvalResult(Rational(s.getVec()[i.toUnsignedInt()]));
741 : : }
742 : 0 : break;
743 : 0 : }
744 : :
745 : 32 : case Kind::STRING_UPDATE:
746 : : {
747 : 32 : const String& s = results[currNode[0]].d_str;
748 : 32 : Integer s_len(s.size());
749 : 32 : Integer i = results[currNode[1]].d_rat.getNumerator();
750 : 32 : const String& t = results[currNode[2]].d_str;
751 : :
752 [ + + ][ + + ]: 32 : if (i.strictlyNegative() || i >= s_len)
[ + + ]
753 : : {
754 : 12 : results[currNode] = EvalResult(s);
755 : : }
756 : : else
757 : : {
758 : 20 : results[currNode] = EvalResult(s.update(i.toUnsignedInt(), t));
759 : : }
760 : 32 : break;
761 : 32 : }
762 : 22 : case Kind::STRING_CHARAT:
763 : : {
764 : 22 : const String& s = results[currNode[0]].d_str;
765 : 22 : Integer s_len(s.size());
766 : 22 : Integer i = results[currNode[1]].d_rat.getNumerator();
767 [ + - ][ + - ]: 22 : if (i.strictlyNegative() || i >= s_len)
[ + - ]
768 : : {
769 : 22 : results[currNode] = EvalResult(String(""));
770 : : }
771 : : else
772 : : {
773 : 0 : results[currNode] = EvalResult(s.substr(i.toUnsignedInt(), 1));
774 : : }
775 : 22 : break;
776 : 22 : }
777 : :
778 : 2591 : case Kind::STRING_CONTAINS:
779 : : {
780 : 2591 : const String& s = results[currNode[0]].d_str;
781 : 2591 : const String& t = results[currNode[1]].d_str;
782 : 2591 : results[currNode] = EvalResult(s.find(t) != std::string::npos);
783 : 2591 : break;
784 : : }
785 : :
786 : 429 : case Kind::STRING_INDEXOF:
787 : : {
788 : 429 : const String& s = results[currNode[0]].d_str;
789 : 429 : Integer s_len(s.size());
790 : 429 : const String& x = results[currNode[1]].d_str;
791 : 429 : Integer i = results[currNode[2]].d_rat.getNumerator();
792 : :
793 [ + + ]: 429 : if (i.strictlyNegative())
794 : : {
795 : 4 : results[currNode] = EvalResult(Rational(-1));
796 : : }
797 : : else
798 : : {
799 : 425 : size_t r = s.find(x, i.toUnsignedInt());
800 [ + + ]: 425 : if (r == std::string::npos)
801 : : {
802 : 203 : results[currNode] = EvalResult(Rational(-1));
803 : : }
804 : : else
805 : : {
806 : 222 : results[currNode] = EvalResult(Rational(r));
807 : : }
808 : : }
809 : 429 : break;
810 : 429 : }
811 : :
812 : 364 : case Kind::STRING_REPLACE:
813 : : {
814 : 364 : const String& s = results[currNode[0]].d_str;
815 : 364 : const String& x = results[currNode[1]].d_str;
816 : 364 : const String& y = results[currNode[2]].d_str;
817 : 364 : results[currNode] = EvalResult(s.replace(x, y));
818 : 364 : break;
819 : : }
820 : 68 : case Kind::STRING_REPLACE_ALL:
821 : : {
822 : 68 : const String& s = results[currNode[0]].d_str;
823 : 68 : const String& x = results[currNode[1]].d_str;
824 : 68 : const String& y = results[currNode[2]].d_str;
825 [ + + ][ + + ]: 68 : if (s.empty() || x.empty())
[ + + ]
826 : : {
827 : 52 : results[currNode] = EvalResult(s);
828 : : }
829 : : else
830 : : {
831 : 16 : const std::vector<unsigned>& svec = s.getVec();
832 : 16 : const std::vector<unsigned>& yvec = y.getVec();
833 : 16 : std::size_t sizeS = s.size();
834 : 16 : std::size_t sizeX = x.size();
835 : 16 : std::size_t index = 0;
836 : 16 : std::size_t curr = 0;
837 : 16 : std::vector<unsigned> chars;
838 : : do
839 : : {
840 : 28 : curr = s.find(x, index);
841 [ + + ]: 28 : if (curr != std::string::npos)
842 : : {
843 [ - + ]: 12 : if (curr > index)
844 : : {
845 : 0 : chars.insert(
846 : 0 : chars.end(), svec.begin() + index, svec.begin() + curr);
847 : : }
848 : 12 : chars.insert(chars.end(), yvec.begin(), yvec.end());
849 : 12 : index = curr + sizeX;
850 : : }
851 : : else
852 : : {
853 : 48 : chars.insert(
854 : 64 : chars.end(), svec.begin() + index, svec.begin() + sizeS);
855 : : }
856 [ + + ][ + - ]: 28 : } while (curr != std::string::npos && curr < sizeS);
857 : : // constant evaluation
858 : 16 : results[currNode] = EvalResult(String(chars));
859 : 16 : }
860 : 68 : break;
861 : : }
862 : :
863 : 65 : case Kind::STRING_PREFIX:
864 : : {
865 : 65 : const String& t = results[currNode[0]].d_str;
866 : 65 : const String& s = results[currNode[1]].d_str;
867 [ + + ]: 65 : if (s.size() < t.size())
868 : : {
869 : 34 : results[currNode] = EvalResult(false);
870 : : }
871 : : else
872 : : {
873 : 31 : results[currNode] = EvalResult(s.prefix(t.size()) == t);
874 : : }
875 : 65 : break;
876 : : }
877 : :
878 : 46 : case Kind::STRING_SUFFIX:
879 : : {
880 : 46 : const String& t = results[currNode[0]].d_str;
881 : 46 : const String& s = results[currNode[1]].d_str;
882 [ + + ]: 46 : if (s.size() < t.size())
883 : : {
884 : 30 : results[currNode] = EvalResult(false);
885 : : }
886 : : else
887 : : {
888 : 16 : results[currNode] = EvalResult(s.suffix(t.size()) == t);
889 : : }
890 : 46 : break;
891 : : }
892 : :
893 : 122 : case Kind::STRING_ITOS:
894 : : {
895 : 122 : Integer i = results[currNode[0]].d_rat.getNumerator();
896 [ - + ]: 122 : if (i.strictlyNegative())
897 : : {
898 : 0 : results[currNode] = EvalResult(String(""));
899 : : }
900 : : else
901 : : {
902 : 122 : results[currNode] = EvalResult(String(i.toString()));
903 : : }
904 : 122 : break;
905 : 122 : }
906 : :
907 : 109 : case Kind::STRING_STOI:
908 : : {
909 : 109 : const String& s = results[currNode[0]].d_str;
910 [ + + ]: 109 : if (s.isNumber())
911 : : {
912 : 56 : results[currNode] = EvalResult(Rational(s.toNumber()));
913 : : }
914 : : else
915 : : {
916 : 53 : results[currNode] = EvalResult(Rational(-1));
917 : : }
918 : 109 : break;
919 : : }
920 : :
921 : 22 : case Kind::STRING_FROM_CODE:
922 : : {
923 : 22 : Integer i = results[currNode[0]].d_rat.getNumerator();
924 : 22 : if (i >= 0 && i < d_alphaCard)
925 : : {
926 : 14 : std::vector<unsigned> svec = {i.toUnsignedInt()};
927 : 14 : results[currNode] = EvalResult(String(svec));
928 : 14 : }
929 : : else
930 : : {
931 : 8 : results[currNode] = EvalResult(String(""));
932 : : }
933 : 22 : break;
934 : 22 : }
935 : :
936 : 211 : case Kind::STRING_TO_CODE:
937 : : {
938 : 211 : const String& s = results[currNode[0]].d_str;
939 [ + + ]: 211 : if (s.size() == 1)
940 : : {
941 : 193 : results[currNode] = EvalResult(Rational(s.getVec()[0]));
942 : : }
943 : : else
944 : : {
945 : 18 : results[currNode] = EvalResult(Rational(-1));
946 : : }
947 : 211 : break;
948 : : }
949 : 26 : case Kind::STRING_REV:
950 : : {
951 : 26 : const String& s = results[currNode[0]].d_str;
952 : 26 : std::vector<unsigned> nvec = s.getVec();
953 : 26 : std::reverse(nvec.begin(), nvec.end());
954 : 26 : results[currNode] = EvalResult(String(nvec));
955 : 26 : break;
956 : 26 : }
957 : 16 : case Kind::STRING_TO_LOWER:
958 : : case Kind::STRING_TO_UPPER:
959 : : {
960 : 16 : const String& s = results[currNode[0]].d_str;
961 : 16 : std::vector<unsigned> nvec = s.getVec();
962 : 16 : Kind k = currNodeVal.getKind();
963 [ + + ]: 36 : for (unsigned i = 0, nvsize = nvec.size(); i < nvsize; i++)
964 : : {
965 : 20 : unsigned newChar = nvec[i];
966 : : // transform it
967 : : // upper 65 ... 90
968 : : // lower 97 ... 122
969 [ + + ]: 20 : if (k == Kind::STRING_TO_UPPER)
970 : : {
971 [ + + ][ + - ]: 8 : if (newChar >= 97 && newChar <= 122)
972 : : {
973 : 4 : newChar = newChar - 32;
974 : : }
975 : : }
976 [ + - ]: 12 : else if (k == Kind::STRING_TO_LOWER)
977 : : {
978 [ + - ][ + + ]: 12 : if (newChar >= 65 && newChar <= 90)
979 : : {
980 : 4 : newChar = newChar + 32;
981 : : }
982 : : }
983 : 20 : nvec[i] = newChar;
984 : : }
985 : 16 : results[currNode] = EvalResult(String(nvec));
986 : 16 : break;
987 : 16 : }
988 : 81 : case Kind::STRING_LEQ:
989 : : {
990 : 81 : const String& s1 = results[currNode[0]].d_str;
991 : 81 : const String& s2 = results[currNode[1]].d_str;
992 : 81 : results[currNode] = EvalResult(s1.isLeq(s2));
993 : 81 : break;
994 : : }
995 : 705536 : case Kind::CONST_BITVECTOR:
996 : 705536 : results[currNode] = EvalResult(currNodeVal.getConst<BitVector>());
997 : 705536 : break;
998 : :
999 : 65018 : case Kind::BITVECTOR_NOT:
1000 : 65018 : results[currNode] = EvalResult(~results[currNode[0]].d_bv);
1001 : 65018 : break;
1002 : :
1003 : 11384 : case Kind::BITVECTOR_NEG:
1004 : 11384 : results[currNode] = EvalResult(-results[currNode[0]].d_bv);
1005 : 11384 : break;
1006 : :
1007 : 55290 : case Kind::BITVECTOR_EXTRACT:
1008 : : {
1009 : 55290 : unsigned lo = bv::utils::getExtractLow(currNodeVal);
1010 : 55290 : unsigned hi = bv::utils::getExtractHigh(currNodeVal);
1011 : 55290 : results[currNode] =
1012 : 110580 : EvalResult(results[currNode[0]].d_bv.extract(hi, lo));
1013 : 55290 : break;
1014 : : }
1015 : :
1016 : 35611 : case Kind::BITVECTOR_CONCAT:
1017 : : {
1018 : 35611 : BitVector res = results[currNode[0]].d_bv;
1019 [ + + ]: 79556 : for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
1020 : : {
1021 : 43945 : res = res.concat(results[currNode[i]].d_bv);
1022 : : }
1023 : 35611 : results[currNode] = EvalResult(res);
1024 : 35611 : break;
1025 : 35611 : }
1026 : :
1027 : 30661 : case Kind::BITVECTOR_ADD:
1028 : : {
1029 : 30661 : BitVector res = results[currNode[0]].d_bv;
1030 [ + + ]: 61338 : for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
1031 : : {
1032 : 30677 : res = res + results[currNode[i]].d_bv;
1033 : : }
1034 : 30661 : results[currNode] = EvalResult(res);
1035 : 30661 : break;
1036 : 30661 : }
1037 : :
1038 : 62678 : case Kind::BITVECTOR_MULT:
1039 : : {
1040 : 62678 : BitVector res = results[currNode[0]].d_bv;
1041 [ + + ]: 136102 : for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
1042 : : {
1043 : 73424 : res = res * results[currNode[i]].d_bv;
1044 : : }
1045 : 62678 : results[currNode] = EvalResult(res);
1046 : 62678 : break;
1047 : 62678 : }
1048 : 51133 : case Kind::BITVECTOR_AND:
1049 : : {
1050 : 51133 : BitVector res = results[currNode[0]].d_bv;
1051 [ + + ]: 102644 : for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
1052 : : {
1053 : 51511 : res = res & results[currNode[i]].d_bv;
1054 : : }
1055 : 51133 : results[currNode] = EvalResult(res);
1056 : 51133 : break;
1057 : 51133 : }
1058 : :
1059 : 90964 : case Kind::BITVECTOR_OR:
1060 : : {
1061 : 90964 : BitVector res = results[currNode[0]].d_bv;
1062 [ + + ]: 206502 : for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
1063 : : {
1064 : 115538 : res = res | results[currNode[i]].d_bv;
1065 : : }
1066 : 90964 : results[currNode] = EvalResult(res);
1067 : 90964 : break;
1068 : 90964 : }
1069 : :
1070 : 691 : case Kind::BITVECTOR_XOR:
1071 : : {
1072 : 691 : BitVector res = results[currNode[0]].d_bv;
1073 [ + + ]: 1386 : for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
1074 : : {
1075 : 695 : res = res ^ results[currNode[i]].d_bv;
1076 : : }
1077 : 691 : results[currNode] = EvalResult(res);
1078 : 691 : break;
1079 : 691 : }
1080 : 48534 : case Kind::BITVECTOR_UDIV:
1081 : : {
1082 : 48534 : BitVector res = results[currNode[0]].d_bv;
1083 : 48534 : res = res.unsignedDivTotal(results[currNode[1]].d_bv);
1084 : 48534 : results[currNode] = EvalResult(res);
1085 : 48534 : break;
1086 : 48534 : }
1087 : 52798 : case Kind::BITVECTOR_UREM:
1088 : : {
1089 : 52798 : BitVector res = results[currNode[0]].d_bv;
1090 : 52798 : res = res.unsignedRemTotal(results[currNode[1]].d_bv);
1091 : 52798 : results[currNode] = EvalResult(res);
1092 : 52798 : break;
1093 : 52798 : }
1094 : 414 : case Kind::BITVECTOR_SHL:
1095 : : {
1096 : 414 : BitVector res = results[currNode[0]].d_bv;
1097 : 414 : res = res.leftShift(results[currNode[1]].d_bv);
1098 : 414 : results[currNode] = EvalResult(res);
1099 : 414 : break;
1100 : 414 : }
1101 : 411 : case Kind::BITVECTOR_ASHR:
1102 : : {
1103 : 411 : BitVector res = results[currNode[0]].d_bv;
1104 : 411 : res = res.arithRightShift(results[currNode[1]].d_bv);
1105 : 411 : results[currNode] = EvalResult(res);
1106 : 411 : break;
1107 : 411 : }
1108 : 14815 : case Kind::BITVECTOR_ULT:
1109 : : {
1110 : 14815 : BitVector res = results[currNode[0]].d_bv;
1111 : 14815 : bool b = res.unsignedLessThan(results[currNode[1]].d_bv);
1112 : 14815 : results[currNode] = EvalResult(b);
1113 : 14815 : break;
1114 : 14815 : }
1115 : 340 : case Kind::BITVECTOR_SLT:
1116 : : {
1117 : 340 : BitVector res = results[currNode[0]].d_bv;
1118 : 340 : bool b = res.signedLessThan(results[currNode[1]].d_bv);
1119 : 340 : results[currNode] = EvalResult(b);
1120 : 340 : break;
1121 : 340 : }
1122 : 73 : case Kind::BITVECTOR_SLE:
1123 : : {
1124 : 73 : BitVector res = results[currNode[0]].d_bv;
1125 : 73 : bool b = res.signedLessThanEq(results[currNode[1]].d_bv);
1126 : 73 : results[currNode] = EvalResult(b);
1127 : 73 : break;
1128 : 73 : }
1129 : 193 : case Kind::BITVECTOR_ULE:
1130 : : {
1131 : 193 : BitVector res = results[currNode[0]].d_bv;
1132 : 193 : bool b = res.unsignedLessThanEq(results[currNode[1]].d_bv);
1133 : 193 : results[currNode] = EvalResult(b);
1134 : 193 : break;
1135 : 193 : }
1136 : 505 : case Kind::BITVECTOR_UGT:
1137 : : {
1138 : 505 : BitVector res = results[currNode[1]].d_bv;
1139 : 505 : bool b = res.unsignedLessThan(results[currNode[0]].d_bv);
1140 : 505 : results[currNode] = EvalResult(b);
1141 : 505 : break;
1142 : 505 : }
1143 : 321 : case Kind::BITVECTOR_SGT:
1144 : : {
1145 : 321 : BitVector res = results[currNode[1]].d_bv;
1146 : 321 : bool b = res.signedLessThan(results[currNode[0]].d_bv);
1147 : 321 : results[currNode] = EvalResult(b);
1148 : 321 : break;
1149 : 321 : }
1150 : 583 : case Kind::BITVECTOR_SGE:
1151 : : {
1152 : 583 : BitVector res = results[currNode[1]].d_bv;
1153 : 583 : bool b = res.signedLessThanEq(results[currNode[0]].d_bv);
1154 : 583 : results[currNode] = EvalResult(b);
1155 : 583 : break;
1156 : 583 : }
1157 : 294 : case Kind::BITVECTOR_UGE:
1158 : : {
1159 : 294 : BitVector res = results[currNode[1]].d_bv;
1160 : 294 : bool b = res.unsignedLessThanEq(results[currNode[0]].d_bv);
1161 : 294 : results[currNode] = EvalResult(b);
1162 : 294 : break;
1163 : 294 : }
1164 : 3457 : case Kind::BITVECTOR_REPEAT:
1165 : : {
1166 : 3457 : BitVector res = results[currNode[0]].d_bv;
1167 : : unsigned amount =
1168 : 3457 : currNode.getOperator().getConst<BitVectorRepeat>().d_repeatAmount;
1169 : 3457 : BitVector ret = res;
1170 [ + + ]: 3672 : for (size_t i = 1; i < amount; i++)
1171 : : {
1172 : 215 : ret = ret.concat(res);
1173 : : }
1174 : 3457 : results[currNode] = EvalResult(ret);
1175 : 3457 : break;
1176 : 3457 : }
1177 : 5423 : case Kind::BITVECTOR_SIGN_EXTEND:
1178 : : {
1179 : 5423 : BitVector res = results[currNode[0]].d_bv;
1180 : 5423 : unsigned amount = currNode.getOperator()
1181 : 5423 : .getConst<BitVectorSignExtend>()
1182 : 5423 : .d_signExtendAmount;
1183 : 5423 : results[currNode] = EvalResult(res.signExtend(amount));
1184 : 5423 : break;
1185 : 5423 : }
1186 : 5665 : case Kind::BITVECTOR_ZERO_EXTEND:
1187 : : {
1188 : 5665 : BitVector res = results[currNode[0]].d_bv;
1189 : 5665 : unsigned amount = currNode.getOperator()
1190 : 5665 : .getConst<BitVectorZeroExtend>()
1191 : 5665 : .d_zeroExtendAmount;
1192 : 5665 : results[currNode] = EvalResult(res.zeroExtend(amount));
1193 : 5665 : break;
1194 : 5665 : }
1195 : :
1196 : 1777080 : case Kind::EQUAL:
1197 : : {
1198 : 1777080 : EvalResult lhs = results[currNode[0]];
1199 : 1777080 : EvalResult rhs = results[currNode[1]];
1200 : :
1201 [ + + ][ + + ]: 1777080 : switch (lhs.d_tag)
[ + - ]
1202 : : {
1203 : 603883 : case EvalResult::BOOL:
1204 : : {
1205 : 603883 : results[currNode] = EvalResult(lhs.d_bool == rhs.d_bool);
1206 : 603883 : break;
1207 : : }
1208 : :
1209 : 44774 : case EvalResult::BITVECTOR:
1210 : : {
1211 : 44774 : results[currNode] = EvalResult(lhs.d_bv == rhs.d_bv);
1212 : 44774 : break;
1213 : : }
1214 : :
1215 : 1122087 : case EvalResult::RATIONAL:
1216 : : {
1217 : 1122087 : results[currNode] = EvalResult(lhs.d_rat == rhs.d_rat);
1218 : 1122087 : break;
1219 : : }
1220 : :
1221 : 6312 : case EvalResult::STRING:
1222 : : {
1223 : 6312 : results[currNode] = EvalResult(lhs.d_str == rhs.d_str);
1224 : 6312 : break;
1225 : : }
1226 : 24 : case EvalResult::UVALUE:
1227 : : {
1228 : 24 : results[currNode] = EvalResult(lhs.d_av == rhs.d_av);
1229 : 24 : break;
1230 : : }
1231 : :
1232 : 0 : default:
1233 : : {
1234 : 0 : Trace("evaluator") << "Evaluation of " << currNode[0].getKind()
1235 : 0 : << " not supported" << std::endl;
1236 : 0 : results[currNode] = EvalResult();
1237 : 0 : evalAsNode[currNode] =
1238 : 0 : needsReconstruct ? reconstruct(currNode, results, evalAsNode)
1239 : 0 : : currNodeVal;
1240 : 0 : break;
1241 : : }
1242 : : }
1243 : :
1244 : 1777080 : break;
1245 : 1777080 : }
1246 : :
1247 : 2579255 : case Kind::ITE:
1248 : : {
1249 [ + + ]: 2579255 : if (results[currNode[0]].d_bool)
1250 : : {
1251 : 994502 : results[currNode] = results[currNode[1]];
1252 : : }
1253 : : else
1254 : : {
1255 : 1584753 : results[currNode] = results[currNode[2]];
1256 : : }
1257 : 2579255 : break;
1258 : : }
1259 : 10294 : case Kind::BITVECTOR_UBV_TO_INT:
1260 : : {
1261 : 10294 : BitVector res = results[currNode[0]].d_bv;
1262 : 10294 : results[currNode] = EvalResult(Rational(res.toInteger()));
1263 : 10294 : break;
1264 : 10294 : }
1265 : 21 : case Kind::BITVECTOR_SBV_TO_INT:
1266 : : {
1267 : 21 : BitVector res = results[currNode[0]].d_bv;
1268 : 21 : const uint32_t size = currNode[0].getType().getBitVectorSize();
1269 : : // should not evaluate on empty bitvectors
1270 [ - + ][ - + ]: 21 : Assert(size != 0);
[ - - ]
1271 [ + + ]: 21 : if (res.isBitSet(size - 1))
1272 : : {
1273 : 14 : Rational ttm = Rational(Integer(2).pow(size));
1274 : 7 : results[currNode] = EvalResult(Rational(res.toInteger()) - ttm);
1275 : 7 : }
1276 : : else
1277 : : {
1278 : 14 : results[currNode] = EvalResult(Rational(res.toInteger()));
1279 : : }
1280 : 21 : break;
1281 : 21 : }
1282 : 7438 : case Kind::INT_TO_BITVECTOR:
1283 : : {
1284 : 7438 : Integer i = results[currNode[0]].d_rat.getNumerator();
1285 : : const uint32_t size =
1286 : 7438 : currNodeVal.getOperator().getConst<IntToBitVector>().d_size;
1287 : 7438 : results[currNode] = EvalResult(BitVector(size, i));
1288 : 7438 : break;
1289 : 7438 : }
1290 : 70577 : case Kind::CONST_BITVECTOR_SYMBOLIC:
1291 : : {
1292 : 70577 : Integer i = results[currNode[0]].d_rat.getNumerator();
1293 : 70577 : Integer w = results[currNode[1]].d_rat.getNumerator();
1294 [ + - ]: 70577 : if (w.fitsUnsignedInt())
1295 : : {
1296 [ - + ][ - + ]: 70577 : Assert(w.sgn() >= 0);
[ - - ]
1297 [ + - ]: 141154 : Trace("evaluator") << currNode << " evalutes to "
1298 [ - + ][ - - ]: 70577 : << BitVector(w.toUnsignedInt(), i) << std::endl;
1299 : 70577 : results[currNode] = EvalResult(BitVector(w.toUnsignedInt(), i));
1300 : : }
1301 : : else
1302 : : {
1303 : 0 : processUnhandled(
1304 : : currNode, currNodeVal, evalAsNode, results, needsReconstruct);
1305 : : }
1306 : 70577 : break;
1307 : 70577 : }
1308 : 25932 : case Kind::BITVECTOR_SIZE:
1309 : : {
1310 : 25932 : const TypeNode& tn = currNode[0].getType();
1311 [ + - ]: 25932 : if (tn.isBitVector())
1312 : : {
1313 : 25932 : results[currNode] = EvalResult(Rational(tn.getBitVectorSize()));
1314 : : }
1315 : : else
1316 : : {
1317 : 0 : processUnhandled(
1318 : : currNode, currNodeVal, evalAsNode, results, needsReconstruct);
1319 : : }
1320 : 25932 : break;
1321 : 25932 : }
1322 : 100135 : default:
1323 : : {
1324 [ + - ]: 200270 : Trace("evaluator") << "Kind " << currNodeVal.getKind()
1325 : 100135 : << " not supported" << std::endl;
1326 : 100135 : processUnhandled(
1327 : : currNode, currNodeVal, evalAsNode, results, needsReconstruct);
1328 : : }
1329 : : }
1330 [ + + ]: 44162106 : }
1331 [ + + ]: 70625153 : }
1332 : :
1333 : 8317772 : return results[n];
1334 : 4158886 : }
1335 : :
1336 : 19109896 : Node Evaluator::reconstruct(TNode n,
1337 : : std::unordered_map<TNode, EvalResult>& eresults,
1338 : : std::unordered_map<TNode, Node>& evalAsNode) const
1339 : : {
1340 [ + + ]: 19109896 : if (n.getNumChildren() == 0)
1341 : : {
1342 : 43022 : return n;
1343 : : }
1344 [ + - ]: 19066874 : Trace("evaluator") << "Evaluator: reconstruct " << n << std::endl;
1345 : 19066874 : NodeManager* nm = n.getNodeManager();
1346 : 19066874 : std::unordered_map<TNode, EvalResult>::iterator itr;
1347 : 19066874 : std::unordered_map<TNode, Node>::iterator itn;
1348 : 19066874 : std::vector<Node> echildren;
1349 [ + + ]: 19066874 : if (n.getMetaKind() == kind::metakind::PARAMETERIZED)
1350 : : {
1351 : 2020356 : TNode op = n.getOperator();
1352 [ + + ]: 2020356 : if (op.isConst())
1353 : : {
1354 : 1340976 : echildren.push_back(op);
1355 : : }
1356 : : else
1357 : : {
1358 : 679380 : itr = eresults.find(op);
1359 [ - + ][ - + ]: 679380 : Assert(itr != eresults.end());
[ - - ]
1360 [ + - ]: 679380 : if (itr->second.d_tag == EvalResult::INVALID)
1361 : : {
1362 : : // could not evaluate the operator, look in the node cache
1363 : 679380 : itn = evalAsNode.find(op);
1364 [ - + ][ - + ]: 679380 : Assert(itn != evalAsNode.end());
[ - - ]
1365 : 679380 : echildren.push_back(itn->second);
1366 : : }
1367 : : else
1368 : : {
1369 : : // otherwise, use the evaluation of the operator
1370 : 0 : echildren.push_back(itr->second.toNode(op.getType()));
1371 : : }
1372 : : }
1373 : 2020356 : }
1374 [ + + ]: 57772513 : for (const auto& currNodeChild : n)
1375 : : {
1376 : 38705639 : itr = eresults.find(currNodeChild);
1377 [ - + ][ - + ]: 38705639 : Assert(itr != eresults.end());
[ - - ]
1378 [ + + ]: 38705639 : if (itr->second.d_tag == EvalResult::INVALID)
1379 : : {
1380 : : // could not evaluate this child, look in the node cache
1381 : 32891208 : itn = evalAsNode.find(currNodeChild);
1382 [ - + ][ - + ]: 32891208 : Assert(itn != evalAsNode.end());
[ - - ]
1383 [ - + ][ - + ]: 32891208 : Assert(!itn->second.isNull());
[ - - ]
1384 : 32891208 : echildren.push_back(itn->second);
1385 : : }
1386 : : else
1387 : : {
1388 : : // otherwise, use the evaluation
1389 : 5814431 : echildren.push_back(itr->second.toNode(currNodeChild.getType()));
1390 : : }
1391 : 38705639 : }
1392 : : // The value is the result of our (partially) successful evaluation
1393 : : // of the children.
1394 : 19066874 : Node nn = nm->mkNode(n.getKind(), echildren);
1395 [ + - ]: 19066874 : Trace("evaluator") << "Evaluator: reconstructed " << nn << std::endl;
1396 : : // Return node, without rewriting. Notice we do not need to substitute here
1397 : : // since all substitutions should already have been applied recursively.
1398 : 19066874 : return nn;
1399 : 19066874 : }
1400 : :
1401 : 100938 : void Evaluator::processUnhandled(TNode n,
1402 : : TNode nv,
1403 : : std::unordered_map<TNode, Node>& evalAsNode,
1404 : : std::unordered_map<TNode, EvalResult>& results,
1405 : : bool needsReconstruct) const
1406 : : {
1407 : 100938 : results[n] = EvalResult();
1408 : 100938 : evalAsNode[n] =
1409 [ + + ][ + + ]: 201876 : needsReconstruct ? reconstruct(n, results, evalAsNode) : Node(nv);
[ - - ]
1410 : 100938 : }
1411 : :
1412 : : } // namespace theory
1413 : : } // namespace cvc5::internal
|
