From aec1f43a8fbedf13fe6906d6be93060d5180f2f3 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Fri, 23 Oct 2020 10:32:54 -0700 Subject: 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 --- src/theory/strings/theory_strings.cpp | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) (limited to 'src') 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; -- cgit v1.2.3