Add constants from equality engine evaluation to model (#5391)

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.

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 1dc19deb137c924e2b67a5f8a31ab12bdb5da05a..a9e2c00512a8e5d40690630e8a720b2df5ca0ffd 100644 (file)
--- 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 3bce17525f329154a6798530557cd1309b06951f..334901c7ab26bfcf3589ddab75d8947a613a750b 100644 (file)
--- 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 (file)
index 0000000..aa0db85
--- /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 (file)
index 0000000..f67a953
--- /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)