From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 16 Dec 2019 06:22:40 +0000 (-0600)
Subject: Minor improvement to evaluator (#3570)
X-Git-Tag: cvc5-1.0.0~3763
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0e5efa8c4ff22925d3fc011a3588a3e67c107d0e;p=cvc5.git

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 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++)