Fix exclusion criteria for codatatype model values (#7546)

This fixes codatatype model value construction.

Model construction for codatatypes is non-standard since it requires analyzing whether (possibly recursively defined) terms are alpha equivalent to others during model construction. This is currently handled as a special case within the theory model builder. (This should eventually be moved somewhere more appropriate via a new callback to theory).

This fixes the criteria which was too permissive about which values can be used in models. We now exclude values that match the skeleton of representative codatatype terms. Previously we additionally required that the terms were bisimilar.

Fixes #4851.

4 files changed, 47 insertions, 35 deletions

diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
index f711dfdd1..34659031e 100644
--- a/src/theory/theory_model_builder.cpp
+++ b/src/theory/theory_model_builder.cpp
@@ -218,62 +218,62 @@ bool TheoryEngineModelBuilder::isExcludedCdtValue(
     Assert(assertedReps.find(*i) != assertedReps.end());
     Node rep = assertedReps[*i];
     Trace("model-builder-debug") << "  Rep : " << rep << std::endl;
-    // check matching val to rep with eqc as a free variable
-    Node eqc_m;
-    if (isCdtValueMatch(val, rep, eqc, eqc_m))
+    // check whether it is possible that rep will be assigned the same value
+    // as val.
+    if (isCdtValueMatch(val, rep))
     {
-      Trace("model-builder-debug") << "  ...matches with " << eqc << " -> "
-                                   << eqc_m << std::endl;
-      if (eqc_m.getKind() == kind::CODATATYPE_BOUND_VARIABLE)
-      {
-        Trace("model-builder-debug") << "*** " << val
-                                     << " is excluded datatype for " << eqc
-                                     << std::endl;
-        return true;
-      }
+      return true;
     }
   }
   return false;
 }
 
-bool TheoryEngineModelBuilder::isCdtValueMatch(Node v,
-                                               Node r,
-                                               Node eqc,
-                                               Node& eqc_m)
+bool TheoryEngineModelBuilder::isCdtValueMatch(Node v, Node r)
 {
   if (r == v)
   {
+    // values equal match trivially
     return true;
   }
-  else if (r == eqc)
+  else if (v.isConst() && r.isConst())
   {
-    if (eqc_m.isNull())
+    // distinct constant values do not match
+    return false;
+  }
+  else if (r.getKind() == kind::APPLY_CONSTRUCTOR)
+  {
+    if (v.getKind() != kind::APPLY_CONSTRUCTOR)
     {
-      // only if an uninterpreted constant?
-      eqc_m = v;
+      Assert(v.getKind() == kind::CODATATYPE_BOUND_VARIABLE);
+      // v is the position of a loop. It may be possible to match, we return
+      // true, which is an over-approximation of when it is unsafe to use v.
       return true;
     }
-    else
-    {
-      return v == eqc_m;
-    }
-  }
-  else if (v.getKind() == kind::APPLY_CONSTRUCTOR
-           && r.getKind() == kind::APPLY_CONSTRUCTOR)
-  {
     if (v.getOperator() == r.getOperator())
     {
-      for (unsigned i = 0; i < v.getNumChildren(); i++)
+      for (size_t i = 0, nchild = v.getNumChildren(); i < nchild; i++)
       {
-        if (!isCdtValueMatch(v[i], r[i], eqc, eqc_m))
+        if (!isCdtValueMatch(v[i], r[i]))
         {
+          // if one child fails to match, we cannot match
           return false;
         }
       }
       return true;
     }
+    // operators do not match
+    return false;
   }
-  return false;
+  else if (v.getKind() == kind::APPLY_CONSTRUCTOR)
+  {
+    // v has a constructor in a position that we have yet to fill in r.
+    // we are either a finite type in which case this subfield of r can be
+    // assigned a default value (or otherwise would have been split on).
+    // otherwise we are an infinite type and the subfield of r will be
+    // chosen not to clash with the subfield of v.
+    return false;
+  }
+  return true;
 }
 
 bool TheoryEngineModelBuilder::involvesUSort(TypeNode tn) const
diff --git a/src/theory/theory_model_builder.h b/src/theory/theory_model_builder.h
index a604d0402..fb6204b69 100644
--- a/src/theory/theory_model_builder.h
+++ b/src/theory/theory_model_builder.h
@@ -292,11 +292,14 @@ class TheoryEngineModelBuilder : protected EnvObj
                           Node eqc);
   /** is codatatype value match
    *
-   * This returns true if v is r{ eqc -> t } for some t.
-   * If this function returns true, then t above is
-   * stored in eqc_m.
+   * Takes as arguments a codatatype value v, and a codatatype term r of the
+   * same sort.
+   *
+   * It returns true if it is possible that the value of r will be forced to
+   * be equal to v during model construction. A return value of false indicates
+   * that it is safe to use value v to avoid merging with r.
    */
-  bool isCdtValueMatch(Node v, Node r, Node eqc, Node& eqc_m);
+  static bool isCdtValueMatch(Node v, Node r);
   //------------------------------------end for codatatypes
 
   //---------------------------------for debugging finite model finding
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 13434f829..a61b9df19 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1639,6 +1639,7 @@ set(regress_1_tests
   regress1/datatypes/dt-color-2.6.smt2
   regress1/datatypes/dt-param-card4-unsat.smt2
   regress1/datatypes/issue3266-small.smt2
+  regress1/datatypes/issue4851-cdt-model.smt2
   regress1/datatypes/issue-variant-dt-zero.smt2
   regress1/datatypes/manos-model.smt2
   regress1/datatypes/non-simple-rec.smt2
diff --git a/test/regress/regress1/datatypes/issue4851-cdt-model.smt2 b/test/regress/regress1/datatypes/issue4851-cdt-model.smt2
new file mode 100644
index 000000000..e0ed3ea9f
--- /dev/null
+++ b/test/regress/regress1/datatypes/issue4851-cdt-model.smt2
@@ -0,0 +1,8 @@
+(set-logic ALL)
+(set-info :status sat)
+(declare-codatatypes ((a 0)) (((b (c Int) (d a)))))
+(declare-fun e () a)
+(declare-fun f () a)
+(assert (distinct f (b 0 f)))
+(assert (= e f))
+(check-sat)