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.

diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
index f711dfdd17f06cd2f7f4e7b7c3a4e293649a4aa8..34659031edfaa751c26a360078c064c36c5b221c 100644 (file)
--- 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 a604d04025aa8b4f85ae560dd2cecd3164f2b3de..fb6204b69001b82c4498216fe06389b2b92c943a 100644 (file)
--- 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 13434f8298de800e679f0e4b7644d2e32037240c..a61b9df199315a7043023997f73615a3215cae3d 100644 (file)
--- 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 (file)
index 0000000..e0ed3ea
--- /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)