Fix collect model values for sequences of sequences (#5579)

Fixes #5543.

Recently we changed our model construction for sequences here: #5391.

This fix is not safe for sequences of sequences, where Valuation::getModelValue should not be called, since the argument of the seq.unit is not a shared term.

This makes our model construction for sequences more robust, however I'm not sure this is the end solution. In particular, it is still questionable whether we should call Valuation::getModelValue at all (consider sequences of theories whose model construction comes after strings), or for cases of (seq.unit x) where x is a sequence or string that does not have a concrete value. Regardless, this PR could be merged in the meantime since it should definitely fix some of the current issues.

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 72a4ae50d49ddbf82a2a902d1091a289f9b06fda..8ce8e0ecb97402be9871fcb604a5fd4d277d8fa6 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -337,8 +337,17 @@ bool TheoryStrings::collectModelInfoType(
           // is it an equivalence class with a seq.unit term?
           if (nfe.d_nf[0].getKind() == SEQ_UNIT)
           {
-            Node c = Rewriter::rewrite(nm->mkNode(
-                SEQ_UNIT, d_valuation.getModelValue(nfe.d_nf[0][0])));
+            Node argVal;
+            if (nfe.d_nf[0][0].getType().isStringLike())
+            {
+              argVal = d_state.getRepresentative(nfe.d_nf[0][0]);
+            }
+            else
+            {
+              // otherwise, it is a shared term
+              argVal = d_valuation.getModelValue(nfe.d_nf[0][0]);
+            }
+            Node c = Rewriter::rewrite(nm->mkNode(SEQ_UNIT, argVal));
             pure_eq_assign[eqc] = c;
             Trace("strings-model") << "(unit: " << nfe.d_nf[0] << ") ";
             m->getEqualityEngine()->addTerm(c);

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 9c596621174ae14ef66a0907b897f1a7d3acab80..689b575144fe76cef4f97a06b289d784168271a3 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -900,6 +900,7 @@ set(regress_0_tests
   regress0/seq/intseq.smt2
   regress0/seq/intseq_dt.smt2
   regress0/seq/issue4370-bool-terms.smt2
+  regress0/seq/issue5543-unit-cmv.smt2
   regress0/seq/seq-2var.smt2
   regress0/seq/seq-ex1.smt2
   regress0/seq/seq-ex2.smt2

diff --git a/test/regress/regress0/seq/issue5543-unit-cmv.smt2 b/test/regress/regress0/seq/issue5543-unit-cmv.smt2
new file mode 100644 (file)
index 0000000..8a9a2d4
--- /dev/null
+++ b/test/regress/regress0/seq/issue5543-unit-cmv.smt2
@@ -0,0 +1,12 @@
+; COMMAND-LINE: --strings-exp
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun a () (Seq (Seq Int)))
+(declare-fun b () (Seq (Seq Int)))
+(declare-fun c () (Seq (Seq Int)))
+(declare-fun d () (Seq (Seq Int)))
+(declare-fun e () (Seq Int))
+(declare-fun f () (Seq Int))
+(assert (distinct a (seq.++ (seq.unit e) b)))
+(assert (= (seq.++ (seq.unit f) d) a c))
+(check-sat)