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 UCONST:
  47       new (&d_uc)
  48           UninterpretedConstant(other.d_uc.getType(), other.d_uc.getIndex());
  49       break;
  50     case INVALID: break;
  51   }
  52 }
  53
  54 EvalResult& EvalResult::operator=(const EvalResult& other)
  55 {
  56   if (this != &other)
  57   {
  58     d_tag = other.d_tag;
  59     switch (d_tag)
  60     {
  61       case BOOL: d_bool = other.d_bool; break;
  62       case BITVECTOR:
  63         new (&d_bv) BitVector;
  64         d_bv = other.d_bv;
  65         break;
  66       case RATIONAL:
  67         new (&d_rat) Rational;
  68         d_rat = other.d_rat;
  69         break;
  70       case STRING:
  71         new (&d_str) String;
  72         d_str = other.d_str;
  73         break;
  74       case UCONST:
  75         new (&d_uc)
  76             UninterpretedConstant(other.d_uc.getType(), other.d_uc.getIndex());
  77         break;
  78       case INVALID: break;
  79     }
  80   }
  81   return *this;
  82 }
  83
  84 EvalResult::~EvalResult()
  85 {
  86   switch (d_tag)
  87   {
  88     case BITVECTOR:
  89     {
  90       d_bv.~BitVector();
  91       break;
  92     }
  93     case RATIONAL:
  94     {
  95       d_rat.~Rational();
  96       break;
  97     }
  98     case STRING:
  99     {
 100       d_str.~String();
 101       break;
 102     }
 103     case UCONST:
 104     {
 105       d_uc.~UninterpretedConstant();
 106       break;
 107     }
 108     default: break;
 109   }
 110 }
 111
 112 Node EvalResult::toNode() const
 113 {
 114   NodeManager* nm = NodeManager::currentNM();
 115   switch (d_tag)
 116   {
 117     case EvalResult::BOOL: return nm->mkConst(d_bool);
 118     case EvalResult::BITVECTOR: return nm->mkConst(d_bv);
 119     case EvalResult::RATIONAL: return nm->mkConst(d_rat);
 120     case EvalResult::STRING: return nm->mkConst(d_str);
 121     case EvalResult::UCONST: return nm->mkConst(d_uc);
 122     default:
 123     {
 124       Trace("evaluator") << "Missing conversion from " << d_tag << " to node"
 125                          << std::endl;
 126       return Node();
 127     }
 128   }
 129 }
 130
 131 Node Evaluator::eval(TNode n,
 132                      const std::vector<Node>& args,
 133                      const std::vector<Node>& vals,
 134                      bool useRewriter) const
 135 {
 136   std::unordered_map<Node, Node, NodeHashFunction> visited;
 137   return eval(n, args, vals, visited, useRewriter);
 138 }
 139 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   Trace("evaluator") << "Evaluating " << n << " under substitution " << args
 147                      << " " << vals << " with visited size = " << visited.size()
 148                      << std::endl;
 149   std::unordered_map<TNode, Node, NodeHashFunction> evalAsNode;
 150   std::unordered_map<TNode, EvalResult, TNodeHashFunction> results;
 151   // add visited to results
 152   for (const std::pair<const Node, Node>& p : visited)
 153   {
 154     Trace("evaluator") << "Add " << p.first << " == " << p.second << std::endl;
 155     results[p.first] = evalInternal(p.second, args, vals, evalAsNode, results, useRewriter);
 156     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           evalAsNode.find(p.second);
 161       Assert(itn != evalAsNode.end());
 162       Node val = itn->second;
 163       if (useRewriter)
 164       {
 165         val = Rewriter::rewrite(val);
 166       }
 167       evalAsNode[p.first] = val;
 168     }
 169   }
 170   Trace("evaluator") << "Run eval internal..." << std::endl;
 171   Node ret = evalInternal(n, args, vals, evalAsNode, results, useRewriter).toNode();
 172   // if we failed to evaluate
 173   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         evalAsNode.find(n);
 178     Assert(itn != evalAsNode.end());
 179     ret = Rewriter::rewrite(itn->second);
 180   }
 181   // should be the same as substitution + rewriting, or possibly null if
 182   // useRewriter is false
 183   Assert((ret.isNull() && !useRewriter)
 184          || ret
 185                 == Rewriter::rewrite(n.substitute(
 186                        args.begin(), args.end(), vals.begin(), vals.end())));
 187   return ret;
 188 }
 189
 190 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   std::vector<TNode> queue;
 199   queue.emplace_back(n);
 200   std::unordered_map<TNode, EvalResult, TNodeHashFunction>::iterator itr;
 201
 202   while (queue.size() != 0)
 203   {
 204     TNode currNode = queue.back();
 205
 206     if (results.find(currNode) != results.end())
 207     {
 208       queue.pop_back();
 209       continue;
 210     }
 211
 212     bool doProcess = true;
 213     bool isVar = false;
 214     bool doEval = true;
 215     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       isVar = true;
 220       doEval = false;
 221     }
 222     else if (currNode.getMetaKind() == kind::metakind::PARAMETERIZED)
 223     {
 224       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       if (!op.isConst())
 228       {
 229         itr = results.find(op);
 230         if (itr == results.end())
 231         {
 232           queue.emplace_back(op);
 233           doProcess = false;
 234         }
 235         else if (itr->second.d_tag == EvalResult::INVALID)
 236         {
 237           doEval = false;
 238         }
 239       }
 240     }
 241     for (const auto& currNodeChild : currNode)
 242     {
 243       itr = results.find(currNodeChild);
 244       if (itr == results.end())
 245       {
 246         queue.emplace_back(currNodeChild);
 247         doProcess = false;
 248       }
 249       else if (itr->second.d_tag == EvalResult::INVALID)
 250       {
 251         // we cannot evaluate since there was an invalid child
 252         doEval = false;
 253       }
 254     }
 255     Trace("evaluator") << "Evaluator: visit " << currNode
 256                        << ", process = " << doProcess
 257                        << ", evaluate = " << doEval << std::endl;
 258
 259     if (doProcess)
 260     {
 261       queue.pop_back();
 262
 263       Node currNodeVal = currNode;
 264       // whether we need to reconstruct the current node in the case of failure
 265       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       if (!doEval)
 275       {
 276         if (isVar)
 277         {
 278           const auto& it = std::find(args.begin(), args.end(), currNode);
 279           if (it == args.end())
 280           {
 281             // variable with no substitution is itself
 282             evalAsNode[currNode] = currNode;
 283             results[currNode] = EvalResult();
 284             continue;
 285           }
 286           ptrdiff_t pos = std::distance(args.begin(), it);
 287           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           Trace("evaluator") << "Evaluator: collect arguments" << std::endl;
 296           currNodeVal = reconstruct(currNodeVal, results, evalAsNode);
 297           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             currNodeVal = Rewriter::rewrite(currNodeVal);
 302           }
 303         }
 304         needsReconstruct = false;
 305         Trace("evaluator") << "Evaluator: now after substitution + rewriting: "
 306                            << currNodeVal << std::endl;
 307         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           results[currNode] = EvalResult();
 313           evalAsNode[currNode] = currNodeVal;
 314           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       Trace("evaluator") << "Current node val : " << currNodeVal << std::endl;
 322
 323       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         case kind::CONST_BOOLEAN:
 385           results[currNode] = EvalResult(currNodeVal.getConst<bool>());
 386           break;
 387
 388         case kind::NOT:
 389         {
 390           results[currNode] = EvalResult(!(results[currNode[0]].d_bool));
 391           break;
 392         }
 393
 394         case kind::AND:
 395         {
 396           bool res = results[currNode[0]].d_bool;
 397           for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
 398           {
 399             res = res && results[currNode[i]].d_bool;
 400           }
 401           results[currNode] = EvalResult(res);
 402           break;
 403         }
 404
 405         case kind::OR:
 406         {
 407           bool res = results[currNode[0]].d_bool;
 408           for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
 409           {
 410             res = res || results[currNode[i]].d_bool;
 411           }
 412           results[currNode] = EvalResult(res);
 413           break;
 414         }
 415
 416         case kind::CONST_RATIONAL:
 417         {
 418           const Rational& r = currNodeVal.getConst<Rational>();
 419           results[currNode] = EvalResult(r);
 420           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         case kind::PLUS:
 430         {
 431           Rational res = results[currNode[0]].d_rat;
 432           for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
 433           {
 434             res = res + results[currNode[i]].d_rat;
 435           }
 436           results[currNode] = EvalResult(res);
 437           break;
 438         }
 439
 440         case kind::MINUS:
 441         {
 442           const Rational& x = results[currNode[0]].d_rat;
 443           const Rational& y = results[currNode[1]].d_rat;
 444           results[currNode] = EvalResult(x - y);
 445           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         case kind::MULT:
 455         case kind::NONLINEAR_MULT:
 456         {
 457           Rational res = results[currNode[0]].d_rat;
 458           for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
 459           {
 460             res = res * results[currNode[i]].d_rat;
 461           }
 462           results[currNode] = EvalResult(res);
 463           break;
 464         }
 465
 466         case kind::GEQ:
 467         {
 468           const Rational& x = results[currNode[0]].d_rat;
 469           const Rational& y = results[currNode[1]].d_rat;
 470           results[currNode] = EvalResult(x >= y);
 471           break;
 472         }
 473         case kind::LEQ:
 474         {
 475           const Rational& x = results[currNode[0]].d_rat;
 476           const Rational& y = results[currNode[1]].d_rat;
 477           results[currNode] = EvalResult(x <= y);
 478           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         case kind::CONST_STRING:
 501           results[currNode] = EvalResult(currNodeVal.getConst<String>());
 502           break;
 503
 504         case kind::STRING_CONCAT:
 505         {
 506           String res = results[currNode[0]].d_str;
 507           for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
 508           {
 509             res = res.concat(results[currNode[i]].d_str);
 510           }
 511           results[currNode] = EvalResult(res);
 512           break;
 513         }
 514
 515         case kind::STRING_LENGTH:
 516         {
 517           const String& s = results[currNode[0]].d_str;
 518           results[currNode] = EvalResult(Rational(s.size()));
 519           break;
 520         }
 521
 522         case kind::STRING_SUBSTR:
 523         {
 524           const String& s = results[currNode[0]].d_str;
 525           Integer s_len(s.size());
 526           Integer i = results[currNode[1]].d_rat.getNumerator();
 527           Integer j = results[currNode[2]].d_rat.getNumerator();
 528
 529           if (i.strictlyNegative() || j.strictlyNegative() || i >= s_len)
 530           {
 531             results[currNode] = EvalResult(String(""));
 532           }
 533           else if (i + j > s_len)
 534           {
 535             results[currNode] =
 536                 EvalResult(s.suffix((s_len - i).toUnsignedInt()));
 537           }
 538           else
 539           {
 540             results[currNode] =
 541                 EvalResult(s.substr(i.toUnsignedInt(), j.toUnsignedInt()));
 542           }
 543           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         case kind::STRING_STRCTN:
 580         {
 581           const String& s = results[currNode[0]].d_str;
 582           const String& t = results[currNode[1]].d_str;
 583           results[currNode] = EvalResult(s.find(t) != std::string::npos);
 584           break;
 585         }
 586
 587         case kind::STRING_STRIDOF:
 588         {
 589           const String& s = results[currNode[0]].d_str;
 590           Integer s_len(s.size());
 591           const String& x = results[currNode[1]].d_str;
 592           Integer i = results[currNode[2]].d_rat.getNumerator();
 593
 594           if (i.strictlyNegative())
 595           {
 596             results[currNode] = EvalResult(Rational(-1));
 597           }
 598           else
 599           {
 600             size_t r = s.find(x, i.toUnsignedInt());
 601             if (r == std::string::npos)
 602             {
 603               results[currNode] = EvalResult(Rational(-1));
 604             }
 605             else
 606             {
 607               results[currNode] = EvalResult(Rational(r));
 608             }
 609           }
 610           break;
 611         }
 612
 613         case kind::STRING_STRREPL:
 614         {
 615           const String& s = results[currNode[0]].d_str;
 616           const String& x = results[currNode[1]].d_str;
 617           const String& y = results[currNode[2]].d_str;
 618           results[currNode] = EvalResult(s.replace(x, y));
 619           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         case kind::STRING_ITOS:
 653         {
 654           Integer i = results[currNode[0]].d_rat.getNumerator();
 655           if (i.strictlyNegative())
 656           {
 657             results[currNode] = EvalResult(String(""));
 658           }
 659           else
 660           {
 661             results[currNode] = EvalResult(String(i.toString()));
 662           }
 663           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         case kind::STRING_TO_CODE:
 696         {
 697           const String& s = results[currNode[0]].d_str;
 698           if (s.size() == 1)
 699           {
 700             results[currNode] = EvalResult(Rational(s.getVec()[0]));
 701           }
 702           else
 703           {
 704             results[currNode] = EvalResult(Rational(-1));
 705           }
 706           break;
 707         }
 708
 709         case kind::CONST_BITVECTOR:
 710           results[currNode] = EvalResult(currNodeVal.getConst<BitVector>());
 711           break;
 712
 713         case kind::BITVECTOR_NOT:
 714           results[currNode] = EvalResult(~results[currNode[0]].d_bv);
 715           break;
 716
 717         case kind::BITVECTOR_NEG:
 718           results[currNode] = EvalResult(-results[currNode[0]].d_bv);
 719           break;
 720
 721         case kind::BITVECTOR_EXTRACT:
 722         {
 723           unsigned lo = bv::utils::getExtractLow(currNodeVal);
 724           unsigned hi = bv::utils::getExtractHigh(currNodeVal);
 725           results[currNode] =
 726               EvalResult(results[currNode[0]].d_bv.extract(hi, lo));
 727           break;
 728         }
 729
 730         case kind::BITVECTOR_CONCAT:
 731         {
 732           BitVector res = results[currNode[0]].d_bv;
 733           for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
 734           {
 735             res = res.concat(results[currNode[i]].d_bv);
 736           }
 737           results[currNode] = EvalResult(res);
 738           break;
 739         }
 740
 741         case kind::BITVECTOR_PLUS:
 742         {
 743           BitVector res = results[currNode[0]].d_bv;
 744           for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
 745           {
 746             res = res + results[currNode[i]].d_bv;
 747           }
 748           results[currNode] = EvalResult(res);
 749           break;
 750         }
 751
 752         case kind::BITVECTOR_MULT:
 753         {
 754           BitVector res = results[currNode[0]].d_bv;
 755           for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
 756           {
 757             res = res * results[currNode[i]].d_bv;
 758           }
 759           results[currNode] = EvalResult(res);
 760           break;
 761         }
 762         case kind::BITVECTOR_AND:
 763         {
 764           BitVector res = results[currNode[0]].d_bv;
 765           for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
 766           {
 767             res = res & results[currNode[i]].d_bv;
 768           }
 769           results[currNode] = EvalResult(res);
 770           break;
 771         }
 772
 773         case kind::BITVECTOR_OR:
 774         {
 775           BitVector res = results[currNode[0]].d_bv;
 776           for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
 777           {
 778             res = res | results[currNode[i]].d_bv;
 779           }
 780           results[currNode] = EvalResult(res);
 781           break;
 782         }
 783
 784         case kind::BITVECTOR_XOR:
 785         {
 786           BitVector res = results[currNode[0]].d_bv;
 787           for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
 788           {
 789             res = res ^ results[currNode[i]].d_bv;
 790           }
 791           results[currNode] = EvalResult(res);
 792           break;
 793         }
 794         case kind::BITVECTOR_UDIV:
 795         case kind::BITVECTOR_UDIV_TOTAL:
 796         {
 797           if (currNodeVal.getKind() == kind::BITVECTOR_UDIV_TOTAL
 798               || results[currNode[1]].d_bv.getValue() != 0)
 799           {
 800             BitVector res = results[currNode[0]].d_bv;
 801             res = res.unsignedDivTotal(results[currNode[1]].d_bv);
 802             results[currNode] = EvalResult(res);
 803           }
 804           else
 805           {
 806             results[currNode] = EvalResult();
 807             evalAsNode[currNode] =
 808                 needsReconstruct ? reconstruct(currNode, results, evalAsNode)
 809                                  : currNodeVal;
 810           }
 811           break;
 812         }
 813         case kind::BITVECTOR_UREM:
 814         case kind::BITVECTOR_UREM_TOTAL:
 815         {
 816           if (currNodeVal.getKind() == kind::BITVECTOR_UREM_TOTAL
 817               || results[currNode[1]].d_bv.getValue() != 0)
 818           {
 819             BitVector res = results[currNode[0]].d_bv;
 820             res = res.unsignedRemTotal(results[currNode[1]].d_bv);
 821             results[currNode] = EvalResult(res);
 822           }
 823           else
 824           {
 825             results[currNode] = EvalResult();
 826             evalAsNode[currNode] =
 827                 needsReconstruct ? reconstruct(currNode, results, evalAsNode)
 828                                  : currNodeVal;
 829           }
 830           break;
 831         }
 832
 833         case kind::EQUAL:
 834         {
 835           EvalResult lhs = results[currNode[0]];
 836           EvalResult rhs = results[currNode[1]];
 837
 838           switch (lhs.d_tag)
 839           {
 840             case EvalResult::BOOL:
 841             {
 842               results[currNode] = EvalResult(lhs.d_bool == rhs.d_bool);
 843               break;
 844             }
 845
 846             case EvalResult::BITVECTOR:
 847             {
 848               results[currNode] = EvalResult(lhs.d_bv == rhs.d_bv);
 849               break;
 850             }
 851
 852             case EvalResult::RATIONAL:
 853             {
 854               results[currNode] = EvalResult(lhs.d_rat == rhs.d_rat);
 855               break;
 856             }
 857
 858             case EvalResult::STRING:
 859             {
 860               results[currNode] = EvalResult(lhs.d_str == rhs.d_str);
 861               break;
 862             }
 863             case EvalResult::UCONST:
 864             {
 865               results[currNode] = EvalResult(lhs.d_uc == rhs.d_uc);
 866               break;
 867             }
 868
 869             default:
 870             {
 871               Trace("evaluator") << "Theory " << Theory::theoryOf(currNode[0])
 872                                  << " not supported" << std::endl;
 873               results[currNode] = EvalResult();
 874               evalAsNode[currNode] =
 875                   needsReconstruct ? reconstruct(currNode, results, evalAsNode)
 876                                    : currNodeVal;
 877               break;
 878             }
 879           }
 880
 881           break;
 882         }
 883
 884         case kind::ITE:
 885         {
 886           if (results[currNode[0]].d_bool)
 887           {
 888             results[currNode] = results[currNode[1]];
 889           }
 890           else
 891           {
 892             results[currNode] = results[currNode[2]];
 893           }
 894           break;
 895         }
 896
 897         default:
 898         {
 899           Trace("evaluator") << "Kind " << currNodeVal.getKind()
 900                              << " not supported" << std::endl;
 901           results[currNode] = EvalResult();
 902           evalAsNode[currNode] =
 903               needsReconstruct ? reconstruct(currNode, results, evalAsNode)
 904                                : currNodeVal;
 905         }
 906       }
 907     }
 908   }
 909
 910   return results[n];
 911 }
 912
 913 Node Evaluator::reconstruct(
 914     TNode n,
 915     std::unordered_map<TNode, EvalResult, TNodeHashFunction>& eresults,
 916     std::unordered_map<TNode, Node, NodeHashFunction>& evalAsNode) const
 917 {
 918   if (n.getNumChildren() == 0)
 919   {
 920     return n;
 921   }
 922   Trace("evaluator") << "Evaluator: reconstruct " << n << std::endl;
 923   NodeManager* nm = NodeManager::currentNM();
 924   std::unordered_map<TNode, EvalResult, TNodeHashFunction>::iterator itr;
 925   std::unordered_map<TNode, Node, NodeHashFunction>::iterator itn;
 926   std::vector<Node> echildren;
 927   if (n.getMetaKind() == kind::metakind::PARAMETERIZED)
 928   {
 929     TNode op = n.getOperator();
 930     if (op.isConst())
 931     {
 932       echildren.push_back(op);
 933     }
 934     else
 935     {
 936       itr = eresults.find(op);
 937       Assert(itr != eresults.end());
 938       if (itr->second.d_tag == EvalResult::INVALID)
 939       {
 940         // could not evaluate the operator, look in the node cache
 941         itn = evalAsNode.find(op);
 942         Assert(itn != evalAsNode.end());
 943         echildren.push_back(itn->second);
 944       }
 945       else
 946       {
 947         // otherwise, use the evaluation of the operator
 948         echildren.push_back(itr->second.toNode());
 949       }
 950     }
 951   }
 952   for (const auto& currNodeChild : n)
 953   {
 954     itr = eresults.find(currNodeChild);
 955     Assert(itr != eresults.end());
 956     if (itr->second.d_tag == EvalResult::INVALID)
 957     {
 958       // could not evaluate this child, look in the node cache
 959       itn = evalAsNode.find(currNodeChild);
 960       Assert(itn != evalAsNode.end());
 961       echildren.push_back(itn->second);
 962     }
 963     else
 964     {
 965       // otherwise, use the evaluation
 966       echildren.push_back(itr->second.toNode());
 967     }
 968   }
 969   // The value is the result of our (partially) successful evaluation
 970   // of the children.
 971   Node nn = nm->mkNode(n.getKind(), echildren);
 972   Trace("evaluator") << "Evaluator: reconstructed " << nn << std::endl;
 973   // Return node, without rewriting. Notice we do not need to substitute here
 974   // since all substitutions should already have been applied recursively.
 975   return nn;
 976 }
 977
 978 }  // namespace theory
 979 }  // namespace CVC4