From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 29 Jun 2022 20:19:41 +0000 (-0500)
Subject: Fix model construction for str.unit (#8917)
X-Git-Tag: cvc5-1.0.1~28
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4bc7135f78792a09654b001ce738b23c39448ff6;p=cvc5.git

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 f371516b6..e015e1084 100644
--- 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 0697ccb53..13f277841 100644
--- 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
index 000000000..75b468e39
--- /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)