Fix model construction for str.unit (#8917)

Fixes #8915.

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index f371516b62ed4fc6cedd88a72a84be79e7b138a2..e015e108437d68897c9ccdd321794488278e030b 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -452,8 +452,18 @@ bool TheoryStrings::collectModelInfoType(
       }
       // is it an equivalence class with a seq.unit term?
       Node assignedValue;
-      if (nfe.d_nf[0].getKind() == SEQ_UNIT
-          || nfe.d_nf[0].getKind() == STRING_UNIT)
+      if (nfe.d_nf[0].getKind() == STRING_UNIT)
+      {
+        // str.unit is applied to integers, where we are guaranteed the model
+        // exists. We preempitively get the model value here, so that we
+        // avoid repeated model values for strings.
+        Node val = d_valuation.getModelValue(nfe.d_nf[0][0]);
+        assignedValue = utils::mkUnit(eqc.getType(), val);
+        assignedValue = rewrite(assignedValue);
+        Trace("strings-model")
+            << "-> assign via str.unit: " << assignedValue << std::endl;
+      }
+      else if (nfe.d_nf[0].getKind() == SEQ_UNIT)
       {
         if (nfe.d_nf[0][0].getType().isStringLike())
         {

diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index 0697ccb53129eb3470515f2761d6a19a82175399..13f2778411dc46716e55445db43bc35401e354a4 100644 (file)
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -2637,6 +2637,7 @@ set(regress_1_tests
   regress1/strings/issue8434-nterm-str-rw.smt2
   regress1/strings/issue8890-inj-oob.smt2
   regress1/strings/issue8906-oob-exp.smt2
+  regress1/strings/issue8915-str-unit-model.smt2
   regress1/strings/kaluza-fl.smt2
   regress1/strings/loop002.smt2
   regress1/strings/loop003.smt2

diff --git a/test/regress/cli/regress1/strings/issue8915-str-unit-model.smt2 b/test/regress/cli/regress1/strings/issue8915-str-unit-model.smt2
new file mode 100644 (file)
index 0000000..75b468e
--- /dev/null
+++ b/test/regress/cli/regress1/strings/issue8915-str-unit-model.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --strings-exp
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun a () String)
+(declare-fun e () String)
+(declare-fun v () String)
+(assert (exists ((E String)) (and (distinct v e) (distinct e a) (distinct v "A") (> (str.to_code a) 65))))
+(check-sat)