return retNode;
}
-//TODO:
-bool RegExpOpr::guessLength( Node r, int &co ) {
- int k = r.getKind();
- switch( k ) {
- case kind::STRING_TO_REGEXP:
- {
- if(r[0].isConst()) {
- co += r[0].getConst< CVC4::String >().size();
- return true;
- } else {
- return false;
- }
- }
- break;
- case kind::REGEXP_CONCAT:
- {
- for(unsigned i=0; i<r.getNumChildren(); ++i) {
- if(!guessLength( r[i], co)) {
- return false;
- }
- }
- return true;
- }
- break;
- case kind::REGEXP_UNION:
- {
- int g_co;
- for(unsigned i=0; i<r.getNumChildren(); ++i) {
- int cop = 0;
- if(!guessLength( r[i], cop)) {
- return false;
- }
- if(i == 0) {
- g_co = cop;
- } else {
- g_co = gcd(g_co, cop);
- }
- }
- return true;
- }
- break;
- case kind::REGEXP_INTER:
- {
- int g_co;
- for(unsigned i=0; i<r.getNumChildren(); ++i) {
- int cop = 0;
- if(!guessLength( r[i], cop)) {
- return false;
- }
- if(i == 0) {
- g_co = cop;
- } else {
- g_co = gcd(g_co, cop);
- }
- }
- return true;
- }
- break;
- case kind::REGEXP_STAR:
- {
- co = 0;
- return true;
- }
- break;
- default:
- Trace("strings-error") << "Unsupported term: " << mkString( r ) << " in membership of RegExp." << std::endl;
- return false;
- }
-}
-
void RegExpOpr::firstChars( Node r, std::set<unsigned char> &pcset, SetNodes &pvset ) {
Trace("regexp-fset") << "Start FSET(" << mkString(r) << ")" << std::endl;
std::map< Node, std::pair< std::set<unsigned char>, SetNodes > >::const_iterator itr = d_fset_cache.find(r);
}
}
-bool RegExpOpr::follow( Node r, CVC4::String c, std::vector< unsigned char > &vec_chars ) {
- int k = r.getKind();
- switch( k ) {
- case kind::STRING_TO_REGEXP:
- {
- if(r[0].isConst()) {
- if(r[0] != d_emptyString) {
- unsigned char t1 = r[0].getConst< CVC4::String >().getFirstChar();
- if(c.isEmptyString()) {
- vec_chars.push_back( t1 );
- return true;
- } else {
- unsigned char t2 = c.getFirstChar();
- if(t1 != t2) {
- return false;
- } else {
- if(c.size() >= 2) {
- vec_chars.push_back( c.substr(1,1).getFirstChar() );
- } else {
- vec_chars.push_back( '\0' );
- }
- return true;
- }
- }
- } else {
- return false;
- }
- } else {
- return false;
- }
- }
- break;
- case kind::REGEXP_CONCAT:
- {
- for(unsigned i=0; i<r.getNumChildren(); ++i) {
- if( follow(r[i], c, vec_chars) ) {
- if(vec_chars[vec_chars.size() - 1] == '\0') {
- vec_chars.pop_back();
- c = d_emptyString.getConst< CVC4::String >();
- }
- } else {
- return false;
- }
- }
- vec_chars.push_back( '\0' );
- return true;
- }
- break;
- case kind::REGEXP_UNION:
- {
- bool flag = false;
- for(unsigned i=0; i<r.getNumChildren(); ++i) {
- if( follow(r[i], c, vec_chars) ) {
- flag=true;
- }
- }
- return flag;
- }
- break;
- case kind::REGEXP_INTER:
- {
- std::vector< unsigned char > vt2;
- for(unsigned i=0; i<r.getNumChildren(); ++i) {
- std::vector< unsigned char > v_tmp;
- if( !follow(r[i], c, v_tmp) ) {
- return false;
- }
- std::vector< unsigned char > vt3(vt2);
- vt2.clear();
- std::set_intersection( vt3.begin(), vt3.end(), v_tmp.begin(), v_tmp.end(), vt2.begin() );
- if(vt2.size() == 0) {
- return false;
- }
- }
- vec_chars.insert( vec_chars.end(), vt2.begin(), vt2.end() );
- return true;
- }
- break;
- case kind::REGEXP_STAR:
- {
- if(follow(r[0], c, vec_chars)) {
- if(vec_chars[vec_chars.size() - 1] == '\0') {
- if(c.isEmptyString()) {
- return true;
- } else {
- vec_chars.pop_back();
- c = d_emptyString.getConst< CVC4::String >();
- return follow(r[0], c, vec_chars);
- }
- } else {
- return true;
- }
- } else {
- vec_chars.push_back( '\0' );
- return true;
- }
- }
- break;
- default: {
- Trace("strings-error") << "Unsupported term: " << mkString( r ) << " in follow of RegExp." << std::endl;
- //AlwaysAssert( false );
- //return Node::null();
- return false;
- }
- }
-}
-
-Node RegExpOpr::mkAllExceptOne( unsigned char exp_c ) {
- std::vector< Node > vec_nodes;
- for(unsigned char c=d_char_start; c<=d_char_end; ++c) {
- if(c != exp_c ) {
- Node n = NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst( ::CVC4::String( c ) ) );
- vec_nodes.push_back( n );
- }
- }
- return NodeManager::currentNM()->mkNode( kind::REGEXP_UNION, vec_nodes );
-}
-
//simplify
void RegExpOpr::simplify(Node t, std::vector< Node > &new_nodes, bool polarity) {
Trace("strings-regexp-simpl") << "RegExp-Simpl starts with " << t << ", polarity=" << polarity << std::endl;
}
}
-void RegExpOpr::getCharSet( Node r, std::set<unsigned char> &pcset, SetNodes &pvset ) {
- std::map< Node, std::pair< std::set<unsigned char>, SetNodes > >::const_iterator itr = d_cset_cache.find(r);
- if(itr != d_cset_cache.end()) {
- pcset.insert((itr->second).first.begin(), (itr->second).first.end());
- pvset.insert((itr->second).second.begin(), (itr->second).second.end());
- } else {
- std::set<unsigned char> cset;
- SetNodes vset;
- int k = r.getKind();
- switch( k ) {
- case kind::REGEXP_EMPTY: {
- break;
- }
- case kind::REGEXP_SIGMA: {
- for(unsigned char i='\0'; i<=d_lastchar; i++) {
- cset.insert(i);
- }
- break;
- }
- case kind::REGEXP_RANGE: {
- unsigned char a = r[0].getConst<String>().getFirstChar();
- unsigned char b = r[1].getConst<String>().getFirstChar();
- for(unsigned char i=a; i<=b; i++) {
- cset.insert(i);
- }
- break;
- }
- case kind::STRING_TO_REGEXP: {
- Node st = Rewriter::rewrite(r[0]);
- if(st.isConst()) {
- CVC4::String s = st.getConst< CVC4::String >();
- cset.insert(s.getVec().begin(), s.getVec().end());
- } else if(st.getKind() == kind::VARIABLE) {
- vset.insert( st );
- } else {
- for(unsigned i=0; i<st.getNumChildren(); i++) {
- if(st[i].isConst()) {
- CVC4::String s = st[i].getConst< CVC4::String >();
- cset.insert(s.getVec().begin(), s.getVec().end());
- } else {
- vset.insert( st[i] );
- }
- }
- }
- break;
- }
- case kind::REGEXP_CONCAT: {
- for(unsigned i=0; i<r.getNumChildren(); i++) {
- getCharSet(r[i], cset, vset);
- }
- break;
- }
- case kind::REGEXP_UNION: {
- for(unsigned i=0; i<r.getNumChildren(); i++) {
- getCharSet(r[i], cset, vset);
- }
- break;
- }
- case kind::REGEXP_INTER: {
- //TODO: Overapproximation for now
- //for(unsigned i=0; i<r.getNumChildren(); i++) {
- //getCharSet(r[i], cset, vset);
- //}
- getCharSet(r[0], cset, vset);
- break;
- }
- case kind::REGEXP_STAR: {
- getCharSet(r[0], cset, vset);
- break;
- }
- case kind::REGEXP_LOOP: {
- getCharSet(r[0], cset, vset);
- break;
- }
- default: {
- //Trace("strings-error") << "Unsupported term: " << r << " in getCharSet." << std::endl;
- Unreachable();
- }
- }
- pcset.insert(cset.begin(), cset.end());
- pvset.insert(vset.begin(), vset.end());
- std::pair< std::set<unsigned char>, SetNodes > p(cset, vset);
- d_cset_cache[r] = p;
-
- Trace("regexp-cset") << "CSET( " << mkString(r) << " ) = { ";
- for(std::set<unsigned char>::const_iterator itr = cset.begin();
- itr != cset.end(); itr++) {
- Trace("regexp-cset") << (*itr) << ",";
- }
- Trace("regexp-cset") << " }" << std::endl;
- }
-}
-
bool RegExpOpr::isPairNodesInSet(std::set< PairNodes > &s, Node n1, Node n2) {
for(std::set< PairNodes >::const_iterator itr = s.begin();
itr != s.end(); ++itr) {
}
}
-Node RegExpOpr::complement(Node r, int &ret) {
- Node rNode;
- ret = 1;
- if(d_compl_cache.find(r) != d_compl_cache.end()) {
- rNode = d_compl_cache[r].first;
- ret = d_compl_cache[r].second;
- } else {
- if(r == d_emptyRegexp) {
- rNode = d_sigma_star;
- } else if(r == d_emptySingleton) {
- rNode = NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, d_sigma, d_sigma_star);
- } else if(!checkConstRegExp(r)) {
- //TODO: var to be extended
- ret = 0;
- } else {
- std::set<unsigned char> cset;
- SetNodes vset;
- firstChars(r, cset, vset);
- std::vector< Node > vec_nodes;
- for(unsigned char i=0; i<=d_lastchar; i++) {
- CVC4::String c(i);
- Node n = NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst(c));
- Node r2;
- if(cset.find(i) == cset.end()) {
- r2 = d_sigma_star;
- } else {
- int rt;
- derivativeS(r, c, r2);
- if(r2 == r) {
- r2 = d_emptyRegexp;
- } else {
- r2 = complement(r2, rt);
- }
- }
- n = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, n, r2));
- vec_nodes.push_back(n);
- }
- rNode = vec_nodes.size()==0? d_emptyRegexp : vec_nodes.size()==1? vec_nodes[0] :
- NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, vec_nodes);
- }
- rNode = Rewriter::rewrite(rNode);
- std::pair< Node, int > p(rNode, ret);
- d_compl_cache[r] = p;
- }
- Trace("regexp-compl") << "COMPL( " << mkString(r) << " ) = " << mkString(rNode) << ", ret=" << ret << std::endl;
- return rNode;
-}
-
-void RegExpOpr::splitRegExp(Node r, std::vector< PairNodes > &pset) {
- Assert(checkConstRegExp(r));
- if(d_split_cache.find(r) != d_split_cache.end()) {
- pset = d_split_cache[r];
- } else {
- switch( r.getKind() ) {
- case kind::REGEXP_EMPTY: {
- break;
- }
- case kind::REGEXP_OPT: {
- PairNodes tmp(d_emptySingleton, d_emptySingleton);
- pset.push_back(tmp);
- }
- case kind::REGEXP_RANGE:
- case kind::REGEXP_SIGMA: {
- PairNodes tmp1(d_emptySingleton, r);
- PairNodes tmp2(r, d_emptySingleton);
- pset.push_back(tmp1);
- pset.push_back(tmp2);
- break;
- }
- case kind::STRING_TO_REGEXP: {
- Assert(r[0].isConst());
- CVC4::String s = r[0].getConst< CVC4::String >();
- PairNodes tmp1(d_emptySingleton, r);
- pset.push_back(tmp1);
- for(unsigned i=1; i<s.size(); i++) {
- CVC4::String s1 = s.substr(0, i);
- CVC4::String s2 = s.substr(i);
- Node n1 = NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst(s1));
- Node n2 = NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst(s2));
- PairNodes tmp3(n1, n2);
- pset.push_back(tmp3);
- }
- PairNodes tmp2(r, d_emptySingleton);
- pset.push_back(tmp2);
- break;
- }
- case kind::REGEXP_CONCAT: {
- for(unsigned i=0; i<r.getNumChildren(); i++) {
- std::vector< PairNodes > tset;
- splitRegExp(r[i], tset);
- std::vector< Node > hvec;
- std::vector< Node > tvec;
- for(unsigned j=0; j<=i; j++) {
- hvec.push_back(r[j]);
- }
- for(unsigned j=i; j<r.getNumChildren(); j++) {
- tvec.push_back(r[j]);
- }
- for(unsigned j=0; j<tset.size(); j++) {
- hvec[i] = tset[j].first;
- tvec[0] = tset[j].second;
- Node r1 = Rewriter::rewrite( hvec.size()==1?hvec[0]:NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, hvec) );
- Node r2 = Rewriter::rewrite( tvec.size()==1?tvec[0]:NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, tvec) );
- PairNodes tmp2(r1, r2);
- pset.push_back(tmp2);
- }
- }
- break;
- }
- case kind::REGEXP_UNION: {
- for(unsigned i=0; i<r.getNumChildren(); ++i) {
- std::vector< PairNodes > tset;
- splitRegExp(r[i], tset);
- pset.insert(pset.end(), tset.begin(), tset.end());
- }
- break;
- }
- case kind::REGEXP_INTER: {
- bool spflag = false;
- Node tmp = r[0];
- for(unsigned i=1; i<r.getNumChildren(); i++) {
- tmp = intersect(tmp, r[i], spflag);
- }
- splitRegExp(tmp, pset);
- break;
- }
- case kind::REGEXP_STAR: {
- std::vector< PairNodes > tset;
- splitRegExp(r[0], tset);
- PairNodes tmp1(d_emptySingleton, d_emptySingleton);
- pset.push_back(tmp1);
- for(unsigned i=0; i<tset.size(); i++) {
- Node r1 = tset[i].first==d_emptySingleton ? r : NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, r, tset[i].first);
- Node r2 = tset[i].second==d_emptySingleton ? r : NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, tset[i].second, r);
- PairNodes tmp2(r1, r2);
- pset.push_back(tmp2);
- }
- break;
- }
- case kind::REGEXP_LOOP: {
- unsigned l = r[1].getConst<Rational>().getNumerator().toUnsignedInt();
- unsigned u = r[2].getConst<Rational>().getNumerator().toUnsignedInt();
- if(l == u) {
- //R^n
- if(l == 0) {
- PairNodes tmp1(d_emptySingleton, d_emptySingleton);
- pset.push_back(tmp1);
- } else if(l == 1) {
- splitRegExp(r[0], pset);
- } else {
- std::vector< PairNodes > tset;
- splitRegExp(r[0], tset);
- for(unsigned j=0; j<l; j++) {
- Node num1 = NodeManager::currentNM()->mkConst(CVC4::Rational(j));
- Node r1 = j==0? d_emptySingleton : j==1? r[0] : NodeManager::currentNM()->mkNode(kind::REGEXP_LOOP, r[0], num1, num1);
- unsigned j2 = l - j - 1;
- Node num2 = NodeManager::currentNM()->mkConst(CVC4::Rational(j2));
- Node r2 = j2==0? d_emptySingleton : j2==1? r[0] : NodeManager::currentNM()->mkNode(kind::REGEXP_LOOP, r[0], num2, num2);
- for(unsigned i=0; i<tset.size(); i++) {
- r1 = tset[i].first==d_emptySingleton? r1 : NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, r1, tset[i].first);
- r2 = tset[i].second==d_emptySingleton? r2 : NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, tset[i].second, r2);
- PairNodes tmp2(r1, r2);
- pset.push_back(tmp2);
- }
- }
- }
- } else {
- //R{0,n}
- PairNodes tmp1(d_emptySingleton, d_emptySingleton);
- pset.push_back(tmp1);
- std::vector< PairNodes > tset;
- splitRegExp(r[0], tset);
- pset.insert(pset.end(), tset.begin(), tset.end());
- for(unsigned k=2; k<=u; k++) {
- for(unsigned j=0; j<k; j++) {
- Node num1 = NodeManager::currentNM()->mkConst(CVC4::Rational(j));
- Node r1 = j==0? d_emptySingleton : j==1? r[0] : NodeManager::currentNM()->mkNode(kind::REGEXP_LOOP, r[0], num1, num1);
- unsigned j2 = k - j - 1;
- Node num2 = NodeManager::currentNM()->mkConst(CVC4::Rational(j2));
- Node r2 = j2==0? d_emptySingleton : j2==1? r[0] : NodeManager::currentNM()->mkNode(kind::REGEXP_LOOP, r[0], num2, num2);
- for(unsigned i=0; i<tset.size(); i++) {
- r1 = tset[i].first==d_emptySingleton? r1 : NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, r1, tset[i].first);
- r2 = tset[i].second==d_emptySingleton? r2 : NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, tset[i].second, r2);
- PairNodes tmp2(r1, r2);
- pset.push_back(tmp2);
- }
- }
- }
- }
- break;
- }
- case kind::REGEXP_PLUS: {
- std::vector< PairNodes > tset;
- splitRegExp(r[0], tset);
- for(unsigned i=0; i<tset.size(); i++) {
- Node r1 = NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, r, tset[i].first);
- Node r2 = NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, tset[i].second, r);
- PairNodes tmp2(r1, r2);
- pset.push_back(tmp2);
- }
- break;
- }
- default: {
- Trace("strings-error") << "Unsupported term: " << r << " in splitRegExp." << std::endl;
- Assert( false );
- //return Node::null();
- }
- }
- d_split_cache[r] = pset;
- }
-}
-
-void RegExpOpr::flattenRegExp(Node r, std::vector< std::pair< CVC4::String, unsigned > > &fvec) {
- Assert(false);
- Assert(checkConstRegExp(r));
- switch( r.getKind() ) {
- case kind::REGEXP_EMPTY: {
- //TODO
- break;
- }
- case kind::REGEXP_SIGMA: {
- CVC4::String s("a");
- std::pair< CVC4::String, unsigned > tmp(s, 0);
- //TODO
- break;
- }
- case kind::STRING_TO_REGEXP: {
- Assert(r[0].isConst());
- CVC4::String s = r[0].getConst< CVC4::String >();
- std::pair< CVC4::String, unsigned > tmp(s, 0);
- //TODO
- break;
- }
- case kind::REGEXP_CONCAT: {
- for(unsigned i=0; i<r.getNumChildren(); i++) {
- //TODO
- }
- break;
- }
- case kind::REGEXP_UNION: {
- for(unsigned i=0; i<r.getNumChildren(); ++i) {
- //TODO
- }
- break;
- }
- case kind::REGEXP_INTER: {
- //TODO
- break;
- }
- case kind::REGEXP_STAR: {
- //TODO
- break;
- }
- case kind::REGEXP_LOOP: {
- //TODO
- break;
- }
- default: {
- Unreachable();
- }
- }
-}
-
-void RegExpOpr::disjunctRegExp(Node r, std::vector<Node> &vec_or) {
- switch(r.getKind()) {
- case kind::REGEXP_EMPTY: {
- vec_or.push_back(r);
- break;
- }
- case kind::REGEXP_SIGMA: {
- vec_or.push_back(r);
- break;
- }
- case kind::REGEXP_RANGE: {
- vec_or.push_back(r);
- break;
- }
- case kind::STRING_TO_REGEXP: {
- vec_or.push_back(r);
- break;
- }
- case kind::REGEXP_CONCAT: {
- disjunctRegExp(r[0], vec_or);
- for(unsigned i=1; i<r.getNumChildren(); i++) {
- std::vector<Node> vec_con;
- disjunctRegExp(r[i], vec_con);
- std::vector<Node> vec_or2;
- for(unsigned k1=0; k1<vec_or.size(); k1++) {
- for(unsigned k2=0; k2<vec_con.size(); k2++) {
- Node tmp = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, vec_or[k1], vec_con[k2]) );
- if(std::find(vec_or2.begin(), vec_or2.end(), tmp) == vec_or2.end()) {
- vec_or2.push_back( tmp );
- }
- }
- }
- vec_or = vec_or2;
- }
- break;
- }
- case kind::REGEXP_UNION: {
- for(unsigned i=0; i<r.getNumChildren(); ++i) {
- std::vector<Node> vec_or2;
- disjunctRegExp(r[i], vec_or2);
- vec_or.insert(vec_or.end(), vec_or2.begin(), vec_or2.end());
- }
- break;
- }
- case kind::REGEXP_INTER: {
- Assert(checkConstRegExp(r));
- Node rtmp = r[0];
- bool spflag = false;
- for(unsigned i=1; i<r.getNumChildren(); ++i) {
- rtmp = intersect(rtmp, r[i], spflag);
- }
- disjunctRegExp(rtmp, vec_or);
- break;
- }
- case kind::REGEXP_STAR: {
- vec_or.push_back(r);
- break;
- }
- case kind::REGEXP_LOOP: {
- vec_or.push_back(r);
- break;
- }
- default: {
- Unreachable();
- }
- }
-}
-
//printing
std::string RegExpOpr::niceChar(Node r) {
if(r.isConst()) {
Assert( nr.isNull() );
if( ret!=0 ){
getExtTheory()->markReduced( extf[i] );
- if( options::stringOpt1() && hasProcessed() ){
+ if (hasProcessed())
+ {
return;
}
}
}
}
-bool TheoryStrings::applyRConsume( CVC4::String &s, Node &r) {
- Trace("regexp-derivative") << "TheoryStrings::derivative: s=" << s << ", r= " << r << std::endl;
- Assert( d_regexp_opr.checkConstRegExp(r) );
-
- if( !s.isEmptyString() ) {
- Node dc = r;
-
- for(unsigned i=0; i<s.size(); ++i) {
- CVC4::String c = s.substr(i, 1);
- Node dc2;
- int rt = d_regexp_opr.derivativeS(dc, c, dc2);
- dc = dc2;
- if(rt == 0) {
- Unreachable();
- } else if(rt == 2) {
- return false;
- }
- }
- r = dc;
- }
-
- return true;
-}
-
-Node TheoryStrings::applyRSplit(Node s1, Node s2, Node r) {
- Assert(d_regexp_opr.checkConstRegExp(r));
-
- std::vector< std::pair< Node, Node > > vec_can;
- d_regexp_opr.splitRegExp(r, vec_can);
- //TODO: lazy cache or eager?
- std::vector< Node > vec_or;
-
- for(unsigned int i=0; i<vec_can.size(); i++) {
- Node m1 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s1, vec_can[i].first);
- Node m2 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s2, vec_can[i].second);
- Node c = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::AND, m1, m2) );
- vec_or.push_back( c );
- }
- Node conc = vec_or.size()==0? Node::null() : vec_or.size()==1 ? vec_or[0] : Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::OR, vec_or) );
- return conc;
-}
-
-bool TheoryStrings::applyRLen(std::map< Node, std::vector< Node > > &XinR_with_exps) {
- if(XinR_with_exps.size() > 0) {
- //TODO: get vector, var, store.
- return true;
- } else {
- return false;
- }
-}
-
void TheoryStrings::checkMemberships() {
//add the memberships
std::vector<Node> mems = getExtTheory()->getActive(kind::STRING_IN_REGEXP);
Trace("regexp-debug") << "... No Intersect Conflict in Memberships, addedLemma: " << addedLemma << std::endl;
if(!addedLemma) {
+ NodeManager* nm = NodeManager::currentNM();
for( unsigned i=0; i<d_regexp_memberships.size(); i++ ) {
//check regular expression membership
Node assertion = d_regexp_memberships[i];
Node r = atom[1];
std::vector< Node > rnfexp;
- //if(options::stringOpt1()) {
- if(true){
- if(!x.isConst()) {
- x = getNormalString( x, rnfexp);
- changed = true;
+ if (!x.isConst())
+ {
+ x = getNormalString(x, rnfexp);
+ changed = true;
+ }
+ if (!d_regexp_opr.checkConstRegExp(r))
+ {
+ r = getNormalSymRegExp(r, rnfexp);
+ changed = true;
+ }
+ Trace("strings-regexp-nf") << "Term " << atom << " is normalized to "
+ << x << " IN " << r << std::endl;
+ if (changed)
+ {
+ Node tmp =
+ Rewriter::rewrite(nm->mkNode(kind::STRING_IN_REGEXP, x, r));
+ if (!polarity)
+ {
+ tmp = tmp.negate();
}
- if(!d_regexp_opr.checkConstRegExp(r)) {
- r = getNormalSymRegExp(r, rnfexp);
- changed = true;
+ if (tmp == d_true)
+ {
+ d_regexp_ccached.insert(assertion);
+ continue;
}
- Trace("strings-regexp-nf") << "Term " << atom << " is normalized to " << x << " IN " << r << std::endl;
- if(changed) {
- Node tmp = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, x, r) );
- if(!polarity) {
- tmp = tmp.negate();
- }
- if(tmp == d_true) {
- d_regexp_ccached.insert(assertion);
- continue;
- } else if(tmp == d_false) {
- Node antec = mkRegExpAntec(assertion, mkExplain(rnfexp));
- Node conc = Node::null();
- sendLemma(antec, conc, "REGEXP NF Conflict");
- addedLemma = true;
- break;
- }
+ else if (tmp == d_false)
+ {
+ Node antec = mkRegExpAntec(assertion, mkExplain(rnfexp));
+ Node conc = Node::null();
+ sendLemma(antec, conc, "REGEXP NF Conflict");
+ addedLemma = true;
+ break;
}
}
if( polarity ) {
flag = checkPDerivative(x, r, atom, addedLemma, rnfexp);
- if(options::stringOpt2() && flag) {
- if(d_regexp_opr.checkConstRegExp(r) && x.getKind()==kind::STRING_CONCAT) {
- std::vector< std::pair< Node, Node > > vec_can;
- d_regexp_opr.splitRegExp(r, vec_can);
- //TODO: lazy cache or eager?
- std::vector< Node > vec_or;
- std::vector< Node > vec_s2;
- for(unsigned int s2i=1; s2i<x.getNumChildren(); s2i++) {
- vec_s2.push_back(x[s2i]);
- }
- Node s1 = x[0];
- Node s2 = mkConcat(vec_s2);
- for(unsigned int i=0; i<vec_can.size(); i++) {
- Node m1 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s1, vec_can[i].first);
- Node m2 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s2, vec_can[i].second);
- Node c = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::AND, m1, m2) );
- vec_or.push_back( c );
- }
- Node conc = vec_or.size()==1 ? vec_or[0] : Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::OR, vec_or) );
- //Trace("regexp-split") << "R " << r << " to " << conc << std::endl;
- Node antec = mkRegExpAntec(atom, mkExplain(rnfexp));
- if(conc == d_true) {
- if(changed) {
- cprocessed.push_back( assertion );
- } else {
- processed.push_back( assertion );
- }
- } else {
- sendLemma(antec, conc, "RegExp-CST-SP");
- }
- addedLemma = true;
- flag = false;
- }
- }
} else {
if(! options::stringExp()) {
throw LogicException("Strings Incomplete (due to Negative Membership) by default, try --strings-exp option.");
projects / cvc5.git / commitdiff