diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-12-16 10:28:51 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-12-16 10:28:51 -0600 |
commit | 5ee3c8d02e21b1c20bfe56538c4cbe4fed0481eb (patch) | |
tree | 6e0b4271e6583e5e8be6bcd1320c4db56d8f992f | |
parent | c1c8b61a03732cb485e358bc0f78e654242d58de (diff) |
Revert evaluate as node. (#3574)
-rw-r--r-- | src/theory/evaluator.cpp | 14 |
1 files changed, 1 insertions, 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<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( |