RegExpOpr::~RegExpOpr() {}
bool RegExpOpr::checkConstRegExp( Node r ) {
+ Assert(r.getType().isRegExp());
Trace("strings-regexp-cstre")
<< "RegExpOpr::checkConstRegExp /" << mkString(r) << "/" << std::endl;
RegExpConstType rct = getRegExpConstType(r);
RegExpConstType RegExpOpr::getRegExpConstType(Node r)
{
+ Assert(r.getType().isRegExp());
std::unordered_map<Node, RegExpConstType, NodeHashFunction>::iterator it;
std::vector<TNode> visit;
TNode cur;
{
d_constCache[cur] = RE_C_CONSTANT;
}
+ else if (!isRegExpKind(ck))
+ {
+ // non-regular expression applications, e.g. function applications
+ // with regular expression return type are treated as variables.
+ d_constCache[cur] = RE_C_VARIABLE;
+ }
else
{
d_constCache[cur] = RE_C_UNKNOWN;
visit.push_back(cur);
- visit.insert(visit.end(), cur.begin(), cur.end());
+ if (ck == REGEXP_LOOP)
+ {
+ // only add the first child of loop
+ visit.push_back(cur[0]);
+ }
+ else
+ {
+ visit.insert(visit.end(), cur.begin(), cur.end());
+ }
}
}
else if (it->second == RE_C_UNKNOWN)
return d_constCache[r];
}
+bool RegExpOpr::isRegExpKind(Kind k)
+{
+ return k == REGEXP_EMPTY || k == REGEXP_SIGMA || k == STRING_TO_REGEXP
+ || k == REGEXP_CONCAT || k == REGEXP_UNION || k == REGEXP_INTER
+ || k == REGEXP_STAR || k == REGEXP_PLUS || k == REGEXP_OPT
+ || k == REGEXP_RANGE || k == REGEXP_LOOP || k == REGEXP_RV;
+}
+
// 0-unknown, 1-yes, 2-no
int RegExpOpr::delta( Node r, Node &exp ) {
Trace("regexp-delta") << "RegExp-Delta starts with /" << mkString( r ) << "/" << std::endl;
ret = d_delta_cache[r].first;
exp = d_delta_cache[r].second;
} else {
- int k = r.getKind();
+ Kind k = r.getKind();
switch( k ) {
case kind::REGEXP_EMPTY: {
ret = 2;
break;
}
default: {
- //Trace("strings-error") << "Unsupported term: " << mkString( r ) << " in delta of RegExp." << std::endl;
- Unreachable();
+ Assert(!isRegExpKind(k));
+ break;
}
}
if(!exp.isNull()) {
break;
}
default: {
- //Trace("strings-error") << "Unsupported term: " << mkString( r ) << " in derivative of RegExp." << std::endl;
- Unreachable();
+ Assert(!isRegExpKind(r.getKind()));
+ return 0;
+ break;
}
}
if(retNode != d_emptyRegexp) {
retNode = d_emptyRegexp;
}
} else {
- int k = r.getKind();
+ Kind k = r.getKind();
switch( k ) {
case kind::REGEXP_EMPTY: {
retNode = d_emptyRegexp;
default: {
Trace("strings-error") << "Unsupported term: " << mkString( r ) << " in derivative of RegExp." << std::endl;
Unreachable();
+ break;
}
}
if(retNode != d_emptyRegexp) {
// cset is code points
std::set<unsigned> cset;
SetNodes vset;
- int k = r.getKind();
+ Kind k = r.getKind();
switch( k ) {
case kind::REGEXP_EMPTY: {
break;
}
- case kind::REGEXP_SIGMA: {
- Assert(d_lastchar < std::numeric_limits<unsigned>::max());
- for (unsigned i = 0; i <= d_lastchar; i++)
- {
- cset.insert(i);
- }
- break;
- }
case kind::REGEXP_RANGE: {
unsigned a = r[0].getConst<String>().front();
a = String::convertUnsignedIntToCode(a);
firstChars(r[0], cset, vset);
break;
}
+ case kind::REGEXP_SIGMA:
default: {
- Trace("regexp-error") << "Unsupported term: " << r << " in firstChars." << std::endl;
- Unreachable();
+ // we do not expect to call this function on regular expressions that
+ // aren't a standard regular expression kind. However, if we do, then
+ // the following code is conservative and says that the current
+ // regular expression can begin with any character.
+ Assert(k == REGEXP_SIGMA);
+ // can start with any character
+ Assert(d_lastchar < std::numeric_limits<unsigned>::max());
+ for (unsigned i = 0; i <= d_lastchar; i++)
+ {
+ cset.insert(i);
+ }
+ break;
}
}
pcset.insert(cset.begin(), cset.end());
if(itr != d_simpl_neg_cache.end()) {
new_nodes.push_back( itr->second );
} else {
- int k = r.getKind();
+ Kind k = r.getKind();
Node conc;
switch( k ) {
case kind::REGEXP_EMPTY: {
break;
}
default: {
- Trace("strings-error") << "Unsupported term: " << r << " in simplifyNRegExp." << std::endl;
- Assert( false, "Unsupported Term" );
+ Assert(!isRegExpKind(k));
+ break;
}
}
- conc = Rewriter::rewrite( conc );
- new_nodes.push_back( conc );
- d_simpl_neg_cache[p] = conc;
+ if (!conc.isNull())
+ {
+ conc = Rewriter::rewrite(conc);
+ new_nodes.push_back(conc);
+ d_simpl_neg_cache[p] = conc;
+ }
}
}
void RegExpOpr::simplifyPRegExp( Node s, Node r, std::vector< Node > &new_nodes ) {
if(itr != d_simpl_cache.end()) {
new_nodes.push_back( itr->second );
} else {
- int k = r.getKind();
+ Kind k = r.getKind();
Node conc;
switch( k ) {
case kind::REGEXP_EMPTY: {
break;
}
default: {
- Trace("strings-error") << "Unsupported term: " << r << " in simplifyPRegExp." << std::endl;
- Assert( false, "Unsupported Term" );
+ Assert(!isRegExpKind(k));
+ break;
}
}
- conc = Rewriter::rewrite( conc );
- new_nodes.push_back( conc );
- d_simpl_cache[p] = conc;
+ if (!conc.isNull())
+ {
+ conc = Rewriter::rewrite(conc);
+ new_nodes.push_back(conc);
+ d_simpl_cache[p] = conc;
+ }
}
}
break;
}
default:
- Trace("strings-error") << "Unsupported term: " << r << " in RegExp." << std::endl;
- //Assert( false );
- //return Node::null();
+ {
+ std::stringstream ss;
+ ss << r;
+ retStr = ss.str();
+ Assert(!isRegExpKind(r.getKind()));
+ break;
+ }
}
}
<< std::endl;
// if so, do simple unrolling
std::vector<Node> nvec;
- if (nvec.empty())
+ Trace("strings-regexp") << "Simplify on " << atom << std::endl;
+ d_regexp_opr.simplify(atom, nvec, polarity);
+ Trace("strings-regexp") << "...finished" << std::endl;
+ // if simplifying successfully generated a lemma
+ if (!nvec.empty())
{
- d_regexp_opr.simplify(atom, nvec, polarity);
- }
- std::vector<Node> exp_n;
- exp_n.push_back(assertion);
- Node conc = nvec.size() == 1 ? nvec[0] : nm->mkNode(AND, nvec);
- d_im.sendInference(rnfexp, exp_n, conc, "REGEXP_Unfold");
- addedLemma = true;
- if (changed)
- {
- cprocessed.push_back(assertion);
+ std::vector<Node> exp_n;
+ exp_n.push_back(assertion);
+ Node conc = nvec.size() == 1 ? nvec[0] : nm->mkNode(AND, nvec);
+ d_im.sendInference(rnfexp, exp_n, conc, "REGEXP_Unfold");
+ addedLemma = true;
+ if (changed)
+ {
+ cprocessed.push_back(assertion);
+ }
+ else
+ {
+ processed.push_back(assertion);
+ }
+ if (e == 0)
+ {
+ // Remember that we have unfolded a membership for x
+ // notice that we only do this here, after we have definitely
+ // added a lemma.
+ repUnfold.insert(rep);
+ }
}
else
{
- processed.push_back(assertion);
- }
- if (e == 0)
- {
- // Remember that we have unfolded a membership for x
- // notice that we only do this here, after we have definitely
- // added a lemma.
- repUnfold.insert(rep);
+ // otherwise we are incomplete
+ d_parent.getOutputChannel().setIncomplete();
}
}
if (d_state.isInConflict())
Assert(m.getKind() == NOT && m[0].getKind() == STRING_IN_REGEXP);
continue;
}
- RegExpConstType rct = d_regexp_opr.getRegExpConstType(m);
+ RegExpConstType rct = d_regexp_opr.getRegExpConstType(m[1]);
if (rct == RE_C_VARIABLE
|| (options::stringRegExpInterMode() == RE_INTER_CONSTANT
&& rct != RE_C_CONRETE_CONSTANT))
{
Trace("strings-error") << "Unsupported term: " << r
<< " in normalization SymRegExp." << std::endl;
- Assert(false);
+ Assert(!RegExpOpr::isRegExpKind(r.getKind()));
}
}
return ret;
projects / cvc5.git / commitdiff