Add constants from equality engine evaluation to model

Fixes #5330. The issue mentions to related model checking failures:

- When the theory of strings computes a model, there is a step that
  chooses a constant that is different from other constants of the same
  length in other equivalence classes. In the example, the issue was
  that the constant `"A"` was introduced by doing evaluation in the
  equality engine of the theory of strings. The constant was then not
  added to the term set and was skipped while asserting the equality
  engine to the theory model. As a result, an equivalence class was
  assigned `"A"` even though it already existed, which made the model
  invalid. The fix ensures that all constants in the equality engine are
  added to the theory model. It should be ok to handle the issue during
  model construction because other theories shouldn't have to care about
  the constants that we computed internally within the theory of
  strings.
- When an equivalence class has a normal form that consists of a single
  `seq.unit`, then we need to make sure that the value for the argument
  is consistent with the rest of the model and we have to make sure that
  we choose different values for different equivalence classes. The
  commit adds code for retrieving the value of the argument to
  `seq.unit` from the model and adds the resulting constant to the
  theory model to block it for other equivalence classes. Previously,
  this was not done and we ended up with two different equivalence
  classes being assigned the same constant.

Signed-off-by: Andres Noetzli <noetzli@amazon.com>

4 files changed, 28 insertions, 1 deletions

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 1dc19deb1..a9e2c0051 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -337,8 +337,11 @@ bool TheoryStrings::collectModelInfoType(
           // is it an equivalence class with a seq.unit term?
           if (nfe.d_nf[0].getKind() == SEQ_UNIT)
           {
-            pure_eq_assign[eqc] = nfe.d_nf[0];
+            Node c = Rewriter::rewrite(nm->mkNode(
+                SEQ_UNIT, d_valuation.getModelValue(nfe.d_nf[0][0])));
+            pure_eq_assign[eqc] = c;
             Trace("strings-model") << "(unit: " << nfe.d_nf[0] << ") ";
+            m->getEqualityEngine()->addTerm(c);
           }
           // does it have a code and the length of these equivalence classes are
           // one?
@@ -366,6 +369,12 @@ bool TheoryStrings::collectModelInfoType(
       else
       {
         processed[eqc] = eqc;
+        // Make sure that constants are asserted to the theory model that we
+        // are building. It is possible that new constants were introduced by
+        // the eager evaluation in the equality engine. These terms are missing
+        // in the term set and, as a result, are skipped when the equality
+        // engine is asserted to the theory model.
+        m->getEqualityEngine()->addTerm(eqc);
       }
     }
     Trace("strings-model") << "have length " << lts_values[i] << std::endl;
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 3bce17525..334901c7a 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1845,6 +1845,8 @@ set(regress_1_tests
   regress1/strings/issue4735.smt2
   regress1/strings/issue4735_2.smt2
   regress1/strings/issue4759-comp-delta.smt2
+  regress1/strings/issue5330.smt2
+  regress1/strings/issue5330_2.smt2
   regress1/strings/issue5374-proxy-i.smt2
   regress1/strings/kaluza-fl.smt2
   regress1/strings/loop002.smt2
diff --git a/test/regress/regress1/strings/issue5330.smt2 b/test/regress/regress1/strings/issue5330.smt2
new file mode 100644
index 000000000..aa0db8591
--- /dev/null
+++ b/test/regress/regress1/strings/issue5330.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --strings-exp
+; EXPECT: sat
+(set-logic QF_SLIA)
+(declare-fun str1 () String)
+(declare-fun str18 () String)
+(assert (str.in_re (str.replace str18 str1 str18) (str.to_re "pANjvthXNyBbIgIlkC")))
+(check-sat)
diff --git a/test/regress/regress1/strings/issue5330_2.smt2 b/test/regress/regress1/strings/issue5330_2.smt2
new file mode 100644
index 000000000..f67a95335
--- /dev/null
+++ b/test/regress/regress1/strings/issue5330_2.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --strings-exp
+; EXPECT: sat
+(set-logic QF_SLIA)
+(declare-fun seq11 () (Seq Int))
+(declare-fun i5 () Int)
+(declare-fun v17 () Bool)
+(declare-fun v24 () Bool)
+(assert (xor v17 v24 true true (seq.prefixof (seq.rev (seq.rev seq11)) (seq.unit i5))))
+(check-sat)