From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 8 Dec 2020 04:46:22 +0000 (-0600)
Subject: Fix collect model values for sequences of sequences (#5579)
X-Git-Tag: cvc5-1.0.0~2484
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3223d3c765b87db9d87a7ca65c4b7cf5dc9a7885;p=cvc5.git

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 72a4ae50d..8ce8e0ecb 100644
--- 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 9c5966211..689b57514 100644
--- 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
index 000000000..8a9a2d416
--- /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)