diff options
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/strings/theory_strings_preprocess.cpp | 44 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings_preprocess.h | 1 |
2 files changed, 28 insertions, 17 deletions
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index f303fd333..64425ea03 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -58,16 +58,6 @@ void StringsPreprocess::simplifyRegExp( Node s, Node r, std::vector< Node > &ret simplifyRegExp( s, r[i], ret ); } break; - case kind::REGEXP_STAR: - { - Node sk = NodeManager::currentNM()->mkSkolem( "ressym_$$", s.getType(), "created for regular expression star" ); - Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, - NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk, s ), - NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, s, sk )); - ret.push_back( eq ); - simplifyRegExp( sk, r[0], ret ); - } - break; case kind::REGEXP_OPT: { Node eq_empty = NodeManager::currentNM()->mkNode( kind::EQUAL, s, NodeManager::currentNM()->mkConst( ::CVC4::String("") ) ); @@ -77,13 +67,27 @@ void StringsPreprocess::simplifyRegExp( Node s, Node r, std::vector< Node > &ret ret.push_back( NodeManager::currentNM()->mkNode( kind::OR, eq_empty, nrr) ); } break; + //TODO: + case kind::REGEXP_STAR: + case kind::REGEXP_PLUS: + Assert( false ); + break; default: - //TODO:case kind::REGEXP_PLUS: //TODO: special sym: sigma, none, all break; } } +bool StringsPreprocess::checkStarPlus( Node t ) { + if( t.getKind() != kind::REGEXP_STAR && t.getKind() != kind::REGEXP_PLUS ) { + for( unsigned i = 0; i<t.getNumChildren(); ++i ) { + if( checkStarPlus(t[i]) ) return true; + } + return false; + } else { + return true; + } +} Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { std::hash_map<TNode, Node, TNodeHashFunction>::const_iterator i = d_cache.find(t); @@ -94,13 +98,19 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { if( t.getKind() == kind::STRING_IN_REGEXP ){ // t0 in t1 Node t0 = simplify( t[0], new_nodes ); - //rewrite it - std::vector< Node > ret; - simplifyRegExp( t0, t[1], ret ); + + if(!checkStarPlus( t[1] )) { + //rewrite it + std::vector< Node > ret; + simplifyRegExp( t0, t[1], ret ); - Node n = ret.size() == 1 ? ret[0] : NodeManager::currentNM()->mkNode( kind::AND, ret ); - d_cache[t] = (t == n) ? Node::null() : n; - return n; + Node n = ret.size() == 1 ? ret[0] : NodeManager::currentNM()->mkNode( kind::AND, ret ); + d_cache[t] = (t == n) ? Node::null() : n; + return n; + } else { + // TODO + return (t0 == t[0]) ? t : NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, t0, t[1] ); + } }else if( t.getKind() == kind::STRING_SUBSTR ){ Node sk1 = NodeManager::currentNM()->mkSkolem( "st1sym_$$", t.getType(), "created for substr" ); Node sk2 = NodeManager::currentNM()->mkSkolem( "st2sym_$$", t.getType(), "created for substr" ); diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h index d07249a02..ce00a75ce 100644 --- a/src/theory/strings/theory_strings_preprocess.h +++ b/src/theory/strings/theory_strings_preprocess.h @@ -31,6 +31,7 @@ class StringsPreprocess { // NOTE: this class is NOT context-dependent std::hash_map<TNode, Node, TNodeHashFunction> d_cache; private: + bool checkStarPlus( Node t ); void simplifyRegExp( Node s, Node r, std::vector< Node > &ret ); Node simplify( Node t, std::vector< Node > &new_nodes ); public: |