From: Andres Noetzli Date: Sat, 13 Nov 2021 20:24:44 +0000 (-0800) Subject: Skip `str.code` inferences for sequence eqcs (#7644) X-Git-Tag: cvc5-1.0.0~820 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f5b8f74ec2f7297cd54e19459f039416df67f862;p=cvc5.git Skip `str.code` inferences for sequence eqcs (#7644) Fixes cvc5/cvc5-projects#340. Type checking failed because cvc5 was trying to construct a term (str.to_code (seq.unit false)). We do not allow the construction of terms (str.to_code t) where t is not of type string. This commit fixes the issue by skipping sequence equivalence classes when doing inferences related to str.to_code. Note that the regression test is slightly different from the original unit test. It asserts that the index passed to seq.nth is non-negative, which ensures that we can check the resulting model. I have checked that the modified regression test triggers the issue before the change in this commit. --- diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp index 69d41e9d7..69d50a7d9 100644 --- a/src/theory/strings/base_solver.cpp +++ b/src/theory/strings/base_solver.cpp @@ -46,7 +46,7 @@ void BaseSolver::checkInit() // build term index d_eqcInfo.clear(); d_termIndex.clear(); - d_stringsEqc.clear(); + d_stringLikeEqc.clear(); Trace("strings-base") << "BaseSolver::checkInit" << std::endl; // count of congruent, non-congruent per operator (independent of type), @@ -65,7 +65,7 @@ void BaseSolver::checkInit() std::map& tti = d_termIndex[tn]; if (tn.isStringLike()) { - d_stringsEqc.push_back(eqc); + d_stringLikeEqc.push_back(eqc); emps = Word::mkEmptyWord(tn); } Node var; @@ -512,7 +512,7 @@ void BaseSolver::checkCardinality() // between lengths of string terms that are disequal (DEQ-LENGTH-SP). std::map > > cols; std::map > lts; - d_state.separateByLength(d_stringsEqc, cols, lts); + d_state.separateByLength(d_stringLikeEqc, cols, lts); for (std::pair > >& c : cols) { checkCardinalityType(c.first, c.second, lts[c.first]); @@ -759,9 +759,9 @@ Node BaseSolver::explainBestContentEqc(Node n, Node eqc, std::vector& exp) return Node::null(); } -const std::vector& BaseSolver::getStringEqc() const +const std::vector& BaseSolver::getStringLikeEqc() const { - return d_stringsEqc; + return d_stringLikeEqc; } Node BaseSolver::TermIndex::add(TNode n, diff --git a/src/theory/strings/base_solver.h b/src/theory/strings/base_solver.h index bf61b93b2..96d275cd5 100644 --- a/src/theory/strings/base_solver.h +++ b/src/theory/strings/base_solver.h @@ -106,7 +106,7 @@ class BaseSolver : protected EnvObj /** * Get the set of equivalence classes of type string. */ - const std::vector& getStringEqc() const; + const std::vector& getStringLikeEqc() const; //-----------------------end query functions private: @@ -236,8 +236,8 @@ class BaseSolver : protected EnvObj * for more information. */ std::map d_eqcInfo; - /** The list of equivalence classes of type string */ - std::vector d_stringsEqc; + /** The list of equivalence classes of string-like types */ + std::vector d_stringLikeEqc; /** A term index for each type, function kind pair */ std::map > d_termIndex; /** the cardinality of the alphabet */ diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp index cc9365d38..46f75bd10 100644 --- a/src/theory/strings/core_solver.cpp +++ b/src/theory/strings/core_solver.cpp @@ -131,7 +131,7 @@ void CoreSolver::checkCycles() d_eqc.clear(); // Rebuild strings eqc based on acyclic ordering, first copy the equivalence // classes from the base solver. - const std::vector& eqc = d_bsolver.getStringEqc(); + const std::vector& eqc = d_bsolver.getStringLikeEqc(); d_strings_eqc.clear(); for (const Node& r : eqc) { diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 8324e3edb..ed00758a8 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -877,7 +877,7 @@ void TheoryStrings::computeCareGraph(){ void TheoryStrings::checkRegisterTermsPreNormalForm() { - const std::vector& seqc = d_bsolver.getStringEqc(); + const std::vector& seqc = d_bsolver.getStringLikeEqc(); for (const Node& eqc : seqc) { eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, d_equalityEngine); @@ -906,9 +906,14 @@ void TheoryStrings::checkCodes() // str.code applied to the proxy variables for each equivalence classes that // are constants of size one std::vector const_codes; - const std::vector& seqc = d_bsolver.getStringEqc(); + const std::vector& seqc = d_bsolver.getStringLikeEqc(); for (const Node& eqc : seqc) { + if (!eqc.getType().isString()) + { + continue; + } + NormalForm& nfe = d_csolver.getNormalForm(eqc); if (nfe.d_nf.size() == 1 && nfe.d_nf[0].isConst()) { @@ -972,7 +977,7 @@ void TheoryStrings::checkCodes() void TheoryStrings::checkRegisterTermsNormalForms() { - const std::vector& seqc = d_bsolver.getStringEqc(); + const std::vector& seqc = d_bsolver.getStringLikeEqc(); for (const Node& eqc : seqc) { NormalForm& nfi = d_csolver.getNormalForm(eqc); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 4937c8481..bffb3e8cb 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1087,6 +1087,7 @@ set(regress_0_tests regress0/seq/issue5665-invalid-model.smt2 regress0/seq/issue6337-seq.smt2 regress0/seq/len_simplify.smt2 + regress0/seq/proj-issue340.smt2 regress0/seq/seq-2var.smt2 regress0/seq/seq-ex1.smt2 regress0/seq/seq-ex2.smt2 diff --git a/test/regress/regress0/seq/proj-issue340.smt2 b/test/regress/regress0/seq/proj-issue340.smt2 new file mode 100644 index 000000000..75a4fb3a6 --- /dev/null +++ b/test/regress/regress0/seq/proj-issue340.smt2 @@ -0,0 +1,9 @@ +(set-logic QF_SLIA) +(declare-const x0 Bool) +(declare-const x2 (Seq Bool)) +(declare-const i Int) +(assert (= i (str.to_int (str.from_code (seq.len x2))))) +(assert (not (seq.nth x2 i))) +(assert (>= i 0)) +(set-info :status sat) +(check-sat)