minor printer fix; intersection fix

diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index 528436033c4d5dcae14dfa9449453f62bdcc9a60..d719b4e1a10be12077477cd724f5ccdc5fcb5f37 100644 (file)
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -1217,66 +1217,53 @@ Node RegExpOpr::intersectInternal( Node r1, Node r2, std::map< unsigned, std::se
                if(r1 == r2) {\r
                        rNode = r1;\r
                } else if(r1 == d_emptyRegexp || r2 == d_emptyRegexp) {\r
-                       Trace("regexp-intersect") << "INTERSECT Case 1: one empty RE" << std::endl;\r
                        rNode = d_emptyRegexp;\r
                } else if(r1 == d_emptySingleton || r2 == d_emptySingleton) {\r
-                       Trace("regexp-intersect") << "INTERSECT Case 2: one empty Singleton" << std::endl;\r
                        Node exp;\r
                        int r = delta((r1 == d_emptySingleton ? r2 : r1), exp);\r
                        if(r == 0) {\r
                                //TODO: variable\r
                                spflag = true;\r
-                               //Assert( false, "Unsupported Yet, 892 REO" );\r
                        } else if(r == 1) {\r
                                rNode = d_emptySingleton;\r
                        } else {\r
                                rNode = d_emptyRegexp;\r
                        }\r
                } else {\r
-                       Trace("regexp-intersect") << "INTERSECT Case 3: must compare" << std::endl;\r
                        std::set< unsigned > cset, cset2;\r
-                       std::vector< unsigned > cdiff;\r
-                       std::set< Node > vset;\r
+                       std::set< Node > vset, vset2;\r
                        getCharSet(r1, cset, vset);\r
-                       getCharSet(r2, cset2, vset);\r
-                       if(vset.empty()) {\r
-                               std::set_symmetric_difference(cset.begin(), cset.end(), cset2.begin(), cset2.end(), std::back_inserter(cdiff));\r
-                               if(cdiff.empty()) {\r
-                                       Trace("regexp-intersect") << "INTERSECT Case 3.1: compare" << std::endl;\r
-                                       cset.clear();\r
-                                       firstChars(r1, cset, vset);\r
-                                       std::vector< Node > vec_nodes;\r
-                                       for(std::set<unsigned>::const_iterator itr = cset.begin();\r
-                                               itr != cset.end(); itr++) {\r
-                                               CVC4::String c( CVC4::String::convertUnsignedIntToChar(*itr) );\r
-                                               std::pair< Node, Node > p(r1, r2);\r
-                                               if(cache[ *itr ].find(p) == cache[ *itr ].end()) {\r
-                                                       Node r1l = derivativeSingle(r1, c);\r
-                                                       Node r2l = derivativeSingle(r2, c);\r
-                                                       std::map< unsigned, std::set< PairNodes > > cache2(cache);\r
-                                                       PairNodes p(r1l, r2l);\r
-                                                       cache2[ *itr ].insert( p );\r
-                                                       Node rt = intersectInternal(r1l, r2l, cache2, spflag);\r
-                                                       if(spflag) {\r
-                                                               //TODO:\r
-                                                               return Node::null();\r
-                                                       }\r
-                                                       rt = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, \r
-                                                               NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst(c)), rt) );\r
-                                                       vec_nodes.push_back(rt);\r
+                       getCharSet(r2, cset2, vset2);\r
+                       if(vset.empty() && vset2.empty()) {\r
+                               cset.clear();\r
+                               firstChars(r1, cset, vset);\r
+                               std::vector< Node > vec_nodes;\r
+                               for(std::set<unsigned>::const_iterator itr = cset.begin();\r
+                                       itr != cset.end(); itr++) {\r
+                                       CVC4::String c( CVC4::String::convertUnsignedIntToChar(*itr) );\r
+                                       std::pair< Node, Node > p(r1, r2);\r
+                                       if(cache[ *itr ].find(p) == cache[ *itr ].end()) {\r
+                                               Node r1l = derivativeSingle(r1, c);\r
+                                               Node r2l = derivativeSingle(r2, c);\r
+                                               std::map< unsigned, std::set< PairNodes > > cache2(cache);\r
+                                               PairNodes p(r1l, r2l);\r
+                                               cache2[ *itr ].insert( p );\r
+                                               Node rt = intersectInternal(r1l, r2l, cache2, spflag);\r
+                                               if(spflag) {\r
+                                                       //TODO:\r
+                                                       return Node::null();\r
                                                }\r
+                                               rt = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, \r
+                                                       NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst(c)), rt) );\r
+                                               vec_nodes.push_back(rt);\r
                                        }\r
-                                       rNode = vec_nodes.size()==0 ? d_emptyRegexp : vec_nodes.size()==1 ? vec_nodes[0] :\r
-                                                       NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, vec_nodes);\r
-                                       rNode = Rewriter::rewrite( rNode );\r
-                               } else {\r
-                                       Trace("regexp-intersect") << "INTERSECT Case 3.2: diff cset" << std::endl;\r
-                                       rNode = d_emptyRegexp;\r
                                }\r
+                               rNode = vec_nodes.size()==0 ? d_emptyRegexp : vec_nodes.size()==1 ? vec_nodes[0] :\r
+                                               NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, vec_nodes);\r
+                               rNode = Rewriter::rewrite( rNode );\r
                        } else {\r
                                //TODO: non-empty var set\r
                                spflag = true;\r
-                               //Assert( false, "Unsupported Yet, 927 REO" );\r
                        }\r
                }\r
                d_inter_cache[p] = rNode;\r
@@ -1307,7 +1294,6 @@ Node RegExpOpr::complement(Node r, int &ret) {
                        std::set<unsigned> cset;\r
                        SetNodes vset;\r
                        firstChars(r, cset, vset);\r
-                       Assert(!vset.empty(), "Regexp 1298 Error");\r
                        std::vector< Node > vec_nodes;\r
                        for(unsigned i=0; i<d_card; i++) {\r
                                CVC4::String c = CVC4::String::convertUnsignedIntToChar(i);\r
@@ -1330,6 +1316,7 @@ Node RegExpOpr::complement(Node r, int &ret) {
                        rNode = vec_nodes.size()==0? d_emptyRegexp : vec_nodes.size()==1? vec_nodes[0] :\r
                                                NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, vec_nodes);\r
                }\r
+               rNode = Rewriter::rewrite(rNode);\r
                std::pair< Node, int > p(rNode, ret);\r
                d_compl_cache[r] = p;\r
        }\r
@@ -1340,9 +1327,10 @@ Node RegExpOpr::complement(Node r, int &ret) {
 std::string RegExpOpr::niceChar( Node r ) {\r
        if(r.isConst()) {\r
                std::string s = r.getConst<CVC4::String>().toString() ;\r
-               return s == "" ? "{E}" : ( s == " " ? "{ }" : s );\r
+               return s == "" ? "{E}" : ( s == " " ? "{ }" : s.size()>1? "("+s+")" : s );\r
        } else {\r
-               return r.toString();\r
+               std::string ss = "$" + r.toString();\r
+               return ss;\r
        }\r
 }\r
 std::string RegExpOpr::mkString( Node r ) {\r
@@ -1365,12 +1353,12 @@ std::string RegExpOpr::mkString( Node r ) {
                                break;\r
                        }\r
                        case kind::REGEXP_CONCAT: {\r
-                               //retStr += "(";\r
+                               retStr += "(";\r
                                for(unsigned i=0; i<r.getNumChildren(); ++i) {\r
                                        //if(i != 0) retStr += ".";\r
                                        retStr += mkString( r[i] );\r
                                }\r
-                               //retStr += ")";\r
+                               retStr += ")";\r
                                break;\r
                        }\r
                        case kind::REGEXP_UNION: {\r

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index a19d35d4b8f0bc647961c234aeb6e11456fd5173..9ed52e94ad619f420dfde972f1c8617cbd0c78f2 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -2333,7 +2333,7 @@ bool TheoryStrings::checkMemberships() {
        std::vector< Node > processed;
        std::vector< Node > cprocessed;
 
-       if(options::stringEIT()) {
+       //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;
@@ -2391,7 +2391,7 @@ bool TheoryStrings::checkMemberships() {
                                }
                        }
                }
-       }
+       //}
 
        if(!addedLemma) {
          for( unsigned i=0; i<d_regexp_memberships.size(); i++ ) {
@@ -2871,8 +2871,7 @@ void TheoryStrings::addMembership(Node assertion) {
                        }
                }
                lst->push_back( r );
-               d_regexp_memberships.push_back( assertion );
-       } else {
+       }/* else {
                if(options::stringEIT() && d_regexp_opr.checkConstRegExp(r)) {
                        int rt;
                        Node r2 = d_regexp_opr.complement(r, rt);
@@ -2881,7 +2880,8 @@ void TheoryStrings::addMembership(Node assertion) {
                } else {
                        d_regexp_memberships.push_back( assertion );
                }
-       }
+       }*/
+       d_regexp_memberships.push_back( assertion );
 }
 
 //// Finite Model Finding

diff --git a/src/util/regexp.cpp b/src/util/regexp.cpp
index fd5dff994eb0e8e3cd437ee28cc1cd09380f1d4b..b6db624d5770d7f8dee8c4f50c02d186227922e6 100644 (file)
--- a/src/util/regexp.cpp
+++ b/src/util/regexp.cpp
@@ -56,7 +56,9 @@ std::string String::toString() const {
                        default  : {\r
                                std::stringstream ss;\r
                                ss << std::setfill ('0') << std::setw(2) << std::hex << ((int)c);\r
-                               s = "\\x" + ss.str();\r
+                               std::string t = ss.str();\r
+                               t = t.substr(t.size()-2, 2);\r
+                               s = "\\x" + t;\r
                                //std::string s2 = static_cast<std::ostringstream*>( &(std::ostringstream() << (int)c) )->str();\r
                        }\r
                  }\r