From 5ee3c8d02e21b1c20bfe56538c4cbe4fed0481eb Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 16 Dec 2019 10:28:51 -0600 Subject: Revert evaluate as node. (#3574) --- src/theory/evaluator.cpp | 14 +------------- 1 file changed, 1 insertion(+), 13 deletions(-) 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 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::iterator itn = - evalAsNode.find(n); - if (itn != evalAsNode.end()) - { - return itn->second; - } - } - return ret; + return evalInternal(n, args, vals, evalAsNode).toNode(); } EvalResult Evaluator::evalInternal( -- cgit v1.2.3