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 : 9833258 : EvalResult::EvalResult(const EvalResult& other)
31 : : {
32 : 9833258 : d_tag = other.d_tag;
33 [ + + ][ + + ]: 9833258 : switch (d_tag)
[ + + ][ - ]
34 : : {
35 : 2935616 : case BOOL: d_bool = other.d_bool; break;
36 : 240861 : case BITVECTOR:
37 : 240861 : new (&d_bv) BitVector;
38 : 240861 : d_bv = other.d_bv;
39 : 240861 : break;
40 : 4050404 : case RATIONAL:
41 : 4050404 : new (&d_rat) Rational;
42 : 4050404 : d_rat = other.d_rat;
43 : 4050404 : break;
44 : 26517 : case STRING:
45 : 26517 : new (&d_str) String;
46 : 26517 : d_str = other.d_str;
47 : 26517 : break;
48 : 59 : case UVALUE: new (&d_av) UninterpretedSortValue(other.d_av); break;
49 : 2579801 : case INVALID: break;
50 : : }
51 : 9833258 : }
52 : :
53 : 53937602 : EvalResult& EvalResult::operator=(const EvalResult& other)
54 : : {
55 [ + - ]: 53937602 : if (this != &other)
56 : : {
57 : 53937602 : d_tag = other.d_tag;
58 [ + + ][ + + ]: 53937602 : switch (d_tag)
[ + + ][ - ]
59 : : {
60 : 21042246 : case BOOL: d_bool = other.d_bool; break;
61 : 1276077 : case BITVECTOR:
62 : 1276077 : new (&d_bv) BitVector;
63 : 1276077 : d_bv = other.d_bv;
64 : 1276077 : break;
65 : 6039805 : case RATIONAL:
66 : 6039805 : new (&d_rat) Rational;
67 : 6039805 : d_rat = other.d_rat;
68 : 6039805 : break;
69 : 208043 : case STRING:
70 : 208043 : new (&d_str) String;
71 : 208043 : d_str = other.d_str;
72 : 208043 : break;
73 : 169 : case UVALUE: new (&d_av) UninterpretedSortValue(other.d_av); break;
74 : 25371262 : case INVALID: break;
75 : : }
76 : : }
77 : 53937602 : return *this;
78 : : }
79 : :
80 : 113818614 : EvalResult::~EvalResult()
81 : : {
82 [ + + ][ + + ]: 113818614 : switch (d_tag)
[ + ]
83 : : {
84 : 2766943 : case BITVECTOR:
85 : : {
86 : 2766943 : d_bv.~BitVector();
87 : 2766943 : break;
88 : : }
89 : 16116773 : case RATIONAL:
90 : : {
91 : 16116773 : d_rat.~Rational();
92 : 16116773 : break;
93 : : }
94 : 442425 : case STRING:
95 : : {
96 : 442425 : d_str.~String();
97 : 442425 : break;
98 : : }
99 : 397 : case UVALUE:
100 : : {
101 : 397 : d_av.~UninterpretedSortValue();
102 : 397 : break;
103 : : }
104 : 94492076 : default: break;
105 : : }
106 : 113818614 : }
107 : :
108 : 10491758 : Node EvalResult::toNode(const TypeNode& tn) const
109 : : {
110 : 10491758 : NodeManager* nm = tn.getNodeManager();
111 [ + + ][ + + ]: 10491758 : switch (d_tag)
[ + + ]
112 : : {
113 : 3744900 : case EvalResult::BOOL: return nm->mkConst(d_bool);
114 : 763444 : case EvalResult::BITVECTOR: return nm->mkConst(d_bv);
115 : 3186211 : case EvalResult::RATIONAL:
116 [ - + ][ - + ]: 3186211 : Assert(!tn.isNull());
[ - - ]
117 : 3186211 : return nm->mkConstRealOrInt(tn, d_rat);
118 : 217964 : case EvalResult::STRING: return nm->mkConst(d_str);
119 : 149 : case EvalResult::UVALUE: return nm->mkConst(d_av);
120 : 2579090 : default:
121 : : {
122 [ + - ]: 5158180 : Trace("evaluator") << "Missing conversion from " << d_tag << " to node"
123 : 2579090 : << std::endl;
124 : 2579090 : return Node();
125 : : }
126 : : }
127 : : }
128 : :
129 : 1661315 : Evaluator::Evaluator(Rewriter* rr, uint32_t alphaCard)
130 : 1661315 : : d_rr(rr), d_alphaCard(alphaCard)
131 : : {
132 : 1661315 : }
133 : :
134 : 2437738 : Node Evaluator::eval(TNode n,
135 : : const std::vector<Node>& args,
136 : : const std::vector<Node>& vals) const
137 : : {
138 : 2437738 : std::unordered_map<Node, Node> visited;
139 : 4875476 : return eval(n, args, vals, visited);
140 : 2437738 : }
141 : 4196358 : 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 [ + - ]: 8392716 : Trace("evaluator") << "Evaluating " << n << " under substitution " << args
147 : 4196358 : << " " << vals << " with visited size = " << visited.size()
148 : 4196358 : << std::endl;
149 : 4196358 : std::unordered_map<TNode, Node> evalAsNode;
150 : 4196358 : std::unordered_map<TNode, EvalResult> results;
151 : : // add visited to results
152 [ + + ]: 4218212 : for (const std::pair<const Node, Node>& p : visited)
153 : : {
154 [ + - ]: 21854 : Trace("evaluator") << "Add " << p.first << " == " << p.second << std::endl;
155 : 21854 : results[p.first] = evalInternal(p.second, args, vals, evalAsNode, results);
156 [ + + ]: 21854 : 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 [ + - ]: 4196358 : Trace("evaluator") << "Run eval internal..." << std::endl;
170 : : Node ret =
171 : 8392716 : evalInternal(n, args, vals, evalAsNode, results).toNode(n.getType());
172 : : // if we failed to evaluate
173 [ + + ]: 4196358 : if (d_rr != nullptr)
174 : : {
175 [ + + ]: 992568 : if (ret.isNull())
176 : : {
177 : : // should be stored in the evaluation-as-node map
178 : 32339 : std::unordered_map<TNode, Node>::iterator itn = evalAsNode.find(n);
179 [ - + ][ - + ]: 32339 : Assert(itn != evalAsNode.end());
[ - - ]
180 : 32339 : ret = itn->second;
181 : : }
182 : : // always rewrite, which can change if the evaluation was not a constant
183 : 992568 : 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 : 4196358 : 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 : 8392716 : return ret;
192 : 4196358 : }
193 : :
194 : 4298936 : 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 : 4298936 : std::vector<TNode> queue;
202 : 4298936 : queue.emplace_back(n);
203 : 4298936 : std::unordered_map<TNode, EvalResult>::iterator itr;
204 : :
205 [ + + ]: 90638188 : while (queue.size() != 0)
206 : : {
207 : 86339252 : TNode currNode = queue.back();
208 : :
209 [ + + ]: 86339252 : if (results.find(currNode) != results.end())
210 : : {
211 : 1940023 : queue.pop_back();
212 : 1940023 : continue;
213 : : }
214 : :
215 : 84399229 : bool doProcess = true;
216 : 84399229 : bool isVar = false;
217 : 84399229 : bool doEval = true;
218 [ + + ]: 84399229 : 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 : 10212597 : isVar = true;
223 : 10212597 : doEval = false;
224 : : }
225 [ + + ]: 74186632 : else if (currNode.getMetaKind() == kind::metakind::PARAMETERIZED)
226 : : {
227 : 3740223 : 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 [ + + ]: 3740223 : if (!op.isConst())
231 : : {
232 : 1325166 : itr = results.find(op);
233 [ + + ]: 1325166 : if (itr == results.end())
234 : : {
235 : 382123 : queue.emplace_back(op);
236 : 382123 : doProcess = false;
237 : : }
238 [ + - ]: 943043 : else if (itr->second.d_tag == EvalResult::INVALID)
239 : : {
240 : 943043 : doEval = false;
241 : : }
242 : : }
243 [ + + ]: 2415057 : else if (currNode.getKind() == Kind::APPLY_INDEXED_SYMBOLIC)
244 : : {
245 : : // we require special handling below to deal with symbolic indexed
246 : : // operators.
247 : 121718 : doEval = false;
248 : : }
249 : 3740223 : }
250 [ + + ]: 244530685 : for (const auto& currNodeChild : currNode)
251 : : {
252 : 160131456 : itr = results.find(currNodeChild);
253 [ + + ]: 160131456 : if (itr == results.end())
254 : : {
255 : 51173851 : queue.emplace_back(currNodeChild);
256 : 51173851 : doProcess = false;
257 : : }
258 [ + + ]: 108957605 : else if (itr->second.d_tag == EvalResult::INVALID)
259 : : {
260 : : // we cannot evaluate since there was an invalid child
261 : 40438380 : doEval = false;
262 : : }
263 : 160131456 : }
264 [ + - ]: 168798458 : Trace("evaluator") << "Evaluator: visit " << currNode
265 : 0 : << ", process = " << doProcess
266 : 84399229 : << ", evaluate = " << doEval << std::endl;
267 : :
268 [ + + ]: 84399229 : if (doProcess)
269 : : {
270 : 53914887 : queue.pop_back();
271 : :
272 : 53914887 : Node currNodeVal = currNode;
273 : : // whether we need to reconstruct the current node in the case of failure
274 : 53914887 : 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 [ + + ]: 53914887 : if (!doEval)
284 : : {
285 [ + + ]: 30981111 : if (isVar)
286 : : {
287 : 10212597 : const auto& it = std::find(args.begin(), args.end(), currNode);
288 [ + + ]: 10212597 : if (it == args.end())
289 : : {
290 : : // variable with no substitution is itself
291 : 4564399 : evalAsNode[currNode] = currNode;
292 : 4564399 : results[currNode] = EvalResult();
293 : 4564399 : continue;
294 : : }
295 : 5648198 : ptrdiff_t pos = std::distance(args.begin(), it);
296 : 5648198 : 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 [ + - ]: 20768514 : Trace("evaluator") << "Evaluator: collect arguments" << std::endl;
305 : 20768514 : currNodeVal = reconstruct(currNodeVal, results, evalAsNode);
306 [ + + ]: 20768514 : 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 : 463073 : currNodeVal = d_rr->rewrite(currNodeVal);
311 : : }
312 [ + + ]: 20305441 : 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 : 50472 : currNodeVal);
322 [ + + ]: 50472 : if (rr != currNodeVal)
323 : : {
324 : 9505 : 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 [ + + ]: 9505 : if (!rre.isNull())
328 : : {
329 : 8911 : currNodeVal = rre;
330 : : }
331 : 9505 : }
332 : 50472 : }
333 : : }
334 : 26416712 : needsReconstruct = false;
335 [ + - ]: 52833424 : Trace("evaluator") << "Evaluator: now after substitution + rewriting: "
336 : 26416712 : << currNodeVal << std::endl;
337 : 26416712 : if (currNodeVal.getNumChildren() > 0
338 [ + + ][ + + ]: 26416712 : && 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 : 20704109 : results[currNode] = EvalResult();
346 : 20704109 : evalAsNode[currNode] = currNodeVal;
347 : 20704109 : 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 [ + - ]: 28646379 : Trace("evaluator") << "Current node val : " << currNodeVal << std::endl;
355 : :
356 [ + + ][ + + ]: 28646379 : 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 : 80724 : case Kind::APPLY_UF:
361 : : {
362 [ + - ]: 80724 : Trace("evaluator") << "Evaluate " << currNode << std::endl;
363 : 80724 : TNode op = currNode.getOperator();
364 [ + - ]: 80724 : 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 : 80724 : 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 [ + - ]: 80724 : Trace("evaluator") << "Operator evaluated to " << op << std::endl;
377 [ - + ]: 80724 : 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 : 80724 : std::vector<Node> lambdaArgs(args);
387 : 80724 : 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 [ + + ]: 228062 : for (const auto& lambdaArg : op[0])
393 : : {
394 : 147338 : lambdaArgs.insert(lambdaArgs.begin(), lambdaArg);
395 : 228062 : }
396 : :
397 [ + + ]: 228062 : for (const auto& lambdaVal : currNode)
398 : : {
399 : 147338 : lambdaVals.insert(lambdaVals.begin(),
400 : 294676 : results[lambdaVal].toNode(lambdaVal.getType()));
401 : 147338 : }
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 : 80724 : std::unordered_map<TNode, Node> evalAsNodeC;
410 : 80724 : std::unordered_map<TNode, EvalResult> resultsC;
411 : 161448 : results[currNode] = evalInternal(
412 : 80724 : op[1], lambdaArgs, lambdaVals, evalAsNodeC, resultsC);
413 [ + - ]: 161448 : Trace("evaluator") << "Evaluated via arguments to "
414 : 80724 : << results[currNode].d_tag << std::endl;
415 [ - + ]: 80724 : 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 [ + - ]: 80724 : }
423 : 80724 : break;
424 : 4846040 : case Kind::CONST_BOOLEAN:
425 : 4846040 : results[currNode] = EvalResult(currNodeVal.getConst<bool>());
426 : 4846040 : break;
427 : :
428 : 3878420 : case Kind::NOT:
429 : : {
430 : 3878420 : results[currNode] = EvalResult(!(results[currNode[0]].d_bool));
431 : 3878420 : break;
432 : : }
433 : :
434 : 2087987 : case Kind::AND:
435 : : {
436 : 2087987 : bool res = results[currNode[0]].d_bool;
437 [ + + ]: 4354986 : for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
438 : : {
439 [ + + ][ + + ]: 2266999 : res = res && results[currNode[i]].d_bool;
[ + + ][ - - ]
440 : : }
441 : 2087987 : results[currNode] = EvalResult(res);
442 : 2087987 : break;
443 : : }
444 : :
445 : 2689401 : case Kind::OR:
446 : : {
447 : 2689401 : bool res = results[currNode[0]].d_bool;
448 [ + + ]: 13241595 : for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
449 : : {
450 [ + + ][ + + ]: 10552194 : res = res || results[currNode[i]].d_bool;
[ + + ][ - - ]
451 : : }
452 : 2689401 : results[currNode] = EvalResult(res);
453 : 2689401 : break;
454 : : }
455 : 507 : case Kind::IMPLIES:
456 : : {
457 : : bool res =
458 : 507 : !results[currNode[0]].d_bool || results[currNode[1]].d_bool;
459 : 507 : results[currNode] = EvalResult(res);
460 : 507 : break;
461 : : }
462 : 21457 : case Kind::XOR:
463 : : {
464 : 21457 : bool res = results[currNode[0]].d_bool;
465 [ + + ]: 42914 : for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
466 : : {
467 : 21457 : res = res != results[currNode[i]].d_bool;
468 : : }
469 : 21457 : results[currNode] = EvalResult(res);
470 : 21457 : break;
471 : : }
472 : :
473 : 3941193 : case Kind::CONST_RATIONAL:
474 : : case Kind::CONST_INTEGER:
475 : : {
476 : 3941193 : const Rational& r = currNodeVal.getConst<Rational>();
477 : 3941193 : results[currNode] = EvalResult(r);
478 : 3941193 : 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 : 1132619 : case Kind::ADD:
488 : : {
489 : 1132619 : Rational res = results[currNode[0]].d_rat;
490 [ + + ]: 2911000 : for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
491 : : {
492 : 1778381 : res = res + results[currNode[i]].d_rat;
493 : : }
494 : 1132619 : results[currNode] = EvalResult(res);
495 : 1132619 : break;
496 : 1132619 : }
497 : :
498 : 52686 : case Kind::SUB:
499 : : {
500 : 52686 : const Rational& x = results[currNode[0]].d_rat;
501 : 52686 : const Rational& y = results[currNode[1]].d_rat;
502 : 52686 : results[currNode] = EvalResult(x - y);
503 : 52686 : break;
504 : : }
505 : :
506 : 14368 : case Kind::NEG:
507 : : {
508 : 14368 : const Rational& x = results[currNode[0]].d_rat;
509 : 14368 : results[currNode] = EvalResult(-x);
510 : 14368 : break;
511 : : }
512 : 723351 : case Kind::MULT:
513 : : case Kind::NONLINEAR_MULT:
514 : : {
515 : 723351 : Rational res = results[currNode[0]].d_rat;
516 [ + + ]: 1447353 : for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
517 : : {
518 : 724002 : res = res * results[currNode[i]].d_rat;
519 : : }
520 : 723351 : results[currNode] = EvalResult(res);
521 : 723351 : break;
522 : 723351 : }
523 : 74945 : 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 : 74945 : Rational res = results[currNode[0]].d_rat;
531 : 74945 : bool divbyzero = false;
532 : 74945 : Kind k = currNodeVal.getKind();
533 [ + + ][ + + ]: 74945 : bool isReal = (k == Kind::DIVISION || k == Kind::DIVISION_TOTAL);
534 : 74945 : bool isMod =
535 [ + + ][ + + ]: 74945 : (k == Kind::INTS_MODULUS || k == Kind::INTS_MODULUS_TOTAL);
536 [ + + ]: 149029 : for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
537 : : {
538 [ + + ]: 74945 : if (results[currNode[i]].d_rat.isZero())
539 : : {
540 [ + + ][ + + ]: 881 : if (k == Kind::DIVISION_TOTAL || k == Kind::INTS_DIVISION_TOTAL)
541 : : {
542 : 20 : res = Rational(0);
543 : 20 : continue;
544 : : }
545 [ - + ]: 861 : else if (k == Kind::INTS_MODULUS_TOTAL)
546 : : {
547 : : // result is unchanged
548 : 0 : continue;
549 : : }
550 : : else
551 : : {
552 [ + - ]: 1722 : Trace("evaluator")
553 : 861 : << "Division/modulus by zero not supported" << std::endl;
554 : 861 : divbyzero = true;
555 : 861 : results[currNode] = EvalResult();
556 : 861 : break;
557 : : }
558 : : }
559 [ + + ]: 74064 : if (isReal)
560 : : {
561 : 64034 : res = res / results[currNode[i]].d_rat;
562 : : }
563 : : else
564 : : {
565 : 10030 : Integer a = res.getNumerator();
566 : 10030 : Integer b = results[currNode[i]].d_rat.getNumerator();
567 [ + + ]: 20060 : res = Rational(isMod ? a.euclidianDivideRemainder(b)
568 : 10030 : : a.euclidianDivideQuotient(b));
569 : 10030 : }
570 : : }
571 [ + + ]: 74945 : if (divbyzero)
572 : : {
573 : 861 : processUnhandled(
574 : : currNode, currNodeVal, evalAsNode, results, needsReconstruct);
575 : : }
576 : : else
577 : : {
578 : 74084 : results[currNode] = EvalResult(res);
579 : : }
580 : 74945 : break;
581 : 74945 : }
582 : 754172 : case Kind::GEQ:
583 : : {
584 : 754172 : const Rational& x = results[currNode[0]].d_rat;
585 : 754172 : const Rational& y = results[currNode[1]].d_rat;
586 : 754172 : results[currNode] = EvalResult(x >= y);
587 : 754172 : break;
588 : : }
589 : 6695 : case Kind::LEQ:
590 : : {
591 : 6695 : const Rational& x = results[currNode[0]].d_rat;
592 : 6695 : const Rational& y = results[currNode[1]].d_rat;
593 : 6695 : results[currNode] = EvalResult(x <= y);
594 : 6695 : break;
595 : : }
596 : 15157 : case Kind::GT:
597 : : {
598 : 15157 : const Rational& x = results[currNode[0]].d_rat;
599 : 15157 : const Rational& y = results[currNode[1]].d_rat;
600 : 15157 : results[currNode] = EvalResult(x > y);
601 : 15157 : break;
602 : : }
603 : 106311 : case Kind::LT:
604 : : {
605 : 106311 : const Rational& x = results[currNode[0]].d_rat;
606 : 106311 : const Rational& y = results[currNode[1]].d_rat;
607 : 106311 : results[currNode] = EvalResult(x < y);
608 : 106311 : break;
609 : : }
610 : 1271 : case Kind::ABS:
611 : : {
612 : 1271 : const Rational& x = results[currNode[0]].d_rat;
613 : 1271 : results[currNode] = EvalResult(x.abs());
614 : 1271 : break;
615 : : }
616 : 24787 : case Kind::TO_REAL:
617 : : {
618 : : // casting to real is a no-op
619 : 24787 : const Rational& x = results[currNode[0]].d_rat;
620 : 24787 : results[currNode] = EvalResult(x);
621 : 24787 : break;
622 : : }
623 : 556 : case Kind::TO_INTEGER:
624 : : {
625 : : // casting to int takes the floor
626 : 556 : const Rational& x = results[currNode[0]].d_rat.floor();
627 : 556 : results[currNode] = EvalResult(x);
628 : 556 : break;
629 : 556 : }
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 : 12150 : case Kind::POW2:
637 : : {
638 : 12150 : const Rational& x = results[currNode[0]].d_rat;
639 : 12150 : bool valid = false;
640 [ + + ]: 12150 : if (x.sgn() < 0)
641 : : {
642 : 25 : results[currNode] = EvalResult(Rational(0));
643 : 25 : valid = true;
644 : : }
645 [ + + ]: 12125 : else if (x.getNumerator().fitsUnsignedInt())
646 : : {
647 : 12109 : uint32_t value = x.getNumerator().toUnsignedInt();
648 [ + - ]: 12109 : if (value <= 256)
649 : : {
650 : 12109 : valid = true;
651 : 12109 : results[currNode] = EvalResult(Rational(Integer(2).pow(value)));
652 : : }
653 : : }
654 [ + + ]: 12150 : if (!valid)
655 : : {
656 : 16 : processUnhandled(
657 : : currNode, currNodeVal, evalAsNode, results, needsReconstruct);
658 : : }
659 : 12150 : break;
660 : : }
661 : 189 : case Kind::INTS_ISPOW2:
662 : : {
663 : 189 : const Rational& x = results[currNode[0]].d_rat;
664 : 189 : results[currNode] = EvalResult(x.getNumerator().isPow2());
665 : 189 : break;
666 : : }
667 : 627 : case Kind::INTS_LOG2:
668 : : {
669 : 627 : const Rational& x = results[currNode[0]].d_rat;
670 [ - + ]: 627 : if (x.sgn() < 0)
671 : : {
672 : 0 : results[currNode] = EvalResult(Rational(0));
673 : : }
674 : : else
675 : : {
676 : 627 : results[currNode] =
677 : 1254 : EvalResult(Rational(x.getNumerator().length() - 1));
678 : : }
679 : 627 : break;
680 : : }
681 : 194236 : case Kind::CONST_STRING:
682 : 194236 : results[currNode] = EvalResult(currNodeVal.getConst<String>());
683 : 194236 : break;
684 : :
685 : 5548 : case Kind::STRING_CONCAT:
686 : : {
687 : 5548 : String res = results[currNode[0]].d_str;
688 [ + + ]: 18534 : for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
689 : : {
690 : 12986 : res = res.concat(results[currNode[i]].d_str);
691 : : }
692 : 5548 : results[currNode] = EvalResult(res);
693 : 5548 : break;
694 : 5548 : }
695 : :
696 : 13158 : case Kind::STRING_LENGTH:
697 : : {
698 : 13158 : const String& s = results[currNode[0]].d_str;
699 : 13158 : results[currNode] = EvalResult(Rational(s.size()));
700 : 13158 : break;
701 : : }
702 : :
703 : 7407 : case Kind::STRING_SUBSTR:
704 : : {
705 : 7407 : const String& s = results[currNode[0]].d_str;
706 : 7407 : Integer s_len(s.size());
707 : 7407 : Integer i = results[currNode[1]].d_rat.getNumerator();
708 : 7407 : Integer j = results[currNode[2]].d_rat.getNumerator();
709 : :
710 [ + + ][ + + ]: 7407 : if (i.strictlyNegative() || j.strictlyNegative() || i >= s_len)
[ + + ][ + + ]
711 : : {
712 : 1037 : results[currNode] = EvalResult(String(""));
713 : : }
714 [ + + ]: 6370 : else if (i + j > s_len)
715 : : {
716 : 488 : results[currNode] =
717 : 976 : EvalResult(s.suffix((s_len - i).toUnsignedInt()));
718 : : }
719 : : else
720 : : {
721 : 5882 : results[currNode] =
722 : 11764 : EvalResult(s.substr(i.toUnsignedInt(), j.toUnsignedInt()));
723 : : }
724 : 7407 : break;
725 : 7407 : }
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 : 2556 : case Kind::STRING_CONTAINS:
779 : : {
780 : 2556 : const String& s = results[currNode[0]].d_str;
781 : 2556 : const String& t = results[currNode[1]].d_str;
782 : 2556 : results[currNode] = EvalResult(s.find(t) != std::string::npos);
783 : 2556 : break;
784 : : }
785 : :
786 : 470 : case Kind::STRING_INDEXOF:
787 : : {
788 : 470 : const String& s = results[currNode[0]].d_str;
789 : 470 : Integer s_len(s.size());
790 : 470 : const String& x = results[currNode[1]].d_str;
791 : 470 : Integer i = results[currNode[2]].d_rat.getNumerator();
792 : :
793 [ - + ]: 470 : if (i.strictlyNegative())
794 : : {
795 : 0 : results[currNode] = EvalResult(Rational(-1));
796 : : }
797 : : else
798 : : {
799 : 470 : size_t r = s.find(x, i.toUnsignedInt());
800 [ + + ]: 470 : if (r == std::string::npos)
801 : : {
802 : 200 : results[currNode] = EvalResult(Rational(-1));
803 : : }
804 : : else
805 : : {
806 : 270 : results[currNode] = EvalResult(Rational(r));
807 : : }
808 : : }
809 : 470 : break;
810 : 470 : }
811 : :
812 : 374 : case Kind::STRING_REPLACE:
813 : : {
814 : 374 : const String& s = results[currNode[0]].d_str;
815 : 374 : const String& x = results[currNode[1]].d_str;
816 : 374 : const String& y = results[currNode[2]].d_str;
817 : 374 : results[currNode] = EvalResult(s.replace(x, y));
818 : 374 : break;
819 : : }
820 : 64 : case Kind::STRING_REPLACE_ALL:
821 : : {
822 : 64 : const String& s = results[currNode[0]].d_str;
823 : 64 : const String& x = results[currNode[1]].d_str;
824 : 64 : const String& y = results[currNode[2]].d_str;
825 [ + + ][ + + ]: 64 : if (s.empty() || x.empty())
[ + + ]
826 : : {
827 : 52 : results[currNode] = EvalResult(s);
828 : : }
829 : : else
830 : : {
831 : 12 : const std::vector<unsigned>& svec = s.getVec();
832 : 12 : const std::vector<unsigned>& yvec = y.getVec();
833 : 12 : std::size_t sizeS = s.size();
834 : 12 : std::size_t sizeX = x.size();
835 : 12 : std::size_t index = 0;
836 : 12 : std::size_t curr = 0;
837 : 12 : std::vector<unsigned> chars;
838 : : do
839 : : {
840 : 20 : curr = s.find(x, index);
841 [ + + ]: 20 : if (curr != std::string::npos)
842 : : {
843 [ - + ]: 8 : if (curr > index)
844 : : {
845 : 0 : chars.insert(
846 : 0 : chars.end(), svec.begin() + index, svec.begin() + curr);
847 : : }
848 : 8 : chars.insert(chars.end(), yvec.begin(), yvec.end());
849 : 8 : index = curr + sizeX;
850 : : }
851 : : else
852 : : {
853 : 36 : chars.insert(
854 : 48 : chars.end(), svec.begin() + index, svec.begin() + sizeS);
855 : : }
856 [ + + ][ + - ]: 20 : } while (curr != std::string::npos && curr < sizeS);
857 : : // constant evaluation
858 : 12 : results[currNode] = EvalResult(String(chars));
859 : 12 : }
860 : 64 : 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 : 12 : case Kind::STRING_TO_LOWER:
958 : : case Kind::STRING_TO_UPPER:
959 : : {
960 : 12 : const String& s = results[currNode[0]].d_str;
961 : 12 : std::vector<unsigned> nvec = s.getVec();
962 : 12 : Kind k = currNodeVal.getKind();
963 [ + + ]: 32 : 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 : 12 : results[currNode] = EvalResult(String(nvec));
986 : 12 : break;
987 : 12 : }
988 : 78 : case Kind::STRING_LEQ:
989 : : {
990 : 78 : const String& s1 = results[currNode[0]].d_str;
991 : 78 : const String& s2 = results[currNode[1]].d_str;
992 : 78 : results[currNode] = EvalResult(s1.isLeq(s2));
993 : 78 : break;
994 : : }
995 : 673626 : case Kind::CONST_BITVECTOR:
996 : 673626 : results[currNode] = EvalResult(currNodeVal.getConst<BitVector>());
997 : 673626 : break;
998 : :
999 : 65098 : case Kind::BITVECTOR_NOT:
1000 : 65098 : results[currNode] = EvalResult(~results[currNode[0]].d_bv);
1001 : 65098 : break;
1002 : :
1003 : 9389 : case Kind::BITVECTOR_NEG:
1004 : 9389 : results[currNode] = EvalResult(-results[currNode[0]].d_bv);
1005 : 9389 : break;
1006 : :
1007 : 49995 : case Kind::BITVECTOR_EXTRACT:
1008 : : {
1009 : 49995 : unsigned lo = bv::utils::getExtractLow(currNodeVal);
1010 : 49995 : unsigned hi = bv::utils::getExtractHigh(currNodeVal);
1011 : 49995 : results[currNode] =
1012 : 99990 : EvalResult(results[currNode[0]].d_bv.extract(hi, lo));
1013 : 49995 : break;
1014 : : }
1015 : :
1016 : 30550 : case Kind::BITVECTOR_CONCAT:
1017 : : {
1018 : 30550 : BitVector res = results[currNode[0]].d_bv;
1019 [ + + ]: 69418 : for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
1020 : : {
1021 : 38868 : res = res.concat(results[currNode[i]].d_bv);
1022 : : }
1023 : 30550 : results[currNode] = EvalResult(res);
1024 : 30550 : break;
1025 : 30550 : }
1026 : :
1027 : 25916 : case Kind::BITVECTOR_ADD:
1028 : : {
1029 : 25916 : BitVector res = results[currNode[0]].d_bv;
1030 [ + + ]: 51848 : for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
1031 : : {
1032 : 25932 : res = res + results[currNode[i]].d_bv;
1033 : : }
1034 : 25916 : results[currNode] = EvalResult(res);
1035 : 25916 : break;
1036 : 25916 : }
1037 : :
1038 : 62670 : case Kind::BITVECTOR_MULT:
1039 : : {
1040 : 62670 : BitVector res = results[currNode[0]].d_bv;
1041 [ + + ]: 136086 : for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
1042 : : {
1043 : 73416 : res = res * results[currNode[i]].d_bv;
1044 : : }
1045 : 62670 : results[currNode] = EvalResult(res);
1046 : 62670 : break;
1047 : 62670 : }
1048 : 50859 : case Kind::BITVECTOR_AND:
1049 : : {
1050 : 50859 : BitVector res = results[currNode[0]].d_bv;
1051 [ + + ]: 102096 : for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
1052 : : {
1053 : 51237 : res = res & results[currNode[i]].d_bv;
1054 : : }
1055 : 50859 : results[currNode] = EvalResult(res);
1056 : 50859 : break;
1057 : 50859 : }
1058 : :
1059 : 90956 : case Kind::BITVECTOR_OR:
1060 : : {
1061 : 90956 : BitVector res = results[currNode[0]].d_bv;
1062 [ + + ]: 206486 : for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
1063 : : {
1064 : 115530 : res = res | results[currNode[i]].d_bv;
1065 : : }
1066 : 90956 : results[currNode] = EvalResult(res);
1067 : 90956 : break;
1068 : 90956 : }
1069 : :
1070 : 591 : case Kind::BITVECTOR_XOR:
1071 : : {
1072 : 591 : BitVector res = results[currNode[0]].d_bv;
1073 [ + + ]: 1186 : for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
1074 : : {
1075 : 595 : res = res ^ results[currNode[i]].d_bv;
1076 : : }
1077 : 591 : results[currNode] = EvalResult(res);
1078 : 591 : break;
1079 : 591 : }
1080 : 48556 : case Kind::BITVECTOR_UDIV:
1081 : : {
1082 : 48556 : BitVector res = results[currNode[0]].d_bv;
1083 : 48556 : res = res.unsignedDivTotal(results[currNode[1]].d_bv);
1084 : 48556 : results[currNode] = EvalResult(res);
1085 : 48556 : break;
1086 : 48556 : }
1087 : 52804 : case Kind::BITVECTOR_UREM:
1088 : : {
1089 : 52804 : BitVector res = results[currNode[0]].d_bv;
1090 : 52804 : res = res.unsignedRemTotal(results[currNode[1]].d_bv);
1091 : 52804 : results[currNode] = EvalResult(res);
1092 : 52804 : break;
1093 : 52804 : }
1094 : 378 : case Kind::BITVECTOR_SHL:
1095 : : {
1096 : 378 : BitVector res = results[currNode[0]].d_bv;
1097 : 378 : res = res.leftShift(results[currNode[1]].d_bv);
1098 : 378 : results[currNode] = EvalResult(res);
1099 : 378 : break;
1100 : 378 : }
1101 : 574 : case Kind::BITVECTOR_ASHR:
1102 : : {
1103 : 574 : BitVector res = results[currNode[0]].d_bv;
1104 : 574 : res = res.arithRightShift(results[currNode[1]].d_bv);
1105 : 574 : results[currNode] = EvalResult(res);
1106 : 574 : break;
1107 : 574 : }
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 : 48 : case Kind::BITVECTOR_SLE:
1123 : : {
1124 : 48 : BitVector res = results[currNode[0]].d_bv;
1125 : 48 : bool b = res.signedLessThanEq(results[currNode[1]].d_bv);
1126 : 48 : results[currNode] = EvalResult(b);
1127 : 48 : break;
1128 : 48 : }
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 : 515 : case Kind::BITVECTOR_UGT:
1137 : : {
1138 : 515 : BitVector res = results[currNode[1]].d_bv;
1139 : 515 : bool b = res.unsignedLessThan(results[currNode[0]].d_bv);
1140 : 515 : results[currNode] = EvalResult(b);
1141 : 515 : break;
1142 : 515 : }
1143 : 300 : case Kind::BITVECTOR_SGT:
1144 : : {
1145 : 300 : BitVector res = results[currNode[1]].d_bv;
1146 : 300 : bool b = res.signedLessThan(results[currNode[0]].d_bv);
1147 : 300 : results[currNode] = EvalResult(b);
1148 : 300 : break;
1149 : 300 : }
1150 : 707 : case Kind::BITVECTOR_SGE:
1151 : : {
1152 : 707 : BitVector res = results[currNode[1]].d_bv;
1153 : 707 : bool b = res.signedLessThanEq(results[currNode[0]].d_bv);
1154 : 707 : results[currNode] = EvalResult(b);
1155 : 707 : break;
1156 : 707 : }
1157 : 297 : case Kind::BITVECTOR_UGE:
1158 : : {
1159 : 297 : BitVector res = results[currNode[1]].d_bv;
1160 : 297 : bool b = res.unsignedLessThanEq(results[currNode[0]].d_bv);
1161 : 297 : results[currNode] = EvalResult(b);
1162 : 297 : break;
1163 : 297 : }
1164 : 3687 : case Kind::BITVECTOR_REPEAT:
1165 : : {
1166 : 3687 : BitVector res = results[currNode[0]].d_bv;
1167 : : unsigned amount =
1168 : 3687 : currNode.getOperator().getConst<BitVectorRepeat>().d_repeatAmount;
1169 : 3687 : BitVector ret = res;
1170 [ + + ]: 4042 : for (size_t i = 1; i < amount; i++)
1171 : : {
1172 : 355 : ret = ret.concat(res);
1173 : : }
1174 : 3687 : results[currNode] = EvalResult(ret);
1175 : 3687 : break;
1176 : 3687 : }
1177 : 5260 : case Kind::BITVECTOR_SIGN_EXTEND:
1178 : : {
1179 : 5260 : BitVector res = results[currNode[0]].d_bv;
1180 : 5260 : unsigned amount = currNode.getOperator()
1181 : 5260 : .getConst<BitVectorSignExtend>()
1182 : 5260 : .d_signExtendAmount;
1183 : 5260 : results[currNode] = EvalResult(res.signExtend(amount));
1184 : 5260 : break;
1185 : 5260 : }
1186 : 5610 : case Kind::BITVECTOR_ZERO_EXTEND:
1187 : : {
1188 : 5610 : BitVector res = results[currNode[0]].d_bv;
1189 : 5610 : unsigned amount = currNode.getOperator()
1190 : 5610 : .getConst<BitVectorZeroExtend>()
1191 : 5610 : .d_zeroExtendAmount;
1192 : 5610 : results[currNode] = EvalResult(res.zeroExtend(amount));
1193 : 5610 : break;
1194 : 5610 : }
1195 : :
1196 : 2767161 : case Kind::EQUAL:
1197 : : {
1198 : 2767161 : EvalResult lhs = results[currNode[0]];
1199 : 2767161 : EvalResult rhs = results[currNode[1]];
1200 : :
1201 [ + + ][ + + ]: 2767161 : switch (lhs.d_tag)
[ + - ]
1202 : : {
1203 : 846596 : case EvalResult::BOOL:
1204 : : {
1205 : 846596 : results[currNode] = EvalResult(lhs.d_bool == rhs.d_bool);
1206 : 846596 : break;
1207 : : }
1208 : :
1209 : 44630 : case EvalResult::BITVECTOR:
1210 : : {
1211 : 44630 : results[currNode] = EvalResult(lhs.d_bv == rhs.d_bv);
1212 : 44630 : break;
1213 : : }
1214 : :
1215 : 1869703 : case EvalResult::RATIONAL:
1216 : : {
1217 : 1869703 : results[currNode] = EvalResult(lhs.d_rat == rhs.d_rat);
1218 : 1869703 : break;
1219 : : }
1220 : :
1221 : 6208 : case EvalResult::STRING:
1222 : : {
1223 : 6208 : results[currNode] = EvalResult(lhs.d_str == rhs.d_str);
1224 : 6208 : 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 : 2767161 : break;
1245 : 2767161 : }
1246 : :
1247 : 3786409 : case Kind::ITE:
1248 : : {
1249 [ + + ]: 3786409 : if (results[currNode[0]].d_bool)
1250 : : {
1251 : 1376388 : results[currNode] = results[currNode[1]];
1252 : : }
1253 : : else
1254 : : {
1255 : 2410021 : results[currNode] = results[currNode[2]];
1256 : : }
1257 : 3786409 : break;
1258 : : }
1259 : 8952 : case Kind::BITVECTOR_UBV_TO_INT:
1260 : : {
1261 : 8952 : BitVector res = results[currNode[0]].d_bv;
1262 : 8952 : results[currNode] = EvalResult(Rational(res.toInteger()));
1263 : 8952 : break;
1264 : 8952 : }
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 : 6013 : case Kind::INT_TO_BITVECTOR:
1283 : : {
1284 : 6013 : Integer i = results[currNode[0]].d_rat.getNumerator();
1285 : : const uint32_t size =
1286 : 6013 : currNodeVal.getOperator().getConst<IntToBitVector>().d_size;
1287 : 6013 : results[currNode] = EvalResult(BitVector(size, i));
1288 : 6013 : break;
1289 : 6013 : }
1290 : 67473 : case Kind::CONST_BITVECTOR_SYMBOLIC:
1291 : : {
1292 : 67473 : Integer i = results[currNode[0]].d_rat.getNumerator();
1293 : 67473 : Integer w = results[currNode[1]].d_rat.getNumerator();
1294 [ + - ]: 67473 : if (w.fitsUnsignedInt())
1295 : : {
1296 [ - + ][ - + ]: 67473 : Assert(w.sgn() >= 0);
[ - - ]
1297 [ + - ]: 134946 : Trace("evaluator") << currNode << " evalutes to "
1298 [ - + ][ - - ]: 67473 : << BitVector(w.toUnsignedInt(), i) << std::endl;
1299 : 67473 : results[currNode] = EvalResult(BitVector(w.toUnsignedInt(), i));
1300 : : }
1301 : : else
1302 : : {
1303 : 0 : processUnhandled(
1304 : : currNode, currNodeVal, evalAsNode, results, needsReconstruct);
1305 : : }
1306 : 67473 : break;
1307 : 67473 : }
1308 : 25967 : case Kind::BITVECTOR_SIZE:
1309 : : {
1310 : 25967 : const TypeNode& tn = currNode[0].getType();
1311 [ + - ]: 25967 : if (tn.isBitVector())
1312 : : {
1313 : 25967 : results[currNode] = EvalResult(Rational(tn.getBitVectorSize()));
1314 : : }
1315 : : else
1316 : : {
1317 : 0 : processUnhandled(
1318 : : currNode, currNodeVal, evalAsNode, results, needsReconstruct);
1319 : : }
1320 : 25967 : break;
1321 : 25967 : }
1322 : 100305 : default:
1323 : : {
1324 [ + - ]: 200610 : Trace("evaluator") << "Kind " << currNodeVal.getKind()
1325 : 100305 : << " not supported" << std::endl;
1326 : 100305 : processUnhandled(
1327 : : currNode, currNodeVal, evalAsNode, results, needsReconstruct);
1328 : : }
1329 : : }
1330 [ + + ]: 53914887 : }
1331 [ + + ]: 86339252 : }
1332 : :
1333 : 8597872 : return results[n];
1334 : 4298936 : }
1335 : :
1336 : 20825372 : Node Evaluator::reconstruct(TNode n,
1337 : : std::unordered_map<TNode, EvalResult>& eresults,
1338 : : std::unordered_map<TNode, Node>& evalAsNode) const
1339 : : {
1340 [ + + ]: 20825372 : if (n.getNumChildren() == 0)
1341 : : {
1342 : 46684 : return n;
1343 : : }
1344 [ + - ]: 20778688 : Trace("evaluator") << "Evaluator: reconstruct " << n << std::endl;
1345 : 20778688 : NodeManager* nm = n.getNodeManager();
1346 : 20778688 : std::unordered_map<TNode, EvalResult>::iterator itr;
1347 : 20778688 : std::unordered_map<TNode, Node>::iterator itn;
1348 : 20778688 : std::vector<Node> echildren;
1349 [ + + ]: 20778688 : if (n.getMetaKind() == kind::metakind::PARAMETERIZED)
1350 : : {
1351 : 2280801 : TNode op = n.getOperator();
1352 [ + + ]: 2280801 : if (op.isConst())
1353 : : {
1354 : 1550164 : echildren.push_back(op);
1355 : : }
1356 : : else
1357 : : {
1358 : 730637 : itr = eresults.find(op);
1359 [ - + ][ - + ]: 730637 : Assert(itr != eresults.end());
[ - - ]
1360 [ + - ]: 730637 : if (itr->second.d_tag == EvalResult::INVALID)
1361 : : {
1362 : : // could not evaluate the operator, look in the node cache
1363 : 730637 : itn = evalAsNode.find(op);
1364 [ - + ][ - + ]: 730637 : Assert(itn != evalAsNode.end());
[ - - ]
1365 : 730637 : 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 : 2280801 : }
1374 [ + + ]: 62983049 : for (const auto& currNodeChild : n)
1375 : : {
1376 : 42204361 : itr = eresults.find(currNodeChild);
1377 [ - + ][ - + ]: 42204361 : Assert(itr != eresults.end());
[ - - ]
1378 [ + + ]: 42204361 : if (itr->second.d_tag == EvalResult::INVALID)
1379 : : {
1380 : : // could not evaluate this child, look in the node cache
1381 : 36056299 : itn = evalAsNode.find(currNodeChild);
1382 [ - + ][ - + ]: 36056299 : Assert(itn != evalAsNode.end());
[ - - ]
1383 [ - + ][ - + ]: 36056299 : Assert(!itn->second.isNull());
[ - - ]
1384 : 36056299 : echildren.push_back(itn->second);
1385 : : }
1386 : : else
1387 : : {
1388 : : // otherwise, use the evaluation
1389 : 6148062 : echildren.push_back(itr->second.toNode(currNodeChild.getType()));
1390 : : }
1391 : 42204361 : }
1392 : : // The value is the result of our (partially) successful evaluation
1393 : : // of the children.
1394 : 20778688 : Node nn = nm->mkNode(n.getKind(), echildren);
1395 [ + - ]: 20778688 : 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 : 20778688 : return nn;
1399 : 20778688 : }
1400 : :
1401 : 101182 : 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 : 101182 : results[n] = EvalResult();
1408 : 101182 : evalAsNode[n] =
1409 [ + + ][ + + ]: 202364 : needsReconstruct ? reconstruct(n, results, evalAsNode) : Node(nv);
[ - - ]
1410 : 101182 : }
1411 : :
1412 : : } // namespace theory
1413 : : } // namespace cvc5::internal
|
