minor change with kshitij's change

diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index 01a6753246a64e987d4e910784047188f7887289..5c664ba3473482dfabe399d69a26461aec96e1d2 100644 (file)
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -292,7 +292,7 @@ int RegExpOpr::derivativeS( Node r, CVC4::String c, Node &retNode ) {
                                                }\r
                                        }\r
                                        if(ret == 0) {\r
-                                               Node sk = NodeManager::currentNM()->mkSkolem( "rsp_$$", NodeManager::currentNM()->stringType(), "Split RegExp" );\r
+                                               Node sk = NodeManager::currentNM()->mkSkolem( "rsp", NodeManager::currentNM()->stringType(), "Split RegExp" );\r
                                                retNode = NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, sk);\r
                                                if(!rest.isNull()) {\r
                                                        retNode = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, retNode, rest));\r
@@ -1030,7 +1030,7 @@ void RegExpOpr::simplifyPRegExp( Node s, Node r, std::vector< Node > &new_nodes
                                                emptyflag = true;\r
                                                break;\r
                                        } else {\r
-                                               Node sk = NodeManager::currentNM()->mkSkolem( "rc_$$", s.getType(), "created for regular expression concat" );\r
+                                               Node sk = NodeManager::currentNM()->mkSkolem( "rc", s.getType(), "created for regular expression concat" );\r
                                                Node lem = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, sk, r[i]);\r
                                                nvec.push_back(lem);\r
                                                cc.push_back(sk);\r
@@ -1090,8 +1090,8 @@ void RegExpOpr::simplifyPRegExp( Node s, Node r, std::vector< Node > &new_nodes
                                } else {\r
                                        Node se = s.eqNode(d_emptyString);\r
                                        Node sinr = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s, r[0]);\r
-                                       Node sk1 = NodeManager::currentNM()->mkSkolem( "rs_$$", s.getType(), "created for regular expression star" );\r
-                                       Node sk2 = NodeManager::currentNM()->mkSkolem( "rs_$$", s.getType(), "created for regular expression star" );\r
+                                       Node sk1 = NodeManager::currentNM()->mkSkolem( "rs", s.getType(), "created for regular expression star" );\r
+                                       Node sk2 = NodeManager::currentNM()->mkSkolem( "rs", s.getType(), "created for regular expression star" );\r
                                        Node s1nz = sk1.eqNode(d_emptyString).negate();\r
                                        Node s2nz = sk2.eqNode(d_emptyString).negate();\r
                                        Node s1inr = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, sk1, r[0]);\r

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 21baa97dd058e2741a3c59b47f5b07efb61ca403..61d60d4cd9617e991ea170bb3e39013f0c3c2613 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -427,8 +427,8 @@ void TheoryStrings::preRegisterTerm(TNode n) {
         Node t1geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, n[1], d_zero);
         Node t2geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, n[2], d_zero);
         Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1geq0, t2geq0 ));
-        Node sk1 = NodeManager::currentNM()->mkSkolem( "ss1_$$", NodeManager::currentNM()->stringType(), "created for charat/substr" );
-        Node sk3 = NodeManager::currentNM()->mkSkolem( "ss3_$$", NodeManager::currentNM()->stringType(), "created for charat/substr" );
+        Node sk1 = NodeManager::currentNM()->mkSkolem( "ss1", NodeManager::currentNM()->stringType(), "created for charat/substr" );
+        Node sk3 = NodeManager::currentNM()->mkSkolem( "ss3", NodeManager::currentNM()->stringType(), "created for charat/substr" );
         d_statistics.d_new_skolems += 2;
         Node x_eq_123 = n[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, n, sk3 ) );
         Node len_sk1_eq_i = n[1].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) );
@@ -1090,9 +1090,9 @@ bool TheoryStrings::processLoop(std::vector< Node > &antec,
                        } else {
                                Trace("strings-loop") << "Strings::Loop: Normal Breaking." << std::endl;
                                //right
-                               Node sk_w= NodeManager::currentNM()->mkSkolem( "w_loop_$$", normal_forms[other_n_index][other_index].getType(), "created for loop detection split" );
-                               Node sk_y= NodeManager::currentNM()->mkSkolem( "y_loop_$$", normal_forms[other_n_index][other_index].getType(), "created for loop detection split" );
-                               Node sk_z= NodeManager::currentNM()->mkSkolem( "z_loop_$$", normal_forms[other_n_index][other_index].getType(), "created for loop detection split" );
+                               Node sk_w= NodeManager::currentNM()->mkSkolem( "w_loop", normal_forms[other_n_index][other_index].getType(), "created for loop detection split" );
+                               Node sk_y= NodeManager::currentNM()->mkSkolem( "y_loop", normal_forms[other_n_index][other_index].getType(), "created for loop detection split" );
+                               Node sk_z= NodeManager::currentNM()->mkSkolem( "z_loop", normal_forms[other_n_index][other_index].getType(), "created for loop detection split" );
                                d_statistics.d_new_skolems += 3;
                                //t1 * ... * tn = y * z
                                Node conc1 = t_yz.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk_y, sk_z ) );
@@ -1241,7 +1241,7 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms
                                                                                if( stra.find(fc) == std::string::npos ||
                                                                                        (stra.find(strb) == std::string::npos &&
                                                                                         !stra.overlap(strb)) ) {
-                                                                                       Node sk = NodeManager::currentNM()->mkSkolem( "sopt_$$", NodeManager::currentNM()->stringType(), "created for string sp" );
+                                                                                       Node sk = NodeManager::currentNM()->mkSkolem( "sopt", NodeManager::currentNM()->stringType(), "created for string sp" );
                                                                                        Node eq = other_str.eqNode( mkConcat(const_str, sk) );
                                                                                        Node ant = mkExplain( antec );
                                                                                        sendLemma(ant, eq, "CST-EPS");
@@ -1253,7 +1253,7 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms
                                                                                        NodeManager::currentNM()->mkConst( const_str.getConst<String>().substr(0, 1) );
                                                                                //split the string
                                                                                Node eq1 = Rewriter::rewrite( other_str.eqNode( d_emptyString ) );
-                                                                               Node eq2 = mkSplitEq( "c_spt_$$", "created for v/c split", other_str, firstChar, false );
+                                                                               Node eq2 = mkSplitEq( "c_spt", "created for v/c split", other_str, firstChar, false );
                                                                                d_pending_req_phase[ eq1 ] = true;
                                                                                conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 );
                                                                                Trace("strings-solve-debug") << "Break normal form constant/variable " << std::endl;
@@ -1285,8 +1285,8 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms
                                                                                }
                                                                        }
 
-                                                                       Node eq1 = mkSplitEq( "v_spt_l_$$", "created for v/v split", normal_forms[i][index_i], normal_forms[j][index_j], true );
-                                                                       Node eq2 = mkSplitEq( "v_spt_r_$$", "created for v/v split", normal_forms[j][index_j], normal_forms[i][index_i], true );
+                                                                       Node eq1 = mkSplitEq( "v_spt_l", "created for v/v split", normal_forms[i][index_i], normal_forms[j][index_j], true );
+                                                                       Node eq2 = mkSplitEq( "v_spt_r", "created for v/v split", normal_forms[j][index_j], normal_forms[i][index_i], true );
                                                                        conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 );
 
                                                                        Node ant = mkExplain( antec, antec_new_lits );
@@ -1587,9 +1587,9 @@ bool TheoryStrings::processDeq( Node ni, Node nj ) {
                                                }
                                                antec_new_lits.push_back( li.eqNode( lj ).negate() );
                                                std::vector< Node > conc;
-                                               Node sk1 = NodeManager::currentNM()->mkSkolem( "x_dsplit_$$", ni.getType(), "created for disequality normalization" );
-                                               Node sk2 = NodeManager::currentNM()->mkSkolem( "y_dsplit_$$", ni.getType(), "created for disequality normalization" );
-                                               Node sk3 = NodeManager::currentNM()->mkSkolem( "z_dsplit_$$", ni.getType(), "created for disequality normalization" );
+                                               Node sk1 = NodeManager::currentNM()->mkSkolem( "x_dsplit", ni.getType(), "created for disequality normalization" );
+                                               Node sk2 = NodeManager::currentNM()->mkSkolem( "y_dsplit", ni.getType(), "created for disequality normalization" );
+                                               Node sk3 = NodeManager::currentNM()->mkSkolem( "z_dsplit", ni.getType(), "created for disequality normalization" );
                                                d_statistics.d_new_skolems += 3;
                                                //Node nemp = sk1.eqNode(d_emptyString).negate();
                                                //conc.push_back(nemp);
@@ -1908,7 +1908,7 @@ bool TheoryStrings::checkSimple() {
             Node sk;
             //if( d_length_inst.find(n)==d_length_inst.end() ) {
               //Node nr = d_equalityEngine.getRepresentative( n );
-              sk = NodeManager::currentNM()->mkSkolem( "lsym_$$", n.getType(), "created for length" );
+              sk = NodeManager::currentNM()->mkSkolem( "lsym", n.getType(), "created for length" );
               d_statistics.d_new_skolems += 1;
               d_length_intro_vars.insert( sk );
               Node eq = sk.eqNode(n);
@@ -2570,10 +2570,10 @@ bool TheoryStrings::checkMemberships() {
               }else{
                 Trace("strings-regexp-debug") << "Case 2\n";
                 std::vector< Node > conc_c;
-                Node s11 = NodeManager::currentNM()->mkSkolem( "s11_$$", NodeManager::currentNM()->stringType(), "created for re" );
-                Node s12 = NodeManager::currentNM()->mkSkolem( "s12_$$", NodeManager::currentNM()->stringType(), "created for re" );
-                Node s21 = NodeManager::currentNM()->mkSkolem( "s21_$$", NodeManager::currentNM()->stringType(), "created for re" );
-                Node s22 = NodeManager::currentNM()->mkSkolem( "s22_$$", NodeManager::currentNM()->stringType(), "created for re" );
+                Node s11 = NodeManager::currentNM()->mkSkolem( "s11", NodeManager::currentNM()->stringType(), "created for re" );
+                Node s12 = NodeManager::currentNM()->mkSkolem( "s12", NodeManager::currentNM()->stringType(), "created for re" );
+                Node s21 = NodeManager::currentNM()->mkSkolem( "s21", NodeManager::currentNM()->stringType(), "created for re" );
+                Node s22 = NodeManager::currentNM()->mkSkolem( "s22", NodeManager::currentNM()->stringType(), "created for re" );
                 conc = p1.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, s11, s12));
                 conc_c.push_back(conc);
                 conc = p2.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, s21, s22));
@@ -2745,8 +2745,8 @@ bool TheoryStrings::checkPosContains() {
                        Node s = atom[1];
                        if( !areEqual( s, d_emptyString ) && !areEqual( s, x ) ) {
                                if(d_pos_ctn_cached.find(atom) == d_pos_ctn_cached.end()) {
-                                       Node sk1 = NodeManager::currentNM()->mkSkolem( "sc1_$$", s.getType(), "created for contain" );
-                                       Node sk2 = NodeManager::currentNM()->mkSkolem( "sc2_$$", s.getType(), "created for contain" );
+                                       Node sk1 = NodeManager::currentNM()->mkSkolem( "sc1", s.getType(), "created for contain" );
+                                       Node sk2 = NodeManager::currentNM()->mkSkolem( "sc2", s.getType(), "created for contain" );
                                        d_statistics.d_new_skolems += 2;
                                        Node eq = Rewriter::rewrite( x.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, s, sk2 ) ) );
                                        sendLemma( atom, eq, "POS-INC" );

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index ced461c92c2b3843dbdffec915810de6edb81ac9..ef5da000fa6a3e7460bb84dffee292c4e8007861 100644 (file)
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -184,8 +184,8 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
                Node t1geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, t[1], d_zero);
                Node t2geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, t[2], d_zero);
                Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1geq0, t2geq0 ));
-               Node sk1 = NodeManager::currentNM()->mkSkolem( "ss1_$$", NodeManager::currentNM()->stringType(), "created for charat/substr" );
-               Node sk3 = NodeManager::currentNM()->mkSkolem( "ss3_$$", NodeManager::currentNM()->stringType(), "created for charat/substr" );
+               Node sk1 = NodeManager::currentNM()->mkSkolem( "ss1", NodeManager::currentNM()->stringType(), "created for charat/substr" );
+               Node sk3 = NodeManager::currentNM()->mkSkolem( "ss3", NodeManager::currentNM()->stringType(), "created for charat/substr" );
                Node x_eq_123 = t[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, t, sk3 ) );
                Node len_sk1_eq_i = t[1].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) );
                Node lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::ITE, cond, 
@@ -196,11 +196,11 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
                d_cache[t] = t;
        } else if( t.getKind() == kind::STRING_STRIDOF ) {
                if(options::stringExp()) {
-                       Node sk1 = NodeManager::currentNM()->mkSkolem( "io1_$$", t[0].getType(), "created for indexof" );
-                       Node sk2 = NodeManager::currentNM()->mkSkolem( "io2_$$", t[0].getType(), "created for indexof" );
-                       Node sk3 = NodeManager::currentNM()->mkSkolem( "io3_$$", t[0].getType(), "created for indexof" );
-                       Node sk4 = NodeManager::currentNM()->mkSkolem( "io4_$$", t[0].getType(), "created for indexof" );
-                       Node skk = NodeManager::currentNM()->mkSkolem( "iok_$$", t[2].getType(), "created for indexof" );
+                       Node sk1 = NodeManager::currentNM()->mkSkolem( "io1", t[0].getType(), "created for indexof" );
+                       Node sk2 = NodeManager::currentNM()->mkSkolem( "io2", t[0].getType(), "created for indexof" );
+                       Node sk3 = NodeManager::currentNM()->mkSkolem( "io3", t[0].getType(), "created for indexof" );
+                       Node sk4 = NodeManager::currentNM()->mkSkolem( "io4", t[0].getType(), "created for indexof" );
+                       Node skk = NodeManager::currentNM()->mkSkolem( "iok", t[2].getType(), "created for indexof" );
                        Node eq = t[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk2, sk3, sk4 ) );
                        new_nodes.push_back( eq );
                        Node negone = NodeManager::currentNM()->mkConst( ::CVC4::Rational(-1) );
@@ -274,11 +274,11 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
                        
                        std::vector< TypeNode > argTypes;
                        argTypes.push_back(NodeManager::currentNM()->integerType());
-                       Node ufP = NodeManager::currentNM()->mkSkolem("ufP_$$", 
+                       Node ufP = NodeManager::currentNM()->mkSkolem("ufP", 
                                                                NodeManager::currentNM()->mkFunctionType(
                                                                        argTypes, NodeManager::currentNM()->integerType()),
                                                                "uf type conv P");
-                       Node ufM = NodeManager::currentNM()->mkSkolem("ufM_$$", 
+                       Node ufM = NodeManager::currentNM()->mkSkolem("ufM", 
                                                                NodeManager::currentNM()->mkFunctionType(
                                                                        argTypes, NodeManager::currentNM()->integerType()),
                                                                "uf type conv M");
@@ -368,11 +368,11 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
                        Node ten = NodeManager::currentNM()->mkConst( ::CVC4::Rational(10) );
                        std::vector< TypeNode > argTypes;
                        argTypes.push_back(NodeManager::currentNM()->integerType());
-                       Node ufP = NodeManager::currentNM()->mkSkolem("ufP_$$", 
+                       Node ufP = NodeManager::currentNM()->mkSkolem("ufP", 
                                                                NodeManager::currentNM()->mkFunctionType(
                                                                        argTypes, NodeManager::currentNM()->integerType()),
                                                                "uf type conv P");
-                       Node ufM = NodeManager::currentNM()->mkSkolem("ufM_$$", 
+                       Node ufM = NodeManager::currentNM()->mkSkolem("ufM", 
                                                                NodeManager::currentNM()->mkFunctionType(
                                                                        argTypes, NodeManager::currentNM()->integerType()),
                                                                "uf type conv M");
@@ -404,9 +404,9 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
                        //cc1 = NodeManager::currentNM()->mkNode(kind::AND, ufP0.eqNode(negone), cc1);
                        //cc2
                        std::vector< Node > vec_n;
-                       Node z1 = NodeManager::currentNM()->mkSkolem("z1_$$", NodeManager::currentNM()->stringType());
-                       Node z2 = NodeManager::currentNM()->mkSkolem("z2_$$", NodeManager::currentNM()->stringType());
-                       Node z3 = NodeManager::currentNM()->mkSkolem("z3_$$", NodeManager::currentNM()->stringType());
+                       Node z1 = NodeManager::currentNM()->mkSkolem("z1", NodeManager::currentNM()->stringType());
+                       Node z2 = NodeManager::currentNM()->mkSkolem("z2", NodeManager::currentNM()->stringType());
+                       Node z3 = NodeManager::currentNM()->mkSkolem("z3", NodeManager::currentNM()->stringType());
                        Node g = one.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, z2) );
                        vec_n.push_back(g);
                        g = t[0].eqNode( NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, z1, z2, z3) );
@@ -499,9 +499,9 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
                        Node x = t[0];
                        Node y = t[1];
                        Node z = t[2];
-                       Node sk1 = NodeManager::currentNM()->mkSkolem( "rp1_$$", t[0].getType(), "created for replace" );
-                       Node sk2 = NodeManager::currentNM()->mkSkolem( "rp2_$$", t[0].getType(), "created for replace" );
-                       Node skw = NodeManager::currentNM()->mkSkolem( "rpw_$$", t[0].getType(), "created for replace" );
+                       Node sk1 = NodeManager::currentNM()->mkSkolem( "rp1", t[0].getType(), "created for replace" );
+                       Node sk2 = NodeManager::currentNM()->mkSkolem( "rp2", t[0].getType(), "created for replace" );
+                       Node skw = NodeManager::currentNM()->mkSkolem( "rpw", t[0].getType(), "created for replace" );
                        Node cond = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, x, y );
                        Node c1 = x.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, y, sk2 ) );
                        Node c2 = skw.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, z, sk2 ) );