GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/evaluator.cpp Lines: 377 494 76.3 %
Date: 2021-03-22 Branches: 678 1777 38.2 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file evaluator.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andres Noetzli, Andrew Reynolds
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief The Evaluator class
13
 **
14
 ** The Evaluator class.
15
 **/
16
17
#include "theory/evaluator.h"
18
19
#include "theory/bv/theory_bv_utils.h"
20
#include "theory/rewriter.h"
21
#include "theory/strings/theory_strings_utils.h"
22
#include "theory/theory.h"
23
#include "util/integer.h"
24
25
namespace CVC4 {
26
namespace theory {
27
28
2505941
EvalResult::EvalResult(const EvalResult& other)
29
{
30
2505941
  d_tag = other.d_tag;
31
2505941
  switch (d_tag)
32
  {
33
614293
    case BOOL: d_bool = other.d_bool; break;
34
736176
    case BITVECTOR:
35
736176
      new (&d_bv) BitVector;
36
736176
      d_bv = other.d_bv;
37
736176
      break;
38
798647
    case RATIONAL:
39
798647
      new (&d_rat) Rational;
40
798647
      d_rat = other.d_rat;
41
798647
      break;
42
269311
    case STRING:
43
269311
      new (&d_str) String;
44
269311
      d_str = other.d_str;
45
269311
      break;
46
    case UCONST:
47
      new (&d_uc)
48
          UninterpretedConstant(other.d_uc.getType(), other.d_uc.getIndex());
49
      break;
50
87514
    case INVALID: break;
51
  }
52
2505941
}
53
54
9970519
EvalResult& EvalResult::operator=(const EvalResult& other)
55
{
56
9970519
  if (this != &other)
57
  {
58
9970519
    d_tag = other.d_tag;
59
9970519
    switch (d_tag)
60
    {
61
4537678
      case BOOL: d_bool = other.d_bool; break;
62
2322710
      case BITVECTOR:
63
2322710
        new (&d_bv) BitVector;
64
2322710
        d_bv = other.d_bv;
65
2322710
        break;
66
2383162
      case RATIONAL:
67
2383162
        new (&d_rat) Rational;
68
2383162
        d_rat = other.d_rat;
69
2383162
        break;
70
331311
      case STRING:
71
331311
        new (&d_str) String;
72
331311
        d_str = other.d_str;
73
331311
        break;
74
      case UCONST:
75
        new (&d_uc)
76
            UninterpretedConstant(other.d_uc.getType(), other.d_uc.getIndex());
77
        break;
78
395658
      case INVALID: break;
79
    }
80
  }
81
9970519
  return *this;
82
}
83
84
42146046
EvalResult::~EvalResult()
85
{
86
21073023
  switch (d_tag)
87
  {
88
5349092
    case BITVECTOR:
89
    {
90
5349092
      d_bv.~BitVector();
91
5349092
      break;
92
    }
93
4223986
    case RATIONAL:
94
    {
95
4223986
      d_rat.~Rational();
96
4223986
      break;
97
    }
98
931819
    case STRING:
99
    {
100
931819
      d_str.~String();
101
931819
      break;
102
    }
103
    case UCONST:
104
    {
105
      d_uc.~UninterpretedConstant();
106
      break;
107
    }
108
10568126
    default: break;
109
  }
110
21073023
}
111
112
1566943
Node EvalResult::toNode() const
113
{
114
1566943
  NodeManager* nm = NodeManager::currentNM();
115
1566943
  switch (d_tag)
116
  {
117
125995
    case EvalResult::BOOL: return nm->mkConst(d_bool);
118
961357
    case EvalResult::BITVECTOR: return nm->mkConst(d_bv);
119
117119
    case EvalResult::RATIONAL: return nm->mkConst(d_rat);
120
275255
    case EvalResult::STRING: return nm->mkConst(d_str);
121
    case EvalResult::UCONST: return nm->mkConst(d_uc);
122
87217
    default:
123
    {
124
174434
      Trace("evaluator") << "Missing conversion from " << d_tag << " to node"
125
87217
                         << std::endl;
126
87217
      return Node();
127
    }
128
  }
129
}
130
131
1032807
Node Evaluator::eval(TNode n,
132
                     const std::vector<Node>& args,
133
                     const std::vector<Node>& vals,
134
                     bool useRewriter) const
135
{
136
2065614
  std::unordered_map<Node, Node, NodeHashFunction> visited;
137
2065614
  return eval(n, args, vals, visited, useRewriter);
138
}
139
1052458
Node Evaluator::eval(
140
    TNode n,
141
    const std::vector<Node>& args,
142
    const std::vector<Node>& vals,
143
    const std::unordered_map<Node, Node, NodeHashFunction>& visited,
144
    bool useRewriter) const
145
{
146
2104916
  Trace("evaluator") << "Evaluating " << n << " under substitution " << args
147
2104916
                     << " " << vals << " with visited size = " << visited.size()
148
1052458
                     << std::endl;
149
2104916
  std::unordered_map<TNode, Node, NodeHashFunction> evalAsNode;
150
2104916
  std::unordered_map<TNode, EvalResult, TNodeHashFunction> results;
151
  // add visited to results
152
1083747
  for (const std::pair<const Node, Node>& p : visited)
153
  {
154
31289
    Trace("evaluator") << "Add " << p.first << " == " << p.second << std::endl;
155
31289
    results[p.first] = evalInternal(p.second, args, vals, evalAsNode, results, useRewriter);
156
31289
    if (results[p.first].d_tag == EvalResult::INVALID)
157
    {
158
      // could not evaluate, use the evalAsNode map
159
      std::unordered_map<TNode, Node, NodeHashFunction>::iterator itn =
160
297
          evalAsNode.find(p.second);
161
297
      Assert(itn != evalAsNode.end());
162
594
      Node val = itn->second;
163
297
      if (useRewriter)
164
      {
165
297
        val = Rewriter::rewrite(val);
166
      }
167
297
      evalAsNode[p.first] = val;
168
    }
169
  }
170
1052458
  Trace("evaluator") << "Run eval internal..." << std::endl;
171
1052458
  Node ret = evalInternal(n, args, vals, evalAsNode, results, useRewriter).toNode();
172
  // if we failed to evaluate
173
1052458
  if (ret.isNull() && useRewriter)
174
  {
175
    // should be stored in the evaluation-as-node map
176
    std::unordered_map<TNode, Node, NodeHashFunction>::iterator itn =
177
87217
        evalAsNode.find(n);
178
87217
    Assert(itn != evalAsNode.end());
179
87217
    ret = Rewriter::rewrite(itn->second);
180
  }
181
  // should be the same as substitution + rewriting, or possibly null if
182
  // useRewriter is false
183
1052458
  Assert((ret.isNull() && !useRewriter)
184
         || ret
185
                == Rewriter::rewrite(n.substitute(
186
                       args.begin(), args.end(), vals.begin(), vals.end())));
187
2104916
  return ret;
188
}
189
190
1083747
EvalResult Evaluator::evalInternal(
191
    TNode n,
192
    const std::vector<Node>& args,
193
    const std::vector<Node>& vals,
194
    std::unordered_map<TNode, Node, NodeHashFunction>& evalAsNode,
195
    std::unordered_map<TNode, EvalResult, TNodeHashFunction>& results,
196
    bool useRewriter) const
197
{
198
2167494
  std::vector<TNode> queue;
199
1083747
  queue.emplace_back(n);
200
1083747
  std::unordered_map<TNode, EvalResult, TNodeHashFunction>::iterator itr;
201
202
31397675
  while (queue.size() != 0)
203
  {
204
29524455
    TNode currNode = queue.back();
205
206
15727020
    if (results.find(currNode) != results.end())
207
    {
208
570056
      queue.pop_back();
209
570056
      continue;
210
    }
211
212
14586908
    bool doProcess = true;
213
14586908
    bool isVar = false;
214
14586908
    bool doEval = true;
215
14586908
    if (currNode.isVar())
216
    {
217
      // we do not evaluate if we are a variable, instead we look for the
218
      // variable in args below
219
2601975
      isVar = true;
220
2601975
      doEval = false;
221
    }
222
11984933
    else if (currNode.getMetaKind() == kind::metakind::PARAMETERIZED)
223
    {
224
768130
      TNode op = currNode.getOperator();
225
      // Certain nodes are parameterized with constant operators, including
226
      // bitvector extract. These operators do not need to be evaluated.
227
384065
      if (!op.isConst())
228
      {
229
161036
        itr = results.find(op);
230
161036
        if (itr == results.end())
231
        {
232
68540
          queue.emplace_back(op);
233
68540
          doProcess = false;
234
        }
235
92496
        else if (itr->second.d_tag == EvalResult::INVALID)
236
        {
237
92496
          doEval = false;
238
        }
239
      }
240
    }
241
47522588
    for (const auto& currNodeChild : currNode)
242
    {
243
32935680
      itr = results.find(currNodeChild);
244
32935680
      if (itr == results.end())
245
      {
246
9356999
        queue.emplace_back(currNodeChild);
247
9356999
        doProcess = false;
248
      }
249
23578681
      else if (itr->second.d_tag == EvalResult::INVALID)
250
      {
251
        // we cannot evaluate since there was an invalid child
252
365982
        doEval = false;
253
      }
254
    }
255
29173816
    Trace("evaluator") << "Evaluator: visit " << currNode
256
14586908
                       << ", process = " << doProcess
257
14586908
                       << ", evaluate = " << doEval << std::endl;
258
259
14586908
    if (doProcess)
260
    {
261
9939230
      queue.pop_back();
262
263
19659043
      Node currNodeVal = currNode;
264
      // whether we need to reconstruct the current node in the case of failure
265
9939230
      bool needsReconstruct = true;
266
267
      // The code below should either:
268
      // (1) store a valid EvalResult into results[currNode], or
269
      // (2) store an invalid EvalResult into results[currNode] and
270
      // store the result of substitution + rewriting currNode { args -> vals }
271
      // into evalAsNode[currNode].
272
273
      // If we did not successfully evaluate all children, or are a variable
274
9939230
      if (!doEval)
275
      {
276
2839690
        if (isVar)
277
        {
278
2601975
          const auto& it = std::find(args.begin(), args.end(), currNode);
279
2681995
          if (it == args.end())
280
          {
281
            // variable with no substitution is itself
282
80020
            evalAsNode[currNode] = currNode;
283
80020
            results[currNode] = EvalResult();
284
80020
            continue;
285
          }
286
2521955
          ptrdiff_t pos = std::distance(args.begin(), it);
287
2521955
          currNodeVal = vals[pos];
288
          // Don't need to rewrite since range of substitution should already
289
          // be normalized.
290
        }
291
        else
292
        {
293
          // Reconstruct the node with a combination of the children that
294
          // successfully evaluated, and the children that did not.
295
237715
          Trace("evaluator") << "Evaluator: collect arguments" << std::endl;
296
237715
          currNodeVal = reconstruct(currNodeVal, results, evalAsNode);
297
237715
          if (useRewriter)
298
          {
299
            // Rewrite the result now, if we use the rewriter. We will see below
300
            // if we are able to turn it into a valid EvalResult.
301
237715
            currNodeVal = Rewriter::rewrite(currNodeVal);
302
          }
303
        }
304
2759670
        needsReconstruct = false;
305
5519340
        Trace("evaluator") << "Evaluator: now after substitution + rewriting: "
306
2759670
                           << currNodeVal << std::endl;
307
2899067
        if (currNodeVal.getNumChildren() > 0)
308
        {
309
          // We may continue with a valid EvalResult at this point only if
310
          // we have no children. We must otherwise fail here since some of
311
          // our children may not have successful evaluations.
312
139397
          results[currNode] = EvalResult();
313
139397
          evalAsNode[currNode] = currNodeVal;
314
139397
          continue;
315
        }
316
        // Otherwise, we may be able to turn the overall result into an
317
        // valid EvalResult and continue. We fallthrough and continue with the
318
        // block of code below.
319
      }
320
321
9719813
      Trace("evaluator") << "Current node val : " << currNodeVal << std::endl;
322
323
9719813
      switch (currNodeVal.getKind())
324
      {
325
        // APPLY_UF is a special case where we look up the operator and apply
326
        // beta reduction if possible
327
        case kind::APPLY_UF:
328
        {
329
          Trace("evaluator") << "Evaluate " << currNode << std::endl;
330
          TNode op = currNode.getOperator();
331
          Assert(evalAsNode.find(op) != evalAsNode.end());
332
          // no function can be a valid EvalResult
333
          op = evalAsNode[op];
334
          Trace("evaluator") << "Operator evaluated to " << op << std::endl;
335
          if (op.getKind() != kind::LAMBDA)
336
          {
337
            // this node is not evaluatable due to operator, must add to
338
            // evalAsNode
339
            results[currNode] = EvalResult();
340
            evalAsNode[currNode] = reconstruct(currNode, results, evalAsNode);
341
            continue;
342
          }
343
          // Create a copy of the current substitutions
344
          std::vector<Node> lambdaArgs(args);
345
          std::vector<Node> lambdaVals(vals);
346
347
          // Add the values for the arguments of the lambda as substitutions at
348
          // the beginning of the vector to shadow variables from outer scopes
349
          // with the same name
350
          for (const auto& lambdaArg : op[0])
351
          {
352
            lambdaArgs.insert(lambdaArgs.begin(), lambdaArg);
353
          }
354
355
          for (const auto& lambdaVal : currNode)
356
          {
357
            lambdaVals.insert(lambdaVals.begin(), results[lambdaVal].toNode());
358
          }
359
360
          // Lambdas are evaluated in a recursive fashion because each
361
          // evaluation requires different substitutions. We use a fresh cache
362
          // since the evaluation of op[1] is under a new substitution and thus
363
          // should not be cached. We could alternatively copy evalAsNode to
364
          // evalAsNodeC but favor avoiding this copy for performance reasons.
365
          std::unordered_map<TNode, Node, NodeHashFunction> evalAsNodeC;
366
          std::unordered_map<TNode, EvalResult, TNodeHashFunction> resultsC;
367
          results[currNode] = evalInternal(op[1],
368
                                           lambdaArgs,
369
                                           lambdaVals,
370
                                           evalAsNodeC,
371
                                           resultsC,
372
                                           useRewriter);
373
          Trace("evaluator") << "Evaluated via arguments to "
374
                             << results[currNode].d_tag << std::endl;
375
          if (results[currNode].d_tag == EvalResult::INVALID)
376
          {
377
            // evaluation was invalid, we take the node of op[1] as the result
378
            evalAsNode[currNode] = evalAsNodeC[op[1]];
379
            Trace("evaluator")
380
                << "Take node evaluation: " << evalAsNodeC[op[1]] << std::endl;
381
          }
382
        }
383
        break;
384
1087186
        case kind::CONST_BOOLEAN:
385
1087186
          results[currNode] = EvalResult(currNodeVal.getConst<bool>());
386
1087186
          break;
387
388
1326687
        case kind::NOT:
389
        {
390
1326687
          results[currNode] = EvalResult(!(results[currNode[0]].d_bool));
391
1326687
          break;
392
        }
393
394
904763
        case kind::AND:
395
        {
396
904763
          bool res = results[currNode[0]].d_bool;
397
8389768
          for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
398
          {
399
7485005
            res = res && results[currNode[i]].d_bool;
400
          }
401
904763
          results[currNode] = EvalResult(res);
402
904763
          break;
403
        }
404
405
177167
        case kind::OR:
406
        {
407
177167
          bool res = results[currNode[0]].d_bool;
408
1706192
          for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
409
          {
410
1529025
            res = res || results[currNode[i]].d_bool;
411
          }
412
177167
          results[currNode] = EvalResult(res);
413
177167
          break;
414
        }
415
416
666472
        case kind::CONST_RATIONAL:
417
        {
418
666472
          const Rational& r = currNodeVal.getConst<Rational>();
419
666472
          results[currNode] = EvalResult(r);
420
666472
          break;
421
        }
422
        case kind::UNINTERPRETED_CONSTANT:
423
        {
424
          const UninterpretedConstant& uc =
425
              currNodeVal.getConst<UninterpretedConstant>();
426
          results[currNode] = EvalResult(uc);
427
          break;
428
        }
429
346418
        case kind::PLUS:
430
        {
431
692836
          Rational res = results[currNode[0]].d_rat;
432
797179
          for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
433
          {
434
450761
            res = res + results[currNode[i]].d_rat;
435
          }
436
346418
          results[currNode] = EvalResult(res);
437
346418
          break;
438
        }
439
440
3326
        case kind::MINUS:
441
        {
442
3326
          const Rational& x = results[currNode[0]].d_rat;
443
3326
          const Rational& y = results[currNode[1]].d_rat;
444
3326
          results[currNode] = EvalResult(x - y);
445
3326
          break;
446
        }
447
448
        case kind::UMINUS:
449
        {
450
          const Rational& x = results[currNode[0]].d_rat;
451
          results[currNode] = EvalResult(-x);
452
          break;
453
        }
454
24443
        case kind::MULT:
455
        case kind::NONLINEAR_MULT:
456
        {
457
48886
          Rational res = results[currNode[0]].d_rat;
458
48910
          for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
459
          {
460
24467
            res = res * results[currNode[i]].d_rat;
461
          }
462
24443
          results[currNode] = EvalResult(res);
463
24443
          break;
464
        }
465
466
313681
        case kind::GEQ:
467
        {
468
313681
          const Rational& x = results[currNode[0]].d_rat;
469
313681
          const Rational& y = results[currNode[1]].d_rat;
470
313681
          results[currNode] = EvalResult(x >= y);
471
313681
          break;
472
        }
473
16483
        case kind::LEQ:
474
        {
475
16483
          const Rational& x = results[currNode[0]].d_rat;
476
16483
          const Rational& y = results[currNode[1]].d_rat;
477
16483
          results[currNode] = EvalResult(x <= y);
478
16483
          break;
479
        }
480
        case kind::GT:
481
        {
482
          const Rational& x = results[currNode[0]].d_rat;
483
          const Rational& y = results[currNode[1]].d_rat;
484
          results[currNode] = EvalResult(x > y);
485
          break;
486
        }
487
        case kind::LT:
488
        {
489
          const Rational& x = results[currNode[0]].d_rat;
490
          const Rational& y = results[currNode[1]].d_rat;
491
          results[currNode] = EvalResult(x < y);
492
          break;
493
        }
494
        case kind::ABS:
495
        {
496
          const Rational& x = results[currNode[0]].d_rat;
497
          results[currNode] = EvalResult(x.abs());
498
          break;
499
        }
500
299555
        case kind::CONST_STRING:
501
299555
          results[currNode] = EvalResult(currNodeVal.getConst<String>());
502
299555
          break;
503
504
24780
        case kind::STRING_CONCAT:
505
        {
506
49560
          String res = results[currNode[0]].d_str;
507
49602
          for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
508
          {
509
24822
            res = res.concat(results[currNode[i]].d_str);
510
          }
511
24780
          results[currNode] = EvalResult(res);
512
24780
          break;
513
        }
514
515
1506
        case kind::STRING_LENGTH:
516
        {
517
1506
          const String& s = results[currNode[0]].d_str;
518
1506
          results[currNode] = EvalResult(Rational(s.size()));
519
1506
          break;
520
        }
521
522
6520
        case kind::STRING_SUBSTR:
523
        {
524
6520
          const String& s = results[currNode[0]].d_str;
525
13040
          Integer s_len(s.size());
526
13040
          Integer i = results[currNode[1]].d_rat.getNumerator();
527
13040
          Integer j = results[currNode[2]].d_rat.getNumerator();
528
529
6520
          if (i.strictlyNegative() || j.strictlyNegative() || i >= s_len)
530
          {
531
895
            results[currNode] = EvalResult(String(""));
532
          }
533
5625
          else if (i + j > s_len)
534
          {
535
440
            results[currNode] =
536
880
                EvalResult(s.suffix((s_len - i).toUnsignedInt()));
537
          }
538
          else
539
          {
540
5185
            results[currNode] =
541
10370
                EvalResult(s.substr(i.toUnsignedInt(), j.toUnsignedInt()));
542
          }
543
6520
          break;
544
        }
545
546
        case kind::STRING_UPDATE:
547
        {
548
          const String& s = results[currNode[0]].d_str;
549
          Integer s_len(s.size());
550
          Integer i = results[currNode[1]].d_rat.getNumerator();
551
          const String& t = results[currNode[2]].d_str;
552
553
          if (i.strictlyNegative() || i >= s_len)
554
          {
555
            results[currNode] = EvalResult(s);
556
          }
557
          else
558
          {
559
            results[currNode] = EvalResult(s.update(i.toUnsignedInt(), t));
560
          }
561
          break;
562
        }
563
        case kind::STRING_CHARAT:
564
        {
565
          const String& s = results[currNode[0]].d_str;
566
          Integer s_len(s.size());
567
          Integer i = results[currNode[1]].d_rat.getNumerator();
568
          if (i.strictlyNegative() || i >= s_len)
569
          {
570
            results[currNode] = EvalResult(String(""));
571
          }
572
          else
573
          {
574
            results[currNode] = EvalResult(s.substr(i.toUnsignedInt(), 1));
575
          }
576
          break;
577
        }
578
579
558
        case kind::STRING_STRCTN:
580
        {
581
558
          const String& s = results[currNode[0]].d_str;
582
558
          const String& t = results[currNode[1]].d_str;
583
558
          results[currNode] = EvalResult(s.find(t) != std::string::npos);
584
558
          break;
585
        }
586
587
8
        case kind::STRING_STRIDOF:
588
        {
589
8
          const String& s = results[currNode[0]].d_str;
590
16
          Integer s_len(s.size());
591
8
          const String& x = results[currNode[1]].d_str;
592
16
          Integer i = results[currNode[2]].d_rat.getNumerator();
593
594
8
          if (i.strictlyNegative())
595
          {
596
            results[currNode] = EvalResult(Rational(-1));
597
          }
598
          else
599
          {
600
8
            size_t r = s.find(x, i.toUnsignedInt());
601
8
            if (r == std::string::npos)
602
            {
603
6
              results[currNode] = EvalResult(Rational(-1));
604
            }
605
            else
606
            {
607
2
              results[currNode] = EvalResult(Rational(r));
608
            }
609
          }
610
8
          break;
611
        }
612
613
339
        case kind::STRING_STRREPL:
614
        {
615
339
          const String& s = results[currNode[0]].d_str;
616
339
          const String& x = results[currNode[1]].d_str;
617
339
          const String& y = results[currNode[2]].d_str;
618
339
          results[currNode] = EvalResult(s.replace(x, y));
619
339
          break;
620
        }
621
622
        case kind::STRING_PREFIX:
623
        {
624
          const String& t = results[currNode[0]].d_str;
625
          const String& s = results[currNode[1]].d_str;
626
          if (s.size() < t.size())
627
          {
628
            results[currNode] = EvalResult(false);
629
          }
630
          else
631
          {
632
            results[currNode] = EvalResult(s.prefix(t.size()) == t);
633
          }
634
          break;
635
        }
636
637
        case kind::STRING_SUFFIX:
638
        {
639
          const String& t = results[currNode[0]].d_str;
640
          const String& s = results[currNode[1]].d_str;
641
          if (s.size() < t.size())
642
          {
643
            results[currNode] = EvalResult(false);
644
          }
645
          else
646
          {
647
            results[currNode] = EvalResult(s.suffix(t.size()) == t);
648
          }
649
          break;
650
        }
651
652
3
        case kind::STRING_ITOS:
653
        {
654
6
          Integer i = results[currNode[0]].d_rat.getNumerator();
655
3
          if (i.strictlyNegative())
656
          {
657
1
            results[currNode] = EvalResult(String(""));
658
          }
659
          else
660
          {
661
2
            results[currNode] = EvalResult(String(i.toString()));
662
          }
663
3
          break;
664
        }
665
666
        case kind::STRING_STOI:
667
        {
668
          const String& s = results[currNode[0]].d_str;
669
          if (s.isNumber())
670
          {
671
            results[currNode] = EvalResult(Rational(s.toNumber()));
672
          }
673
          else
674
          {
675
            results[currNode] = EvalResult(Rational(-1));
676
          }
677
          break;
678
        }
679
680
        case kind::STRING_FROM_CODE:
681
        {
682
          Integer i = results[currNode[0]].d_rat.getNumerator();
683
          if (i >= 0 && i < strings::utils::getAlphabetCardinality())
684
          {
685
            std::vector<unsigned> svec = {i.toUnsignedInt()};
686
            results[currNode] = EvalResult(String(svec));
687
          }
688
          else
689
          {
690
            results[currNode] = EvalResult(String(""));
691
          }
692
          break;
693
        }
694
695
4
        case kind::STRING_TO_CODE:
696
        {
697
4
          const String& s = results[currNode[0]].d_str;
698
4
          if (s.size() == 1)
699
          {
700
2
            results[currNode] = EvalResult(Rational(s.getVec()[0]));
701
          }
702
          else
703
          {
704
2
            results[currNode] = EvalResult(Rational(-1));
705
          }
706
4
          break;
707
        }
708
709
1323116
        case kind::CONST_BITVECTOR:
710
1323116
          results[currNode] = EvalResult(currNodeVal.getConst<BitVector>());
711
1323116
          break;
712
713
115057
        case kind::BITVECTOR_NOT:
714
115057
          results[currNode] = EvalResult(~results[currNode[0]].d_bv);
715
115057
          break;
716
717
39269
        case kind::BITVECTOR_NEG:
718
39269
          results[currNode] = EvalResult(-results[currNode[0]].d_bv);
719
39269
          break;
720
721
134850
        case kind::BITVECTOR_EXTRACT:
722
        {
723
134850
          unsigned lo = bv::utils::getExtractLow(currNodeVal);
724
134850
          unsigned hi = bv::utils::getExtractHigh(currNodeVal);
725
134850
          results[currNode] =
726
269700
              EvalResult(results[currNode[0]].d_bv.extract(hi, lo));
727
134850
          break;
728
        }
729
730
87611
        case kind::BITVECTOR_CONCAT:
731
        {
732
175222
          BitVector res = results[currNode[0]].d_bv;
733
183256
          for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
734
          {
735
95645
            res = res.concat(results[currNode[i]].d_bv);
736
          }
737
87611
          results[currNode] = EvalResult(res);
738
87611
          break;
739
        }
740
741
70702
        case kind::BITVECTOR_PLUS:
742
        {
743
141404
          BitVector res = results[currNode[0]].d_bv;
744
141404
          for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
745
          {
746
70702
            res = res + results[currNode[i]].d_bv;
747
          }
748
70702
          results[currNode] = EvalResult(res);
749
70702
          break;
750
        }
751
752
114958
        case kind::BITVECTOR_MULT:
753
        {
754
229916
          BitVector res = results[currNode[0]].d_bv;
755
246862
          for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
756
          {
757
131904
            res = res * results[currNode[i]].d_bv;
758
          }
759
114958
          results[currNode] = EvalResult(res);
760
114958
          break;
761
        }
762
98991
        case kind::BITVECTOR_AND:
763
        {
764
197982
          BitVector res = results[currNode[0]].d_bv;
765
198360
          for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
766
          {
767
99369
            res = res & results[currNode[i]].d_bv;
768
          }
769
98991
          results[currNode] = EvalResult(res);
770
98991
          break;
771
        }
772
773
204354
        case kind::BITVECTOR_OR:
774
        {
775
408708
          BitVector res = results[currNode[0]].d_bv;
776
445569
          for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
777
          {
778
241215
            res = res | results[currNode[i]].d_bv;
779
          }
780
204354
          results[currNode] = EvalResult(res);
781
204354
          break;
782
        }
783
784
128
        case kind::BITVECTOR_XOR:
785
        {
786
256
          BitVector res = results[currNode[0]].d_bv;
787
256
          for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
788
          {
789
128
            res = res ^ results[currNode[i]].d_bv;
790
          }
791
128
          results[currNode] = EvalResult(res);
792
128
          break;
793
        }
794
48498
        case kind::BITVECTOR_UDIV:
795
        {
796
96996
          BitVector res = results[currNode[0]].d_bv;
797
48498
          res = res.unsignedDivTotal(results[currNode[1]].d_bv);
798
48498
          results[currNode] = EvalResult(res);
799
48498
          break;
800
        }
801
52672
        case kind::BITVECTOR_UREM:
802
        {
803
105344
          BitVector res = results[currNode[0]].d_bv;
804
52672
          res = res.unsignedRemTotal(results[currNode[1]].d_bv);
805
52672
          results[currNode] = EvalResult(res);
806
52672
          break;
807
        }
808
809
711097
        case kind::EQUAL:
810
        {
811
1422194
          EvalResult lhs = results[currNode[0]];
812
1422194
          EvalResult rhs = results[currNode[1]];
813
814
711097
          switch (lhs.d_tag)
815
          {
816
250612
            case EvalResult::BOOL:
817
            {
818
250612
              results[currNode] = EvalResult(lhs.d_bool == rhs.d_bool);
819
250612
              break;
820
            }
821
822
69886
            case EvalResult::BITVECTOR:
823
            {
824
69886
              results[currNode] = EvalResult(lhs.d_bv == rhs.d_bv);
825
69886
              break;
826
            }
827
828
389507
            case EvalResult::RATIONAL:
829
            {
830
389507
              results[currNode] = EvalResult(lhs.d_rat == rhs.d_rat);
831
389507
              break;
832
            }
833
834
1092
            case EvalResult::STRING:
835
            {
836
1092
              results[currNode] = EvalResult(lhs.d_str == rhs.d_str);
837
1092
              break;
838
            }
839
            case EvalResult::UCONST:
840
            {
841
              results[currNode] = EvalResult(lhs.d_uc == rhs.d_uc);
842
              break;
843
            }
844
845
            default:
846
            {
847
              Trace("evaluator") << "Theory " << Theory::theoryOf(currNode[0])
848
                                 << " not supported" << std::endl;
849
              results[currNode] = EvalResult();
850
              evalAsNode[currNode] =
851
                  needsReconstruct ? reconstruct(currNode, results, evalAsNode)
852
                                   : currNodeVal;
853
              break;
854
            }
855
          }
856
857
711097
          break;
858
        }
859
860
1342667
        case kind::ITE:
861
        {
862
1342667
          if (results[currNode[0]].d_bool)
863
          {
864
466138
            results[currNode] = results[currNode[1]];
865
          }
866
          else
867
          {
868
876529
            results[currNode] = results[currNode[2]];
869
          }
870
1342667
          break;
871
        }
872
873
175944
        default:
874
        {
875
351888
          Trace("evaluator") << "Kind " << currNodeVal.getKind()
876
175944
                             << " not supported" << std::endl;
877
175944
          results[currNode] = EvalResult();
878
175944
          evalAsNode[currNode] =
879
351888
              needsReconstruct ? reconstruct(currNode, results, evalAsNode)
880
                               : currNodeVal;
881
        }
882
      }
883
    }
884
  }
885
886
2167494
  return results[n];
887
}
888
889
397150
Node Evaluator::reconstruct(
890
    TNode n,
891
    std::unordered_map<TNode, EvalResult, TNodeHashFunction>& eresults,
892
    std::unordered_map<TNode, Node, NodeHashFunction>& evalAsNode) const
893
{
894
397150
  if (n.getNumChildren() == 0)
895
  {
896
4260
    return n;
897
  }
898
392890
  Trace("evaluator") << "Evaluator: reconstruct " << n << std::endl;
899
392890
  NodeManager* nm = NodeManager::currentNM();
900
392890
  std::unordered_map<TNode, EvalResult, TNodeHashFunction>::iterator itr;
901
392890
  std::unordered_map<TNode, Node, NodeHashFunction>::iterator itn;
902
785780
  std::vector<Node> echildren;
903
392890
  if (n.getMetaKind() == kind::metakind::PARAMETERIZED)
904
  {
905
158114
    TNode op = n.getOperator();
906
79057
    if (op.isConst())
907
    {
908
390
      echildren.push_back(op);
909
    }
910
    else
911
    {
912
78667
      itr = eresults.find(op);
913
78667
      Assert(itr != eresults.end());
914
78667
      if (itr->second.d_tag == EvalResult::INVALID)
915
      {
916
        // could not evaluate the operator, look in the node cache
917
78667
        itn = evalAsNode.find(op);
918
78667
        Assert(itn != evalAsNode.end());
919
78667
        echildren.push_back(itn->second);
920
      }
921
      else
922
      {
923
        // otherwise, use the evaluation of the operator
924
        echildren.push_back(itr->second.toNode());
925
      }
926
    }
927
  }
928
1218188
  for (const auto& currNodeChild : n)
929
  {
930
825298
    itr = eresults.find(currNodeChild);
931
825298
    Assert(itr != eresults.end());
932
825298
    if (itr->second.d_tag == EvalResult::INVALID)
933
    {
934
      // could not evaluate this child, look in the node cache
935
310813
      itn = evalAsNode.find(currNodeChild);
936
310813
      Assert(itn != evalAsNode.end());
937
310813
      echildren.push_back(itn->second);
938
    }
939
    else
940
    {
941
      // otherwise, use the evaluation
942
514485
      echildren.push_back(itr->second.toNode());
943
    }
944
  }
945
  // The value is the result of our (partially) successful evaluation
946
  // of the children.
947
785780
  Node nn = nm->mkNode(n.getKind(), echildren);
948
392890
  Trace("evaluator") << "Evaluator: reconstructed " << nn << std::endl;
949
  // Return node, without rewriting. Notice we do not need to substitute here
950
  // since all substitutions should already have been applied recursively.
951
392890
  return nn;
952
}
953
954
}  // namespace theory
955
26676
}  // namespace CVC4