From 21511862f74c74a9c75da1de01e6b0e0a8120613 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Sun, 30 May 2021 17:35:08 -0700 Subject: [PATCH] Compute model values for nested sequences in order (#6631) Fixes #6337 (the other benchmarks in this issue are either solved correctly or time out after the changes in #6615) and fixes #5665. While computing the model for a nested equivalence class containing seq.unit, we were looking up the representative of the argument in (seq.unit (seq.unit j)) and the representative was simpliy (seq.unit j). However, we had assigned (seq.unit 0) to (seq.unit j) earlier. A second equivalence class of type (Seq (Seq Int)) and length 1 was later assigned (seq.unit (seq.unit 0)) and we didn't detect that (seq.unit (seq.unit j)) and (seq.unit (seq.unit 0)) have the same value. This was incorrect because we do not allow assigning the same value to different equivalence classes. In this case, it led to one of the assertions being false. This commit fixes the issues in two ways: it ensures that types are processed in ascending order of nesting (e.g., (Seq Int) terms are processed before (Seq (Seq Int)) terms) and it changes the procedure to look up the representative in the model instead of the theory state to take into account the model values assigned to the elements of sequences. cc @yoni206 --- src/theory/strings/theory_strings.cpp | 58 ++++++++++++++----- src/theory/strings/theory_strings.h | 20 ++++--- test/regress/CMakeLists.txt | 2 + .../regress0/seq/issue5665-invalid-model.smt2 | 11 ++++ test/regress/regress0/seq/issue6337-seq.smt2 | 12 ++++ 5 files changed, 78 insertions(+), 25 deletions(-) create mode 100644 test/regress/regress0/seq/issue5665-invalid-model.smt2 create mode 100644 test/regress/regress0/seq/issue6337-seq.smt2 diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index b1f5a0765..f4daed85d 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -211,7 +211,10 @@ bool TheoryStrings::collectModelValues(TheoryModel* m, Trace("strings-debug-model") << d_esolver.debugPrintModel() << std::endl; } Trace("strings-model") << "TheoryStrings::collectModelValues" << std::endl; + // Collects representatives by types and orders sequence types by how nested + // they are std::map > repSet; + std::unordered_set toProcess; // Generate model // get the relevant string equivalence classes for (const Node& s : termSet) @@ -221,31 +224,51 @@ bool TheoryStrings::collectModelValues(TheoryModel* m, { Node r = d_state.getRepresentative(s); repSet[tn].insert(r); + toProcess.insert(tn); } } - for (const std::pair >& rst : repSet) + + while (!toProcess.empty()) { - // get partition of strings of equal lengths, per type - std::map > > colT; - std::map > ltsT; - std::vector repVec(rst.second.begin(), rst.second.end()); - d_state.separateByLength(repVec, colT, ltsT); - // now collect model info for the type - TypeNode st = rst.first; - if (!collectModelInfoType(st, rst.second, colT[st], ltsT[st], m)) + // Pick one of the remaining types to collect model values for + TypeNode tn = *toProcess.begin(); + if (!collectModelInfoType(tn, toProcess, repSet, m)) { return false; } } + return true; } -bool TheoryStrings::collectModelInfoType(TypeNode tn, - const std::unordered_set& repSet, - std::vector >& col, - std::vector& lts, - TheoryModel* m) +bool TheoryStrings::collectModelInfoType( + TypeNode tn, + std::unordered_set& toProcess, + const std::map >& repSet, + TheoryModel* m) { + // Make sure that the model values for the element type of sequences are + // computed first + if (tn.isSequence() && tn.getSequenceElementType().isSequence()) + { + TypeNode tnElem = tn.getSequenceElementType(); + if (toProcess.find(tnElem) != toProcess.end() + && !collectModelInfoType(tnElem, toProcess, repSet, m)) + { + return false; + } + } + toProcess.erase(tn); + + // get partition of strings of equal lengths for the representatives of the + // current type + std::map > > colT; + std::map > ltsT; + const std::vector repVec(repSet.at(tn).begin(), repSet.at(tn).end()); + d_state.separateByLength(repVec, colT, ltsT); + const std::vector >& col = colT[tn]; + const std::vector& lts = ltsT[tn]; + NodeManager* nm = NodeManager::currentNM(); std::map< Node, Node > processed; //step 1 : get all values for known lengths @@ -322,7 +345,10 @@ bool TheoryStrings::collectModelInfoType(TypeNode tn, Node argVal; if (nfe.d_nf[0][0].getType().isStringLike()) { - argVal = d_state.getRepresentative(nfe.d_nf[0][0]); + // By this point, we should have assigned model values for the + // elements of this sequence type because of the check in the + // beginning of this method + argVal = m->getRepresentative(nfe.d_nf[0][0]); } else { @@ -479,7 +505,7 @@ bool TheoryStrings::collectModelInfoType(TypeNode tn, } Trace("strings-model") << "String Model : Pure Assigned." << std::endl; //step 4 : assign constants to all other equivalence classes - for (const Node& rn : repSet) + for (const Node& rn : repVec) { if (processed.find(rn) == processed.end()) { diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index a671129d4..fc5e47194 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -190,17 +190,19 @@ class TheoryStrings : public Theory { /** Collect model info for type tn * * Assigns model values (in m) to all relevant terms of the string-like type - * tn in the current context, which are stored in repSet. Furthermore, - * col is a partition of repSet where equivalence classes are grouped into - * sets having equal length, where these lengths are stored in lts. + * tn in the current context, which are stored in repSet[tn]. * - * Returns false if a conflict is discovered while doing this assignment. + * @param tn The type to compute model values for + * @param toProcess Remaining types to compute model values for + * @param repSet A map of types to the representatives of the equivalence + * classes of the given type + * @return false if a conflict is discovered while doing this assignment. */ - bool collectModelInfoType(TypeNode tn, - const std::unordered_set& repSet, - std::vector>& col, - std::vector& lts, - TheoryModel* m); + bool collectModelInfoType( + TypeNode tn, + std::unordered_set& toProcess, + const std::map>& repSet, + TheoryModel* m); /** assert pending fact * diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 7de2d9789..cff39938c 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -997,6 +997,8 @@ set(regress_0_tests regress0/seq/issue5543-unit-cmv.smt2 regress0/seq/issue5547-seq-len-unit.smt2 regress0/seq/issue5547-small-seq-len-unit.smt2 + regress0/seq/issue5665-invalid-model.smt2 + regress0/seq/issue6337-seq.smt2 regress0/seq/len_simplify.smt2 regress0/seq/seq-2var.smt2 regress0/seq/seq-ex1.smt2 diff --git a/test/regress/regress0/seq/issue5665-invalid-model.smt2 b/test/regress/regress0/seq/issue5665-invalid-model.smt2 new file mode 100644 index 000000000..5a4b1186d --- /dev/null +++ b/test/regress/regress0/seq/issue5665-invalid-model.smt2 @@ -0,0 +1,11 @@ +(set-logic QF_SLIA) +(declare-fun a () (Seq (Seq Int))) +(declare-fun b () (Seq (Seq Int))) +(declare-fun c () (Seq (Seq Int))) +(declare-fun d () (Seq Int)) +(declare-fun e () Int) +(declare-fun f () Int) +(assert (= (seq.extract d e 1) (seq.unit f))) +(assert (distinct a b (seq.++ (seq.unit d) c))) +(set-info :status sat) +(check-sat) diff --git a/test/regress/regress0/seq/issue6337-seq.smt2 b/test/regress/regress0/seq/issue6337-seq.smt2 new file mode 100644 index 000000000..f6436f412 --- /dev/null +++ b/test/regress/regress0/seq/issue6337-seq.smt2 @@ -0,0 +1,12 @@ +(set-logic QF_SLIA) +(declare-fun x () (Seq (Seq Int))) +(declare-fun y () (Seq (Seq Int))) +(declare-fun z () (Seq Int)) +(declare-fun w () (Seq Int)) +(declare-fun j () Int) +(assert (= w (seq.unit j))) +(assert (not (= x (seq.unit z)))) +(assert (not (= y (seq.unit w)))) +(assert (not (= x y))) +(set-info :status sat) +(check-sat) -- 2.30.2