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`.

diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp
index ae573956fd3a7938d59b856f525ec08c62185590..67ac255ee8314843f57610d1b7d844889149a030 100644 (file)
--- 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++)