From: Andrew Reynolds Date: Fri, 22 May 2020 19:27:13 +0000 (-0500) Subject: (proof-new) Add rewrite corresponding to regular expression inclusion (#4513) X-Git-Tag: cvc5-1.0.0~3298 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0b49b88e4d1c299a7cd662cd2221fd826b5bc972;p=cvc5.git (proof-new) Add rewrite corresponding to regular expression inclusion (#4513) This introduces a rewrite based on regular expression inclusion (using calls to the RegExpEntail utility function). This allows us to justify the regular expression inclusion inference as a rewrite. --- diff --git a/src/theory/strings/rewrites.cpp b/src/theory/strings/rewrites.cpp index f1a818bf3..2953a2b3c 100644 --- a/src/theory/strings/rewrites.cpp +++ b/src/theory/strings/rewrites.cpp @@ -70,6 +70,7 @@ const char* toString(Rewrite r) case Rewrite::ITOS_EVAL: return "ITOS_EVAL"; case Rewrite::RE_AND_EMPTY: return "RE_AND_EMPTY"; case Rewrite::RE_ANDOR_FLATTEN: return "RE_ANDOR_FLATTEN"; + case Rewrite::RE_ANDOR_INC_CONFLICT: return "RE_ANDOR_INC_CONFLICT"; case Rewrite::RE_CHAR_IN_STR_STAR: return "RE_CHAR_IN_STR_STAR"; case Rewrite::RE_CONCAT: return "RE_CONCAT"; case Rewrite::RE_CONCAT_FLATTEN: return "RE_CONCAT_FLATTEN"; diff --git a/src/theory/strings/rewrites.h b/src/theory/strings/rewrites.h index cfa8c8448..7a315ebd3 100644 --- a/src/theory/strings/rewrites.h +++ b/src/theory/strings/rewrites.h @@ -75,6 +75,7 @@ enum class Rewrite : uint32_t ITOS_EVAL, RE_AND_EMPTY, RE_ANDOR_FLATTEN, + RE_ANDOR_INC_CONFLICT, RE_CHAR_IN_STR_STAR, RE_CONCAT, RE_CONCAT_FLATTEN, diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp index d8b8765eb..aa85d1056 100644 --- a/src/theory/strings/sequences_rewriter.cpp +++ b/src/theory/strings/sequences_rewriter.cpp @@ -920,6 +920,7 @@ Node SequencesRewriter::rewriteAndOrRegExp(TNode node) Trace("strings-rewrite-debug") << "Strings::rewriteAndOrRegExp start " << node << std::endl; std::vector node_vec; + std::vector polRegExp[2]; for (const Node& ni : node) { if (ni.getKind() == nk) @@ -951,20 +952,48 @@ Node SequencesRewriter::rewriteAndOrRegExp(TNode node) else if (std::find(node_vec.begin(), node_vec.end(), ni) == node_vec.end()) { node_vec.push_back(ni); + uint32_t pindex = ni.getKind() == REGEXP_COMPLEMENT ? 1 : 0; + Node nia = pindex == 1 ? ni[0] : ni; + polRegExp[pindex].push_back(nia); } } NodeManager* nm = NodeManager::currentNM(); - std::vector nvec; + std::vector emptyVec; + // use inclusion tests + for (const Node& negMem : polRegExp[1]) + { + for (const Node& posMem : polRegExp[0]) + { + Node m1 = nk == REGEXP_INTER ? negMem : posMem; + Node m2 = nk == REGEXP_INTER ? posMem : negMem; + // inclusion test for conflicting case m1 contains m2 + // (re.inter (re.comp R1) R2) --> re.none where R1 includes R2 + // (re.union R1 (re.comp R2)) --> (re.* re.allchar) where R1 includes R2 + if (RegExpEntail::regExpIncludes(m1, m2)) + { + Node retNode; + if (nk == REGEXP_INTER) + { + retNode = nm->mkNode(kind::REGEXP_EMPTY, emptyVec); + } + else + { + retNode = nm->mkNode(REGEXP_STAR, nm->mkNode(REGEXP_SIGMA, emptyVec)); + } + return returnRewrite(node, retNode, Rewrite::RE_ANDOR_INC_CONFLICT); + } + } + } Node retNode; if (node_vec.empty()) { if (nk == REGEXP_INTER) { - retNode = nm->mkNode(REGEXP_STAR, nm->mkNode(REGEXP_SIGMA, nvec)); + retNode = nm->mkNode(REGEXP_STAR, nm->mkNode(REGEXP_SIGMA, emptyVec)); } else { - retNode = nm->mkNode(kind::REGEXP_EMPTY, nvec); + retNode = nm->mkNode(kind::REGEXP_EMPTY, emptyVec); } } else @@ -1442,6 +1471,7 @@ RewriteResponse SequencesRewriter::postRewrite(TNode node) << node << " to " << retNode << std::endl; return RewriteResponse(REWRITE_AGAIN_FULL, retNode); } + Trace("strings-rewrite-nf") << "No rewrites for : " << node << std::endl; return RewriteResponse(REWRITE_DONE, retNode); } @@ -1746,7 +1776,6 @@ Node SequencesRewriter::rewriteSubstr(Node node) } } } - Trace("strings-rewrite-nf") << "No rewrites for : " << node << std::endl; return node; } @@ -2103,7 +2132,6 @@ Node SequencesRewriter::rewriteContains(Node node) } } - Trace("strings-rewrite-nf") << "No rewrites for : " << node << std::endl; return node; } @@ -2318,7 +2346,6 @@ Node SequencesRewriter::rewriteIndexof(Node node) } } - Trace("strings-rewrite-nf") << "No rewrites for : " << node << std::endl; return node; } @@ -2806,7 +2833,6 @@ Node SequencesRewriter::rewriteReplace(Node node) // contains( t, s ) => // contains( replace( t, s, r ), r ) ----> true - Trace("strings-rewrite-nf") << "No rewrites for : " << node << std::endl; return node; } @@ -2859,7 +2885,6 @@ Node SequencesRewriter::rewriteReplaceAll(Node node) return rri; } - Trace("strings-rewrite-nf") << "No rewrites for : " << node << std::endl; return node; } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 506857479..2df07db5a 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -964,6 +964,7 @@ set(regress_0_tests regress0/strings/parser-syms.cvc regress0/strings/quad-028-2-2-unsat.smt2 regress0/strings/re.all.smt2 + regress0/strings/re-in-rewrite.smt2 regress0/strings/re-syntax.smt2 regress0/strings/re_diff.smt2 regress0/strings/regexp-native-simple.cvc diff --git a/test/regress/regress0/strings/re-in-rewrite.smt2 b/test/regress/regress0/strings/re-in-rewrite.smt2 new file mode 100644 index 000000000..d1567768d --- /dev/null +++ b/test/regress/regress0/strings/re-in-rewrite.smt2 @@ -0,0 +1,5 @@ +(set-logic QF_SLIA) +(set-info :status unsat) +(declare-fun x () String) +(assert (str.in_re x (re.inter (re.comp (re.++ re.allchar (re.* re.allchar))) (re.++ (str.to_re "a") (re.* re.allchar))))) +(check-sat)