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