Make model builder robust to multiple value-like terms in the same equivalence class...

This changes our policy on handling when two value-like terms are in the same equivalence class. We now give preference to the "base" model value, and either warn or throw a debug exception.

After f7675b2, we can have the situation where e.g. (seq.nth seq.empty 1) is in the same equivalence class as a constant, where (seq.nth seq.empty 1) is considered value-like, despite being unevaluatable. We now ensure that the constant is taken as the representative of the equivalence class, and not this term.

It also removes assignable terms from consideration when assigning values to equivalence classes. In particular, (seq.nth seq.empty 1) is skipped, so a warning is not even given when the above occurs.

Fixes #8148.

diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
index 03cdaa7868285c5e2edad48cfd83233bb614e9a9..fc1d5ee9ed4d242d856f950ffb3fef57311e4643 100644 (file)
--- a/src/theory/theory_model_builder.cpp
+++ b/src/theory/theory_model_builder.cpp
@@ -458,6 +458,8 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm)
 
     // The assigned represenative and constant representative
     Node rep, constRep;
+    // is constant rep a "base model value" (see TheoryModel::isBaseModelValue)
+    bool constRepBaseModelValue = false;
     // A flag set to true if the current equivalence class is assignable (see
     // assignableEqc).
     bool assignable = false;
@@ -499,38 +501,69 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm)
       // model-specific processing of the term
       tm->addTermInternal(n);
 
-      // (2) Record constant representative or assign representative, if
-      // applicable. We check if n is a value here, e.g. a term for which
-      // isConst returns true, or a lambda. The latter is required only for
-      // higher-order.
-      if (tm->isValue(n))
+      // compute whether n is assignable
+      if (!isAssignable(n))
       {
-        Assert(constRep.isNull());
-        constRep = n;
-        Trace("model-builder")
-            << "    ..ConstRep( " << eqc << " ) = " << constRep << std::endl;
-        // if we have a constant representative, nothing else matters
-        continue;
-      }
+        // (2) Record constant representative or assign representative, if
+        // applicable. We check if n is a value here, e.g. a term for which
+        // isConst returns true, or a lambda. The latter is required only for
+        // higher-order.
+        if (tm->isValue(n))
+        {
+          // In rare cases, it could be that multiple terms in the same
+          // equivalence class are considered values. We prefer the one that is
+          // a "base" model value (e.g. a constant) here. We throw a warning
+          // if there are 2 model values in the same equivalence class, and
+          // a debug failure if there are 2 base values in the same equivalence
+          // class.
+          bool assignConstRep = false;
+          bool isBaseValue = tm->isBaseModelValue(n);
+          if (constRep.isNull())
+          {
+            assignConstRep = true;
+          }
+          else
+          {
+            warning() << "Model values in the same equivalence class "
+                      << constRep << " " << n << std::endl;
+            if (!constRepBaseModelValue)
+            {
+              assignConstRep = isBaseValue;
+            }
+            else if (isBaseValue)
+            {
+              Assert(false)
+                  << "Base model values in the same equivalence class "
+                  << constRep << " " << n << std::endl;
+            }
+          }
+          if (assignConstRep)
+          {
+            constRep = n;
+            Trace("model-builder") << "    ..ConstRep( " << eqc
+                                   << " ) = " << constRep << std::endl;
+            constRepBaseModelValue = isBaseValue;
+          }
+          // if we have a constant representative, nothing else matters
+          continue;
+        }
 
-      // If we don't have a constant rep, check if this is an assigned rep.
-      itm = tm->d_reps.find(n);
-      if (itm != tm->d_reps.end())
-      {
-        // Notice that this equivalence class may contain multiple terms that
-        // were specified as being a representative, since e.g. datatypes may
-        // assert representative for two constructor terms that are not in the
-        // care graph and are merged during collectModeInfo due to equality
-        // information from another theory. We overwrite the value of rep in
-        // these cases here.
-        rep = itm->second;
-        Trace("model-builder")
-            << "    ..Rep( " << eqc << " ) = " << rep << std::endl;
-      }
+        // If we don't have a constant rep, check if this is an assigned rep.
+        itm = tm->d_reps.find(n);
+        if (itm != tm->d_reps.end())
+        {
+          // Notice that this equivalence class may contain multiple terms that
+          // were specified as being a representative, since e.g. datatypes may
+          // assert representative for two constructor terms that are not in the
+          // care graph and are merged during collectModeInfo due to equality
+          // information from another theory. We overwrite the value of rep in
+          // these cases here.
+          rep = itm->second;
+          Trace("model-builder")
+              << "    ..Rep( " << eqc << " ) = " << rep << std::endl;
+        }
 
-      // (3) Finally, process assignable information
-      if (!isAssignable(n))
-      {
+        // (3) Finally, process assignable information
         evaluable = true;
         // expressions that are not assignable should not be given assignment
         // exclusion sets

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 5f299152fec9f9ab9dfa2573154a9315f6e564bf..b28651d95314dee6ef0e6ef3bc4dbe63deb9ecc0 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2265,6 +2265,8 @@ set(regress_1_tests
   regress1/sep/wand-simp-sat.smt2
   regress1/sep/wand-simp-sat2.smt2
   regress1/sep/wand-simp-unsat.smt2
+  regress1/seq/issue8148-2-const-mv.smt2
+  regress1/seq/issue8148-const-mv.smt2
   regress1/sets/choose.cvc.smt2
   regress1/sets/choose1.smt2
   regress1/sets/choose2.smt2

diff --git a/test/regress/regress1/seq/issue8148-2-const-mv.smt2 b/test/regress/regress1/seq/issue8148-2-const-mv.smt2
new file mode 100644 (file)
index 0000000..7ef7f93
--- /dev/null
+++ b/test/regress/regress1/seq/issue8148-2-const-mv.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: --strings-exp -q
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(assert (forall ((V Int)) (= 0 (seq.nth (seq.unit 0) 1))))
+(check-sat)

diff --git a/test/regress/regress1/seq/issue8148-const-mv.smt2 b/test/regress/regress1/seq/issue8148-const-mv.smt2
new file mode 100644 (file)
index 0000000..01f7aef
--- /dev/null
+++ b/test/regress/regress1/seq/issue8148-const-mv.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --strings-exp -q
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(set-option :re-elim-agg true)
+(declare-fun e!0 () (Seq Bool))
+(assert (= e!0 seq.empty))
+(assert (seq.nth e!0 0))
+(check-sat)