diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-07-02 16:47:50 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-07-02 16:47:50 -0500 |
commit | 032bfdd23c387d1ce37e89b13a619cc65c85c2c3 (patch) | |
tree | 529b067adcf88a76eb862e4d481fe8fe848d8b4d /src/theory/strings/regexp_operation.cpp | |
parent | 8af18dcba80cdf0d995f1cfd5390a1784a27a7c1 (diff) |
Remove some dead code from theory strings (#2125)
Diffstat (limited to 'src/theory/strings/regexp_operation.cpp')
-rw-r--r-- | src/theory/strings/regexp_operation.cpp | 612 |
1 files changed, 0 insertions, 612 deletions
diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index 0eccc72c7..e130d5e4b 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -634,76 +634,6 @@ Node RegExpOpr::derivativeSingle( Node r, CVC4::String c ) { 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); @@ -809,124 +739,6 @@ void RegExpOpr::firstChars( Node r, std::set<unsigned char> &pcset, SetNodes &pv } } -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; @@ -1297,99 +1109,6 @@ void RegExpOpr::simplifyPRegExp( Node s, Node r, std::vector< Node > &new_nodes } } -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) { @@ -1734,337 +1453,6 @@ Node RegExpOpr::intersect(Node r1, Node r2, bool &spflag) { } } -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()) { |