adds native regexp.

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index f303fd33368888c02789323004abcdb5ec04a55b..64425ea03567d139487e4b0a7c398948cc7e3f89 100644 (file)
--- 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 d07249a02a0edd3418cd3e6fd7d9c0e756862191..ce00a75ce7512f2a1360b32b2fb1682b884fdd9a 100644 (file)
--- 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:

diff --git a/src/util/regexp.h b/src/util/regexp.h
index 58f58a40f4da3210ece4d5994d81225eefbb21bb..d4ad38b0ffc77a9660bf4c6f6f17f98d94f879b9 100644 (file)
--- a/src/util/regexp.h
+++ b/src/util/regexp.h
@@ -28,81 +28,6 @@
 
 namespace CVC4 {
 
-class CVC4_PUBLIC Char {
-
-private:
-  unsigned int d_char;
-
-public:
-  Char() {}
-
-  Char(const unsigned int c)
-      : d_char(c) {}
-
-  ~Char() {}
-
-  Char& operator =(const Char& y) {
-    if(this != &y) d_char = y.d_char;
-    return *this;
-  }
-
-  bool operator ==(const Char& y) const {
-    return d_char == y.d_char ;
-  }
-
-  bool operator !=(const Char& y) const {
-    return d_char != y.d_char ;
-  }
-
-  bool operator <(const Char& y) const {
-    return d_char < y.d_char;
-  }
-
-  bool operator >(const Char& y) const {
-    return d_char > y.d_char ;
-  }
-
-  bool operator <=(const Char& y) const {
-    return d_char <= y.d_char;
-  }
-
-  bool operator >=(const Char& y) const {
-    return d_char >= y.d_char ;
-  }
-
-  /*
-   * Convenience functions
-   */
-  std::string toString() const {
-    std::string str = "1";
-    str[0] = (char) d_char;
-    return str;
-  }
-
-  unsigned size() const {
-    return 1;
-  }
-
-  const char* c_str() const {
-    return toString().c_str();
-  }
-};/* class Char */
-
-namespace strings {
-
-struct CharHashFunction {
-  size_t operator()(const ::CVC4::Char& c) const {
-    return __gnu_cxx::hash<const char*>()(c.toString().c_str());
-  }
-};/* struct CharHashFunction */
-
-}
-
-inline std::ostream& operator <<(std::ostream& os, const Char& c) CVC4_PUBLIC;
-inline std::ostream& operator <<(std::ostream& os, const Char& c) {
-  return os << "\"" << c.toString() << "\"";
-}
-
 class CVC4_PUBLIC String {
 
 private:
@@ -330,9 +255,6 @@ public:
     return d_str;
   }
 
-  unsigned size() const {
-    return d_str.size();
-  }
 };/* class String */
 
 /**