Minor refactoring of compute model value for nl (#3489)

* Refactor compute model value for nl

* Format

1 files changed, 22 insertions, 29 deletions

diff --git a/src/theory/arith/nl_model.cpp b/src/theory/arith/nl_model.cpp
index 62bdf310b..762e8b141 100644
--- a/src/theory/arith/nl_model.cpp
+++ b/src/theory/arith/nl_model.cpp
@@ -73,31 +73,22 @@ Node NlModel::computeModelValue(Node n, bool isConcrete)
   Trace("nl-ext-mv-debug") << "computeModelValue " << n << ", index=" << index
                            << std::endl;
   Node ret;
+  Kind nk = n.getKind();
   if (n.isConst())
   {
     ret = n;
   }
-  else if (index == 1
-           && (n.getKind() == NONLINEAR_MULT
-               || isTranscendentalKind(n.getKind())))
+  else if (!isConcrete && hasTerm(n))
   {
-    if (hasTerm(n))
-    {
-      // use model value for abstraction
-      ret = getRepresentative(n);
-    }
-    else
-    {
-      // abstraction does not exist, use model value
-      ret = getValueInternal(n);
-    }
+    // use model value for abstraction
+    ret = getRepresentative(n);
   }
   else if (n.getNumChildren() == 0)
   {
-    if (n.getKind() == PI)
+    // we are interested in the exact value of PI, which cannot be computed.
+    // hence, we return PI itself when asked for the concrete value.
+    if (nk == PI)
     {
-      // we are interested in the exact value of PI, which cannot be computed.
-      // hence, we return PI itself when asked for the concrete value.
       ret = n;
     }
     else
@@ -108,23 +99,25 @@ Node NlModel::computeModelValue(Node n, bool isConcrete)
   else
   {
     // otherwise, compute true value
-    std::vector<Node> children;
-    if (n.getMetaKind() == metakind::PARAMETERIZED)
-    {
-      children.push_back(n.getOperator());
-    }
-    for (unsigned i = 0; i < n.getNumChildren(); i++)
+    TheoryId ctid = theory::kindToTheoryId(nk);
+    if (ctid != THEORY_ARITH && ctid != THEORY_BOOL && ctid != THEORY_BUILTIN)
     {
-      Node mc = computeModelValue(n[i], isConcrete);
-      children.push_back(mc);
-    }
-    ret = NodeManager::currentNM()->mkNode(n.getKind(), children);
-    if (n.getKind() == APPLY_UF)
-    {
-      ret = getValueInternal(ret);
+      // we directly look up terms not belonging to arithmetic
+      ret = getValueInternal(n);
     }
     else
     {
+      std::vector<Node> children;
+      if (n.getMetaKind() == metakind::PARAMETERIZED)
+      {
+        children.push_back(n.getOperator());
+      }
+      for (unsigned i = 0, nchild = n.getNumChildren(); i < nchild; i++)
+      {
+        Node mc = computeModelValue(n[i], isConcrete);
+        children.push_back(mc);
+      }
+      ret = NodeManager::currentNM()->mkNode(nk, children);
       ret = Rewriter::rewrite(ret);
     }
   }