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