summaryrefslogtreecommitdiff
path: root/src/theory/strings/theory_strings.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/strings/theory_strings.cpp')
-rw-r--r--src/theory/strings/theory_strings.cpp159
1 files changed, 112 insertions, 47 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 7998669cf..3f576d4f5 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -57,6 +57,7 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu
d_regexp_ccached(c),
d_str_re_map(c),
d_inter_cache(c),
+ d_inter_index(c),
d_regexp_ant(c),
d_input_vars(u),
d_input_var_lsum(u),
@@ -1052,6 +1053,37 @@ bool TheoryStrings::processLoop(std::vector< Node > &antec,
NodeManager::currentNM()->mkNode( kind::REGEXP_STAR,
NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, rep_c ) ) );
conc = str_in_re;
+ } else if(t_yz.isConst()) {
+ CVC4::String s = t_yz.getConst< CVC4::String >();
+ unsigned size = s.size();
+ std::vector< Node > vconc;
+ for(unsigned len=1; len<=size; len++) {
+ Node y = NodeManager::currentNM()->mkConst(s.substr(0, len));
+ Node z = NodeManager::currentNM()->mkConst(s.substr(len, size - len));
+ Node restr = s_zy;
+ Node cc;
+ if(r != d_emptyString) {
+ std::vector< Node > v2(vec_r);
+ v2.insert(v2.begin(), y);
+ v2.insert(v2.begin(), z);
+ restr = mkConcat( z, y );
+ cc = Rewriter::rewrite(s_zy.eqNode( mkConcat( v2 ) ));
+ } else {
+ cc = Rewriter::rewrite(s_zy.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, z, y) ));
+ }
+ if(cc == d_false) {
+ continue;
+ }
+ Node conc2 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, normal_forms[other_n_index][other_index],
+ NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT,
+ NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, y),
+ NodeManager::currentNM()->mkNode(kind::REGEXP_STAR,
+ NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, restr))));
+ cc = cc==d_true ? conc2 : NodeManager::currentNM()->mkNode( kind::AND, cc, conc2 );
+ d_regexp_ant[conc2] = ant;
+ vconc.push_back(cc);
+ }
+ conc = vconc.size()==0 ? Node::null() : vconc.size()==1 ? vconc[0] : NodeManager::currentNM()->mkNode(kind::OR, vconc);
} else {
Trace("strings-loop") << "Strings::Loop: Normal Breaking." << std::endl;
//right
@@ -1082,9 +1114,9 @@ bool TheoryStrings::processLoop(std::vector< Node > &antec,
} // normal case
//set its antecedant to ant, to say when it is relevant
- d_regexp_ant[str_in_re] = ant;
- //unroll the str in re constraint once
- // unrollStar( str_in_re );
+ if(!str_in_re.isNull()) {
+ d_regexp_ant[str_in_re] = ant;
+ }
sendLemma( ant, conc, "LOOP-BREAK" );
++(d_statistics.d_loop_lemmas);
@@ -2304,31 +2336,57 @@ bool TheoryStrings::checkMemberships() {
if(options::stringEIT()) {
for(NodeListMap::const_iterator itr_xr = d_str_re_map.begin();
itr_xr != d_str_re_map.end(); ++itr_xr ) {
+ bool spflag = false;
+ Node x = (*itr_xr).first;
NodeList* lst = (*itr_xr).second;
- if(lst->size() > 1) {
- Node r = (*lst)[0];
- NodeList::const_iterator itr_lst = lst->begin();
- ++itr_lst;
- for(;itr_lst != lst->end(); ++itr_lst) {
- Node r2 = *itr_lst;
- r = d_regexp_opr.intersect(r, r2);
- if(r == d_emptyRegexp) {
- std::vector< Node > vec_nodes;
- Node x = (*itr_xr).first;
+ if(d_inter_index.find(x) == d_inter_index.end()) {
+ d_inter_index[x] = 0;
+ }
+ int cur_inter_idx = d_inter_index[x];
+ if(cur_inter_idx != (int)lst->size()) {
+ if(lst->size() == 1) {
+ d_inter_cache[x] = (*lst)[0];
+ d_inter_index[x] = 1;
+ } else if(lst->size() > 1) {
+ Node r;
+ if(d_inter_cache.find(x) != d_inter_cache.end()) {
+ r = d_inter_cache[x];
+ }
+ if(r.isNull()) {
+ r = (*lst)[0];
+ cur_inter_idx = 1;
+ }
+ NodeList::const_iterator itr_lst = lst->begin();
+ for(int i=0; i<cur_inter_idx; i++) {
++itr_lst;
- for(NodeList::const_iterator itr2 = lst->begin();
- itr2 != itr_lst; ++itr2) {
- Node n = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, x, *itr2);
- vec_nodes.push_back( n );
+ }
+ for(;itr_lst != lst->end(); ++itr_lst) {
+ Node r2 = *itr_lst;
+ r = d_regexp_opr.intersect(r, r2, spflag);
+ if(spflag) {
+ break;
+ } else if(r == d_emptyRegexp) {
+ std::vector< Node > vec_nodes;
+ ++itr_lst;
+ for(NodeList::const_iterator itr2 = lst->begin();
+ itr2 != itr_lst; ++itr2) {
+ Node n = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, x, *itr2);
+ vec_nodes.push_back( n );
+ }
+ Node antec = vec_nodes.size() == 1? vec_nodes[0] : NodeManager::currentNM()->mkNode(kind::AND, vec_nodes);
+ Node conc;
+ sendLemma(antec, conc, "INTERSEC CONFLICT");
+ addedLemma = true;
+ break;
+ }
+ if(d_conflict) {
+ break;
}
- Node antec = vec_nodes.size() == 1? vec_nodes[0] : NodeManager::currentNM()->mkNode(kind::AND, vec_nodes);
- Node conc;
- sendLemma(antec, conc, "INTERSEC CONFLICT");
- addedLemma = true;
- break;
}
- if(d_conflict) {
- break;
+ //updates
+ if(!d_conflict && !spflag) {
+ d_inter_cache[x] = r;
+ d_inter_index[x] = (int)lst->size();
}
}
}
@@ -2515,16 +2573,30 @@ bool TheoryStrings::checkPDerivative(Node x, Node r, Node atom, bool &addedLemma
}
}*/
if(areEqual(x, d_emptyString)) {
- int rdel = d_regexp_opr.delta(r);
- if(rdel == 1) {
- d_regexp_ccached.insert(atom);
- } else if(rdel == 2) {
- Node antec = mkRegExpAntec(atom, x.eqNode(d_emptyString));
- Node conc = Node::null();
- sendLemma(antec, conc, "RegExp Delta CONFLICT");
- addedLemma = true;
- d_regexp_ccached.insert(atom);
- return false;
+ Node exp;
+ switch(d_regexp_opr.delta(r, exp)) {
+ case 0: {
+ Node antec = mkRegExpAntec(atom, x.eqNode(d_emptyString));
+ sendLemma(antec, exp, "RegExp Delta");
+ addedLemma = true;
+ d_regexp_ccached.insert(atom);
+ return false;
+ }
+ case 1: {
+ d_regexp_ccached.insert(atom);
+ break;
+ }
+ case 2: {
+ Node antec = mkRegExpAntec(atom, x.eqNode(d_emptyString));
+ Node conc = Node::null();
+ sendLemma(antec, conc, "RegExp Delta CONFLICT");
+ addedLemma = true;
+ d_regexp_ccached.insert(atom);
+ return false;
+ }
+ default:
+ //Impossible
+ break;
}
} else {
Node xr = getRepresentative( x );
@@ -2720,7 +2792,7 @@ bool TheoryStrings::addMembershipLength(Node atom) {
bool TheoryStrings::splitRegExp( Node x, Node r, Node ant ) {
// TODO cstr in vre
Assert(x != d_emptyString);
- Trace("strings-regexp-split") << "TheoryStrings::splitRegExp: x=" << x << ", r= " << r << std::endl;
+ Trace("regexp-split") << "TheoryStrings::splitRegExp: x=" << x << ", r= " << r << std::endl;
//if(x.isConst()) {
// Node n = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, x, r );
// Node r = Rewriter::rewrite( n );
@@ -2736,8 +2808,11 @@ bool TheoryStrings::splitRegExp( Node x, Node r, Node ant ) {
bool flag = true;
for(unsigned i=0; i<s.size(); ++i) {
CVC4::String c = s.substr(i, 1);
- dc = d_regexp_opr.derivativeSingle(dc, c);
- if(dc == d_emptyRegexp) {
+ Node dc2;
+ int rt = d_regexp_opr.derivativeS(dc, c, dc2);
+ if(rt == 0) {
+ //TODO
+ } else if(rt == 2) {
// CONFLICT
flag = false;
break;
@@ -2799,16 +2874,6 @@ void TheoryStrings::addMembership(Node assertion) {
}
}
lst->push_back( r );
- //TODO: make it smarter
- /*
- unsigned size = lst->size();
- if(size == 1) {
- d_inter_cache[x] = r;
- } else {
- Node r1 = (*lst)[size - 2];
- Node rr = d_regexp_opr.intersect(r1, r);
- d_inter_cache[x] = rr;
- }*/
}
}
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback