From b224d8415386f685db31ce49f3cd331be842729e Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 28 Jul 2020 13:25:40 -0500 Subject: [PATCH] Fix regular expression delta for complement (#4765) Fixes #4759 . Also refactors this method. --- src/theory/strings/regexp_operation.cpp | 254 +++++++++--------- test/regress/CMakeLists.txt | 1 + .../strings/issue4759-comp-delta.smt2 | 5 + 3 files changed, 126 insertions(+), 134 deletions(-) create mode 100644 test/regress/regress1/strings/issue4759-comp-delta.smt2 diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index a91210a7b..017d861a2 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -117,161 +117,147 @@ RegExpConstType RegExpOpr::getRegExpConstType(Node r) // 0-unknown, 1-yes, 2-no int RegExpOpr::delta( Node r, Node &exp ) { - Trace("regexp-delta") << "RegExp-Delta starts with /" << mkString( r ) << "/" << std::endl; + std::map >::const_iterator itd = + d_delta_cache.find(r); + if (itd != d_delta_cache.end()) + { + // already computed + exp = itd->second.second; + return itd->second.first; + } + Trace("regexp-delta") << "RegExpOpr::delta: " << r << std::endl; int ret = 0; - if( d_delta_cache.find( r ) != d_delta_cache.end() ) { - ret = d_delta_cache[r].first; - exp = d_delta_cache[r].second; - } else { - Kind k = r.getKind(); - switch( k ) { - case kind::REGEXP_EMPTY: { - ret = 2; - break; - } - case kind::REGEXP_SIGMA: { - ret = 2; - break; - } - case kind::STRING_TO_REGEXP: { - Node tmp = Rewriter::rewrite(r[0]); - if(tmp.isConst()) { - if(tmp == d_emptyString) { - ret = 1; - } else { - ret = 2; - } + NodeManager* nm = NodeManager::currentNM(); + Kind k = r.getKind(); + switch (k) + { + case REGEXP_EMPTY: + case REGEXP_SIGMA: + case REGEXP_RANGE: + { + // does not contain empty string + ret = 2; + break; + } + case STRING_TO_REGEXP: + { + Node tmp = Rewriter::rewrite(r[0]); + if (tmp.isConst()) + { + if (tmp == d_emptyString) + { + ret = 1; } else { - ret = 0; - if(tmp.getKind() == kind::STRING_CONCAT) { - for(unsigned i=0; i vec_nodes; - for(unsigned i=0; imkNode(kind::AND, vec_nodes); - } + ret = 2; } - break; } - case kind::REGEXP_UNION: { - bool flag = false; - std::vector< Node > vec_nodes; - for(unsigned i=0; imkNode(kind::OR, vec_nodes); - } + if (ret == 0) + { + exp = r[0].eqNode(d_emptyString); } - break; } - case kind::REGEXP_INTER: { - bool flag = false; - std::vector< Node > vec_nodes; - for(unsigned i=0; i vec; + int checkTmp = k == REGEXP_UNION ? 1 : 2; + int retTmp = k == REGEXP_UNION ? 2 : 1; + for (const Node& rc : r) + { + Node exp2; + int tmp = delta(rc, exp2); + if (tmp == checkTmp) + { + // return is implied by the child's return value + ret = checkTmp; + break; } - if(ret != 2) { - if(!flag) { - ret = 1; - } else { - exp = vec_nodes.size()==1 ? vec_nodes[0] : NodeManager::currentNM()->mkNode(kind::AND, vec_nodes); - } + else if (tmp == 0) + { + // unknown if child contains empty string + Assert(!exp2.isNull()); + vec.push_back(exp2); + hasUnknownChild = true; } - break; - } - case kind::REGEXP_STAR: { - ret = 1; - break; - } - case kind::REGEXP_PLUS: { - ret = delta( r[0], exp ); - break; - } - case kind::REGEXP_OPT: { - ret = 1; - break; - } - case kind::REGEXP_RANGE: { - ret = 2; - break; } - case kind::REGEXP_LOOP: { - uint32_t lo = utils::getLoopMinOccurrences(r); - if (lo == 0) + if (ret != checkTmp) + { + if (!hasUnknownChild) { - ret = 1; + ret = retTmp; } else { - ret = delta(r[0], exp); + Kind kr = k == REGEXP_UNION ? OR : AND; + exp = vec.size() == 1 ? vec[0] : nm->mkNode(kr, vec); } - break; } - case kind::REGEXP_COMPLEMENT: + break; + } + case REGEXP_STAR: + case REGEXP_OPT: + { + // contains empty string + ret = 1; + break; + } + case REGEXP_PLUS: + { + ret = delta(r[0], exp); + break; + } + case REGEXP_LOOP: + { + uint32_t lo = utils::getLoopMinOccurrences(r); + if (lo == 0) { - int tmp = delta(r[0], exp); - // flip the result if known - tmp = tmp == 0 ? 0 : (3 - tmp); - exp = exp.isNull() ? exp : exp.negate(); - break; + ret = 1; } - default: { - Assert(!utils::isRegExpKind(k)); - break; + else + { + ret = delta(r[0], exp); } + break; } - if(!exp.isNull()) { - exp = Rewriter::rewrite(exp); + case REGEXP_COMPLEMENT: + { + int tmp = delta(r[0], exp); + // flip the result if known + ret = tmp == 0 ? 0 : (3 - tmp); + exp = exp.isNull() ? exp : exp.negate(); + break; + } + default: + { + Assert(!utils::isRegExpKind(k)); + break; } - std::pair< int, Node > p(ret, exp); - d_delta_cache[r] = p; } - Trace("regexp-delta") << "RegExp-Delta returns : " << ret << std::endl; + if (!exp.isNull()) + { + exp = Rewriter::rewrite(exp); + } + std::pair p(ret, exp); + d_delta_cache[r] = p; + Trace("regexp-delta") << "RegExpOpr::delta returns " << ret << " for " << r + << ", expr = " << exp << std::endl; return ret; } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 7f3c693c0..95c272a3e 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1810,6 +1810,7 @@ set(regress_1_tests regress1/strings/issue4608-re-derive.smt2 regress1/strings/issue4735.smt2 regress1/strings/issue4735_2.smt2 + regress1/strings/issue4759-comp-delta.smt2 regress1/strings/kaluza-fl.smt2 regress1/strings/loop002.smt2 regress1/strings/loop003.smt2 diff --git a/test/regress/regress1/strings/issue4759-comp-delta.smt2 b/test/regress/regress1/strings/issue4759-comp-delta.smt2 new file mode 100644 index 000000000..2b6d73279 --- /dev/null +++ b/test/regress/regress1/strings/issue4759-comp-delta.smt2 @@ -0,0 +1,5 @@ +(set-logic QF_S) +(set-info :status unsat) +(declare-fun a () String) +(assert (str.in_re "" (re.++ (str.to_re a) (re.comp re.all)))) +(check-sat) -- 2.30.2