From 2b44509b23e23e6dfb29899ccb55ee39de287b07 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 11 Mar 2022 12:03:09 -0600
Subject: [PATCH] Consider APPLY_CONSTRUCTOR applied to values to be a value
 (#8284)

Fixes cvc5/cvc5-projects#474.

Previously TheoryModel::isModelValue was incorrect for APPLY_CONSTRUCTOR.
---
 src/theory/theory_model.cpp                   |  6 ++++-
 src/theory/theory_model_builder.cpp           | 22 ++++++++-----------
 test/regress/CMakeLists.txt                   |  1 +
 .../proj-issue474-app-cons-value.smt2         | 16 ++++++++++++++
 4 files changed, 31 insertions(+), 14 deletions(-)
 create mode 100644 test/regress/regress0/datatypes/proj-issue474-app-cons-value.smt2

diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 54dbcdd3c..e9ecf16ac 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -849,7 +849,11 @@ bool TheoryModel::isValue(TNode n) const
     }
     if (!finishedComputing)
     {
-      bool hasOperator = cur.hasOperator();
+      // The only non-constant operators we consider are APPLY_UF and
+      // APPLY_SELECTOR. All other operators are either builtin, or should be
+      // considered constants, e.g. constructors.
+      Kind k = cur.getKind();
+      bool hasOperator = k == kind::APPLY_UF || k == kind::APPLY_SELECTOR;
       size_t nextChildIndex = v.second;
       if (hasOperator && nextChildIndex > 0)
       {
diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
index 6b61ea110..acef0e9b4 100644
--- a/src/theory/theory_model_builder.cpp
+++ b/src/theory/theory_model_builder.cpp
@@ -79,6 +79,9 @@ Node TheoryEngineModelBuilder::evaluateEqc(TheoryModel* m, TNode r)
     {
       Trace("model-builder-debug") << "...try to normalize" << std::endl;
       Node normalized = normalize(m, n, true);
+      Trace("model-builder-debug")
+          << "...return " << normalized
+          << ", isValue=" << m->isValue(normalized) << std::endl;
       if (m->isValue(normalized))
       {
         return normalized;
@@ -801,9 +804,10 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm)
             Assert(assertedReps.find(*i) != assertedReps.end());
             Node rep = assertedReps[*i];
             Node normalized = normalize(tm, rep, false);
-            Trace("model-builder") << "    Normalizing rep (" << rep
-                                   << "), normalized to (" << normalized << ")"
-                                   << endl;
+            Trace("model-builder")
+                << "    Normalizing rep (" << rep << "), normalized to ("
+                << normalized << ")"
+                << ", isValue=" << tm->isValue(normalized) << std::endl;
             if (tm->isValue(normalized))
             {
               changed = true;
@@ -1200,8 +1204,7 @@ Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, bool evalOnly)
     {
       children.push_back(r.getOperator());
     }
-    bool childrenConst = true;
-    for (size_t i = 0; i < r.getNumChildren(); ++i)
+    for (size_t i = 0, nchild = r.getNumChildren(); i < nchild; ++i)
     {
       Node ri = r[i];
       bool recurse = true;
@@ -1231,18 +1234,11 @@ Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, bool evalOnly)
         {
           ri = normalize(m, ri, evalOnly);
         }
-        if (!m->isValue(ri))
-        {
-          childrenConst = false;
-        }
       }
       children.push_back(ri);
     }
     retNode = NodeManager::currentNM()->mkNode(r.getKind(), children);
-    if (childrenConst)
-    {
-      retNode = rewrite(retNode);
-    }
+    retNode = rewrite(retNode);
   }
   d_normalizedCache[r] = retNode;
   return retNode;
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index d5cfc935e..31c056503 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -536,6 +536,7 @@ set(regress_0_tests
   regress0/datatypes/par-updater-type-rule.smt2 
   regress0/datatypes/parametric-alt-list.cvc.smt2
   regress0/datatypes/proj-issue172.smt2
+  regress0/datatypes/proj-issue474-app-cons-value.smt2
   regress0/datatypes/rec1.cvc.smt2
   regress0/datatypes/rec2.cvc.smt2
   regress0/datatypes/rec4.cvc.smt2
diff --git a/test/regress/regress0/datatypes/proj-issue474-app-cons-value.smt2 b/test/regress/regress0/datatypes/proj-issue474-app-cons-value.smt2
new file mode 100644
index 000000000..0bde05416
--- /dev/null
+++ b/test/regress/regress0/datatypes/proj-issue474-app-cons-value.smt2
@@ -0,0 +1,16 @@
+; COMMAND-LINE: -q
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+
+(declare-datatypes
+ ((Datatype 0))
+ (((constructor1 (selector1 Real))
+    (constructor2 (selector2 Real) (selector3 Real) (selector4 Bool) (selector5 Real)))))
+
+(assert
+ (= 0
+    (to_int
+     (selector1 (constructor2 (sin (ite false (arcsin 0.0) 1.0)) 0.0 false 0.0)))))
+
+(check-sat)
-- 
2.30.2