src/theory/evaluator.cpp

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