From 7bb6e7970de3719308110dd993cf4393031b8d80 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 27 Oct 2021 10:27:30 -0500 Subject: [PATCH] Deterministic variables for RE elim (#7489) Fixes #6766. --- src/smt/set_defaults.cpp | 6 +++- src/theory/strings/regexp_elim.cpp | 33 +++++++++++++++++-- test/regress/CMakeLists.txt | 1 + .../strings/issue6766-re-elim-bv.smt2 | 9 +++++ 4 files changed, 45 insertions(+), 4 deletions(-) create mode 100644 test/regress/regress1/strings/issue6766-re-elim-bv.smt2 diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index c4935340f..19eab3617 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -302,7 +302,11 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const // formulas at preprocess time. // // We don't want to set this option when we are in logics that contain ALL. - if (!logic.hasEverything() && logic.isTheoryEnabled(THEORY_STRINGS)) + // + // We also must enable stringExp if reElimAgg is true, since this introduces + // bounded quantifiers during preprocessing. + if ((!logic.hasEverything() && logic.isTheoryEnabled(THEORY_STRINGS)) + || opts.strings.regExpElimAgg) { // If the user explicitly set a logic that includes strings, but is not // the generic "ALL" logic, then enable stringsExp. diff --git a/src/theory/strings/regexp_elim.cpp b/src/theory/strings/regexp_elim.cpp index dfe006a86..b3dc309d5 100644 --- a/src/theory/strings/regexp_elim.cpp +++ b/src/theory/strings/regexp_elim.cpp @@ -15,6 +15,7 @@ #include "theory/strings/regexp_elim.h" +#include "expr/bound_var_manager.h" #include "options/strings_options.h" #include "proof/proof_node_manager.h" #include "theory/rewriter.h" @@ -29,6 +30,22 @@ namespace cvc5 { namespace theory { namespace strings { +/** + * Attributes used for constructing unique bound variables. The following + * attributes are used to construct (deterministic) bound variables for + * eliminations within eliminateConcat and eliminateStar respectively. + */ +struct ReElimConcatIndexAttributeId +{ +}; +typedef expr::Attribute + ReElimConcatIndexAttribute; +struct ReElimStarIndexAttributeId +{ +}; +typedef expr::Attribute + ReElimStarIndexAttribute; + RegExpElimination::RegExpElimination(bool isAgg, ProofNodeManager* pnm, context::Context* c) @@ -77,6 +94,7 @@ TrustNode RegExpElimination::eliminateTrusted(Node atom) Node RegExpElimination::eliminateConcat(Node atom, bool isAgg) { NodeManager* nm = NodeManager::currentNM(); + BoundVarManager* bvm = nm->getBoundVarManager(); Node x = atom[0]; Node lenx = nm->mkNode(STRING_LENGTH, x); Node re = atom[1]; @@ -260,7 +278,11 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg) } // if the gap after this one is strict, we need a non-greedy find // thus, we add a symbolic constant - Node k = nm->mkBoundVar(nm->integerType()); + Node cacheVal = + BoundVarManager::getCacheValue(atom, nm->mkConst(Rational(i))); + TypeNode intType = nm->integerType(); + Node k = + bvm->mkBoundVar(cacheVal, intType); non_greedy_find_vars.push_back(k); prev_end = nm->mkNode(PLUS, prev_end, k); } @@ -452,7 +474,10 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg) } else { - k = nm->mkBoundVar(nm->integerType()); + Node cacheVal = + BoundVarManager::getCacheValue(atom, nm->mkConst(Rational(i))); + TypeNode intType = nm->integerType(); + k = bvm->mkBoundVar(cacheVal, intType); Node bound = nm->mkNode(AND, nm->mkNode(LEQ, zero, k), @@ -509,6 +534,7 @@ Node RegExpElimination::eliminateStar(Node atom, bool isAgg) // only aggressive rewrites below here NodeManager* nm = NodeManager::currentNM(); + BoundVarManager* bvm = nm->getBoundVarManager(); Node x = atom[0]; Node lenx = nm->mkNode(STRING_LENGTH, x); Node re = atom[1]; @@ -530,7 +556,8 @@ Node RegExpElimination::eliminateStar(Node atom, bool isAgg) } bool lenOnePeriod = true; std::vector char_constraints; - Node index = nm->mkBoundVar(nm->integerType()); + TypeNode intType = nm->integerType(); + Node index = bvm->mkBoundVar(atom, intType); Node substr_ch = nm->mkNode(STRING_SUBSTR, x, index, nm->mkConst(Rational(1))); substr_ch = Rewriter::rewrite(substr_ch); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 24bb43244..cb535a469 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2271,6 +2271,7 @@ set(regress_1_tests regress1/strings/issue6653-4-rre.smt2 regress1/strings/issue6653-rre.smt2 regress1/strings/issue6653-rre-small.smt2 + regress1/strings/issue6766-re-elim-bv.smt2 regress1/strings/issue6777-seq-nth-eval-cm.smt2 regress1/strings/issue6913.smt2 regress1/strings/issue6973-dup-lemma-conc.smt2 diff --git a/test/regress/regress1/strings/issue6766-re-elim-bv.smt2 b/test/regress/regress1/strings/issue6766-re-elim-bv.smt2 new file mode 100644 index 000000000..13677838b --- /dev/null +++ b/test/regress/regress1/strings/issue6766-re-elim-bv.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --strings-exp --re-elim --re-elim-agg +; EXPECT: sat +(set-logic ALL) +(declare-fun a () String) +(declare-fun b () String) +(assert + (str.in_re (str.++ a (ite (str.in_re (str.++ a "BA" b) (re.++ (re.* (str.to_re "A")) (str.to_re "B"))) b a)) + (re.diff (re.* (str.to_re "A")) (str.to_re "")))) +(check-sat) -- 2.30.2