minor fix for strings

diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index d719b4e1a10be12077477cd724f5ccdc5fcb5f37..0dd43b2293f5a1bab23370464046e35e5d4e6bbd 100644 (file)
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -41,10 +41,6 @@ RegExpOpr::RegExpOpr() {
        d_emptySingleton = NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, d_emptyString );\r
        std::vector< Node > nvec;\r
     d_emptyRegexp = NodeManager::currentNM()->mkNode( kind::REGEXP_EMPTY, nvec );\r
-       // All Charactors = all printable ones 32-126\r
-       //d_char_start = 'a';//' ';\r
-       //d_char_end = 'c';//'~';\r
-       //d_sigma = mkAllExceptOne( '\0' );\r
        d_sigma = NodeManager::currentNM()->mkNode( kind::REGEXP_SIGMA, nvec );\r
        d_sigma_star = NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, d_sigma );\r
        d_card = 256;\r
@@ -896,15 +892,13 @@ void RegExpOpr::simplifyNRegExp( Node s, Node r, std::vector< Node > &new_nodes
                        }\r
                        case kind::REGEXP_CONCAT: {\r
                                //TODO: rewrite empty\r
+                               Node lens = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s);\r
                                Node b1 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());\r
                                Node b1v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b1);\r
                                Node g1 = NodeManager::currentNM()->mkNode( kind::AND, NodeManager::currentNM()->mkNode(kind::GEQ, b1, d_zero),\r
                                                        NodeManager::currentNM()->mkNode( kind::GEQ, NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s), b1 ) );\r
-                               Node s1 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->stringType());\r
-                               Node s2 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->stringType());\r
-                               Node b2v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, s1, s2);\r
-                               Node s12 = s.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, s1, s2));\r
-                               Node s1len = b1.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s1));\r
+                               Node s1 = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, s, d_zero, b1));\r
+                               Node s2 = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, s, b1, NodeManager::currentNM()->mkNode(kind::MINUS, lens, b1)));\r
                                Node s1r1 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s1, r[0]).negate();\r
                                if(r[0].getKind() == kind::STRING_TO_REGEXP) {\r
                                        s1r1 = s1.eqNode(r[0][0]).negate();\r
@@ -928,8 +922,6 @@ void RegExpOpr::simplifyNRegExp( Node s, Node r, std::vector< Node > &new_nodes
                                }\r
 \r
                                conc = NodeManager::currentNM()->mkNode(kind::OR, s1r1, s2r2);\r
-                               conc = NodeManager::currentNM()->mkNode(kind::AND, s12, s1len, conc);\r
-                               conc = NodeManager::currentNM()->mkNode(kind::EXISTS, b2v, conc);\r
                                conc = NodeManager::currentNM()->mkNode(kind::IMPLIES, g1, conc);\r
                                conc = NodeManager::currentNM()->mkNode(kind::FORALL, b1v, conc);\r
                                break;\r