From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 16 Dec 2019 16:28:51 +0000 (-0600)
Subject: Revert evaluate as node. (#3574)
X-Git-Tag: cvc5-1.0.0~3761
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5ee3c8d02e21b1c20bfe56538c4cbe4fed0481eb;p=cvc5.git

Revert evaluate as node. (#3574)
---

diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp
index 67ac255ee..406fb5ead 100644
--- a/src/theory/evaluator.cpp
+++ b/src/theory/evaluator.cpp
@@ -121,19 +121,7 @@ Node Evaluator::eval(TNode n,
   Trace("evaluator") << "Evaluating " << n << " under substitution " << args
                      << " " << vals << std::endl;
   std::unordered_map<TNode, Node, NodeHashFunction> evalAsNode;
-  Node ret = evalInternal(n, args, vals, evalAsNode).toNode();
-  // if we failed to evaluate
-  if (ret.isNull())
-  {
-    // maybe it was stored in the evaluation-as-node map
-    std::unordered_map<TNode, Node, NodeHashFunction>::iterator itn =
-        evalAsNode.find(n);
-    if (itn != evalAsNode.end())
-    {
-      return itn->second;
-    }
-  }
-  return ret;
+  return evalInternal(n, args, vals, evalAsNode).toNode();
 }
 
 EvalResult Evaluator::evalInternal(