From 3223d3c765b87db9d87a7ca65c4b7cf5dc9a7885 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 7 Dec 2020 22:46:22 -0600 Subject: [PATCH] Fix collect model values for sequences of sequences (#5579) Fixes #5543. Recently we changed our model construction for sequences here: #5391. This fix is not safe for sequences of sequences, where Valuation::getModelValue should not be called, since the argument of the seq.unit is not a shared term. This makes our model construction for sequences more robust, however I'm not sure this is the end solution. In particular, it is still questionable whether we should call Valuation::getModelValue at all (consider sequences of theories whose model construction comes after strings), or for cases of (seq.unit x) where x is a sequence or string that does not have a concrete value. Regardless, this PR could be merged in the meantime since it should definitely fix some of the current issues. --- src/theory/strings/theory_strings.cpp | 13 +++++++++++-- test/regress/CMakeLists.txt | 1 + test/regress/regress0/seq/issue5543-unit-cmv.smt2 | 12 ++++++++++++ 3 files changed, 24 insertions(+), 2 deletions(-) create mode 100644 test/regress/regress0/seq/issue5543-unit-cmv.smt2 diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 72a4ae50d..8ce8e0ecb 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -337,8 +337,17 @@ bool TheoryStrings::collectModelInfoType( // is it an equivalence class with a seq.unit term? if (nfe.d_nf[0].getKind() == SEQ_UNIT) { - Node c = Rewriter::rewrite(nm->mkNode( - SEQ_UNIT, d_valuation.getModelValue(nfe.d_nf[0][0]))); + Node argVal; + if (nfe.d_nf[0][0].getType().isStringLike()) + { + argVal = d_state.getRepresentative(nfe.d_nf[0][0]); + } + else + { + // otherwise, it is a shared term + argVal = d_valuation.getModelValue(nfe.d_nf[0][0]); + } + Node c = Rewriter::rewrite(nm->mkNode(SEQ_UNIT, argVal)); pure_eq_assign[eqc] = c; Trace("strings-model") << "(unit: " << nfe.d_nf[0] << ") "; m->getEqualityEngine()->addTerm(c); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 9c5966211..689b57514 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -900,6 +900,7 @@ set(regress_0_tests regress0/seq/intseq.smt2 regress0/seq/intseq_dt.smt2 regress0/seq/issue4370-bool-terms.smt2 + regress0/seq/issue5543-unit-cmv.smt2 regress0/seq/seq-2var.smt2 regress0/seq/seq-ex1.smt2 regress0/seq/seq-ex2.smt2 diff --git a/test/regress/regress0/seq/issue5543-unit-cmv.smt2 b/test/regress/regress0/seq/issue5543-unit-cmv.smt2 new file mode 100644 index 000000000..8a9a2d416 --- /dev/null +++ b/test/regress/regress0/seq/issue5543-unit-cmv.smt2 @@ -0,0 +1,12 @@ +; COMMAND-LINE: --strings-exp +; EXPECT: sat +(set-logic ALL) +(declare-fun a () (Seq (Seq Int))) +(declare-fun b () (Seq (Seq Int))) +(declare-fun c () (Seq (Seq Int))) +(declare-fun d () (Seq (Seq Int))) +(declare-fun e () (Seq Int)) +(declare-fun f () (Seq Int)) +(assert (distinct a (seq.++ (seq.unit e) b))) +(assert (= (seq.++ (seq.unit f) d) a c)) +(check-sat) -- 2.30.2