summaryrefslogtreecommitdiff
path: root/src/theory/strings/regexp_entail.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/strings/regexp_entail.cpp')
-rw-r--r--src/theory/strings/regexp_entail.cpp64
1 files changed, 49 insertions, 15 deletions
diff --git a/src/theory/strings/regexp_entail.cpp b/src/theory/strings/regexp_entail.cpp
index f005b2b42..7e1f42f37 100644
--- a/src/theory/strings/regexp_entail.cpp
+++ b/src/theory/strings/regexp_entail.cpp
@@ -48,6 +48,8 @@ Node RegExpEntail::simpleRegexpConsume(std::vector<Node>& mchildren,
do_next = false;
Node xc = mchildren[mchildren.size() - 1];
Node rc = children[children.size() - 1];
+ Trace("regexp-ext-rewrite-debug")
+ << "* " << xc << " in " << rc << std::endl;
Assert(rc.getKind() != REGEXP_CONCAT);
Assert(xc.getKind() != STRING_CONCAT);
if (rc.getKind() == STRING_TO_REGEXP)
@@ -57,7 +59,15 @@ Node RegExpEntail::simpleRegexpConsume(std::vector<Node>& mchildren,
children.pop_back();
mchildren.pop_back();
do_next = true;
- Trace("regexp-ext-rewrite-debug") << "...strip equal" << std::endl;
+ Trace("regexp-ext-rewrite-debug") << "- strip equal" << std::endl;
+ }
+ else if (rc[0].isConst() && Word::isEmpty(rc[0]))
+ {
+ Trace("regexp-ext-rewrite-debug")
+ << "- ignore empty RE" << std::endl;
+ // ignore and continue
+ children.pop_back();
+ do_next = true;
}
else if (xc.isConst() && rc[0].isConst())
{
@@ -65,8 +75,8 @@ Node RegExpEntail::simpleRegexpConsume(std::vector<Node>& mchildren,
size_t index;
Node s = Word::splitConstant(xc, rc[0], index, t == 0);
Trace("regexp-ext-rewrite-debug")
- << "CRE: Regexp const split : " << xc << " " << rc[0] << " -> "
- << s << " " << index << " " << t << std::endl;
+ << "- CRE: Regexp const split : " << xc << " " << rc[0]
+ << " -> " << s << " " << index << " " << t << std::endl;
if (s.isNull())
{
Trace("regexp-ext-rewrite-debug")
@@ -76,7 +86,7 @@ Node RegExpEntail::simpleRegexpConsume(std::vector<Node>& mchildren,
else
{
Trace("regexp-ext-rewrite-debug")
- << "...strip equal const" << std::endl;
+ << "- strip equal const" << std::endl;
children.pop_back();
mchildren.pop_back();
if (index == 0)
@@ -88,6 +98,7 @@ Node RegExpEntail::simpleRegexpConsume(std::vector<Node>& mchildren,
children.push_back(nm->mkNode(STRING_TO_REGEXP, s));
}
}
+ Trace("regexp-ext-rewrite-debug") << "- split const" << std::endl;
do_next = true;
}
}
@@ -97,7 +108,7 @@ Node RegExpEntail::simpleRegexpConsume(std::vector<Node>& mchildren,
CVC4::String s = xc.getConst<String>();
if (Word::isEmpty(xc))
{
- Trace("regexp-ext-rewrite-debug") << "...ignore empty" << std::endl;
+ Trace("regexp-ext-rewrite-debug") << "- ignore empty" << std::endl;
// ignore and continue
mchildren.pop_back();
do_next = true;
@@ -127,6 +138,8 @@ Node RegExpEntail::simpleRegexpConsume(std::vector<Node>& mchildren,
}
else
{
+ Trace("regexp-ext-rewrite-debug")
+ << "...return false" << std::endl;
return nm->mkConst(false);
}
}
@@ -135,19 +148,23 @@ Node RegExpEntail::simpleRegexpConsume(std::vector<Node>& mchildren,
// see if any/each child does not work
bool result_valid = true;
Node result;
- Node emp_s = nm->mkConst(::CVC4::String(""));
+ Node emp_s = nm->mkConst(String(""));
for (unsigned i = 0; i < rc.getNumChildren(); i++)
{
std::vector<Node> mchildren_s;
std::vector<Node> children_s;
mchildren_s.push_back(xc);
utils::getConcat(rc[i], children_s);
+ Trace("regexp-ext-rewrite-debug") << push;
Node ret = simpleRegexpConsume(mchildren_s, children_s, t);
+ Trace("regexp-ext-rewrite-debug") << pop;
if (!ret.isNull())
{
// one conjunct cannot be satisfied, return false
if (rc.getKind() == REGEXP_INTER)
{
+ Trace("regexp-ext-rewrite-debug")
+ << "...return " << ret << std::endl;
return ret;
}
}
@@ -182,10 +199,15 @@ Node RegExpEntail::simpleRegexpConsume(std::vector<Node>& mchildren,
{
// all disjuncts cannot be satisfied, return false
Assert(rc.getKind() == REGEXP_UNION);
+ Trace("regexp-ext-rewrite-debug")
+ << "...return false" << std::endl;
return nm->mkConst(false);
}
else
{
+ Trace("regexp-ext-rewrite-debug")
+ << "- same result, try again, children now " << children
+ << std::endl;
// all branches led to the same result
children.pop_back();
mchildren.pop_back();
@@ -210,17 +232,19 @@ Node RegExpEntail::simpleRegexpConsume(std::vector<Node>& mchildren,
std::vector<Node> children_s;
utils::getConcat(rc[0], children_s);
Trace("regexp-ext-rewrite-debug")
- << "...recursive call on body of star" << std::endl;
+ << "- recursive call on body of star" << std::endl;
+ Trace("regexp-ext-rewrite-debug") << push;
Node ret = simpleRegexpConsume(mchildren_s, children_s, t);
+ Trace("regexp-ext-rewrite-debug") << pop;
if (!ret.isNull())
{
Trace("regexp-ext-rewrite-debug")
- << "CRE : regexp star infeasable " << xc << " " << rc
+ << "- CRE : regexp star infeasable " << xc << " " << rc
<< std::endl;
children.pop_back();
if (!children.empty())
{
- Trace("regexp-ext-rewrite-debug") << "...continue" << std::endl;
+ Trace("regexp-ext-rewrite-debug") << "- continue" << std::endl;
do_next = true;
}
}
@@ -244,16 +268,22 @@ Node RegExpEntail::simpleRegexpConsume(std::vector<Node>& mchildren,
std::reverse(mchildren_ss.begin(), mchildren_ss.end());
std::reverse(children_ss.begin(), children_ss.end());
}
- if (simpleRegexpConsume(mchildren_ss, children_ss, t)
- .isNull())
+ Trace("regexp-ext-rewrite-debug")
+ << "- recursive call required repeat star" << std::endl;
+ Trace("regexp-ext-rewrite-debug") << push;
+ Node rets = simpleRegexpConsume(mchildren_ss, children_ss, t);
+ Trace("regexp-ext-rewrite-debug") << pop;
+ if (rets.isNull())
{
can_skip = true;
}
}
if (!can_skip)
{
+ TypeNode stype = nm->stringType();
+ Node prev = utils::mkConcat(mchildren, stype);
Trace("regexp-ext-rewrite-debug")
- << "...can't skip" << std::endl;
+ << "- can't skip" << std::endl;
// take the result of fully consuming once
if (t == 1)
{
@@ -262,12 +292,15 @@ Node RegExpEntail::simpleRegexpConsume(std::vector<Node>& mchildren,
mchildren.clear();
mchildren.insert(
mchildren.end(), mchildren_s.begin(), mchildren_s.end());
- do_next = true;
+ Node curr = utils::mkConcat(mchildren, stype);
+ do_next = (prev != curr);
+ Trace("regexp-ext-rewrite-debug")
+ << "- do_next = " << do_next << std::endl;
}
else
{
Trace("regexp-ext-rewrite-debug")
- << "...can skip " << rc << " from " << xc << std::endl;
+ << "- can skip " << rc << " from " << xc << std::endl;
}
}
}
@@ -276,7 +309,7 @@ Node RegExpEntail::simpleRegexpConsume(std::vector<Node>& mchildren,
if (!do_next)
{
Trace("regexp-ext-rewrite")
- << "Cannot consume : " << xc << " " << rc << std::endl;
+ << "- cannot consume : " << xc << " " << rc << std::endl;
}
}
}
@@ -286,6 +319,7 @@ Node RegExpEntail::simpleRegexpConsume(std::vector<Node>& mchildren,
std::reverse(mchildren.begin(), mchildren.end());
}
}
+ Trace("regexp-ext-rewrite-debug") << "...finished, return null" << std::endl;
return Node::null();
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback