diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-12-16 00:22:40 -0600 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-12-15 22:22:40 -0800 |
| commit | 0e5efa8c4ff22925d3fc011a3588a3e67c107d0e (patch) | |
| tree | 88ed490687dc49432dc0919eaa6043a64444bfdd | |
| parent | 52b216f385c0b1c1a9bb0ab8541683d9e13a7f46 (diff) | |
Minor improvement to evaluator (#3570)
Fixes a bug where we don't return the partially evaluated version (for unevaluatable nodes). Also adds `NONLINEAR_MULT` whose semantics is identical to `MULT`.
| -rw-r--r-- | src/theory/evaluator.cpp | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp index ae573956f..67ac255ee 100644 --- a/src/theory/evaluator.cpp +++ b/src/theory/evaluator.cpp @@ -122,7 +122,8 @@ Node Evaluator::eval(TNode n, << " " << vals << std::endl; std::unordered_map<TNode, Node, NodeHashFunction> evalAsNode; Node ret = evalInternal(n, args, vals, evalAsNode).toNode(); - if (!ret.isNull()) + // 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 = @@ -357,6 +358,7 @@ EvalResult Evaluator::evalInternal( break; } case kind::MULT: + case kind::NONLINEAR_MULT: { Rational res = results[currNode[0]].d_rat; for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++) |