summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2019-12-16 10:28:51 -0600
committerGitHub <noreply@github.com>2019-12-16 10:28:51 -0600
commit5ee3c8d02e21b1c20bfe56538c4cbe4fed0481eb (patch)
tree6e0b4271e6583e5e8be6bcd1320c4db56d8f992f /src
parentc1c8b61a03732cb485e358bc0f78e654242d58de (diff)
Revert evaluate as node. (#3574)
Diffstat (limited to 'src')
-rw-r--r--src/theory/evaluator.cpp14
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(
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback