From 32d1ef7990a1bd0931c5f781d5046ddce900effd Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 4 Oct 2018 15:11:31 -0500 Subject: [PATCH] Fix end constraint for regexp elimination (#2571) --- src/theory/strings/regexp_elim.cpp | 45 ++++++++++++++++++++--- test/regress/CMakeLists.txt | 1 + test/regress/Makefile.tests | 1 + test/regress/regress1/strings/nt6-dd.smt2 | 13 +++++++ 4 files changed, 54 insertions(+), 6 deletions(-) create mode 100644 test/regress/regress1/strings/nt6-dd.smt2 diff --git a/src/theory/strings/regexp_elim.cpp b/src/theory/strings/regexp_elim.cpp index 7d65a872c..8ea26fca9 100644 --- a/src/theory/strings/regexp_elim.cpp +++ b/src/theory/strings/regexp_elim.cpp @@ -156,12 +156,45 @@ Node RegExpElimination::eliminateConcat(Node atom) // Notice that if the last gap is not exact and its minsize is zero, // then the last indexof/substr constraint entails the following // constraint, so it is not necessary to add. - if (gap_minsize_end > 0 || gap_exact_end) + // Below, we may write "A" for (str.to.re "A") and _ for re.allchar: + Node cEnd = nm->mkConst(Rational(gap_minsize_end)); + if (gap_exact_end) { - Node fit = nm->mkNode( - gap_exact_end ? EQUAL : LEQ, - nm->mkNode(PLUS, prev_end, nm->mkConst(Rational(gap_minsize_end))), - lenx); + Assert(!sep_children.empty()); + // if it is strict, it corresponds to a substr case. + // For example: + // x in (re.++ "A" (re.* _) "B" _ _) ---> + // ... ^ "B" = substr( x, len( x ) - 3, 1 ) ^ ... + Node sc = sep_children.back(); + Node lenSc = nm->mkNode(STRING_LENGTH, sc); + Node loc = nm->mkNode(MINUS, lenx, nm->mkNode(PLUS, lenSc, cEnd)); + Node scc = sc.eqNode(nm->mkNode(STRING_SUBSTR, x, loc, lenSc)); + conj.push_back(scc); + // We also must ensure that we fit. This constraint is necessary in + // addition to the constraint above. Take this example: + // x in (re.++ "A" _ (re.* _) "B" _) ---> + // substr( x, 0, 1 ) = "A" ^ // find "A" + // indexof( x, "B", 2 ) != -1 ^ // find "B" >=1 after "A" + // substr( x, len(x)-2, 1 ) = "B" ^ // "B" is at end - 2. + // indexof( x, "B", 2 ) <= len( x ) - 2 + // The last constaint ensures that the second and third constraints + // may refer to the same "B". If it were not for the last constraint, it + // would have been the case than "ABB" would be a model for x, where + // the second constraint refers to the third position, and the third + // constraint refers to the second position. + Node fit = nm->mkNode(gap_exact[sep_children.size() - 1] ? EQUAL : LEQ, + nm->mkNode(MINUS, prev_end, lenSc), + loc); + conj.push_back(fit); + } + else if (gap_minsize_end > 0) + { + // if it is non-strict, we are in a "greedy find" situtation where + // we just need to ensure that the next occurrence fits. + // For example: + // x in (re.++ "A" (re.* _) "B" _ _ (re.* _)) ---> + // ... ^ indexof( x, "B", 1 ) + 2 <= len( x ) + Node fit = nm->mkNode(LEQ, nm->mkNode(PLUS, prev_end, cEnd), lenx); conj.push_back(fit); } Node res = conj.size() == 1 ? conj[0] : nm->mkNode(AND, conj); @@ -180,7 +213,7 @@ Node RegExpElimination::eliminateConcat(Node atom) Node bvl = nm->mkNode(BOUND_VAR_LIST, non_greedy_find_vars); res = nm->mkNode(EXISTS, bvl, body); } - // e.g., writing "A" for (str.to.re "A") and _ for re.allchar: + // Examples of this elimination: // x in (re.++ "A" (re.* _) "B" (re.* _)) ---> // substr(x,0,1)="A" ^ indexof(x,"B",1)!=-1 // x in (re.++ (re.* _) "A" _ _ _ (re.* _) "B" _ _ (re.* _)) ---> diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 0c68b1920..a5bf3e819 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1520,6 +1520,7 @@ set(regress_1_tests regress1/strings/norn-ab.smt2 regress1/strings/norn-nel-bug-052116.smt2 regress1/strings/norn-simp-rew-sat.smt2 + regress1/strings/nt6-dd.smt2 regress1/strings/nterm-re-inter-sigma.smt2 regress1/strings/pierre150331.smt2 regress1/strings/policy_variable.smt2 diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index 4e77694b7..4e9837c36 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1517,6 +1517,7 @@ REG1_TESTS = \ regress1/strings/norn-ab.smt2 \ regress1/strings/norn-nel-bug-052116.smt2 \ regress1/strings/norn-simp-rew-sat.smt2 \ + regress1/strings/nt6-dd.smt2 \ regress1/strings/nterm-re-inter-sigma.smt2 \ regress1/strings/pierre150331.smt2 \ regress1/strings/policy_variable.smt2 \ diff --git a/test/regress/regress1/strings/nt6-dd.smt2 b/test/regress/regress1/strings/nt6-dd.smt2 new file mode 100644 index 000000000..30a0884a3 --- /dev/null +++ b/test/regress/regress1/strings/nt6-dd.smt2 @@ -0,0 +1,13 @@ +; COMMAND-LINE: --strings-exp --re-elim +; EXPECT: sat +(set-info :smt-lib-version 2.5) +(set-logic ALL) +(set-info :status sat) +(declare-const resource_resource String) +(declare-const p1.0.resource Bool) + +(assert (str.in.re resource_resource (re.++ (str.to.re "ab") (re.* re.allchar) (str.to.re "b") ))) + +(assert (= p1.0.resource (str.in.re resource_resource (re.++ (str.to.re "a") (re.* re.allchar) (str.to.re "b") )))) + +(check-sat) -- 2.30.2