From: Tianyi Liang Date: Mon, 28 Apr 2014 22:21:25 +0000 (-0500) Subject: minor change with kshitij's change X-Git-Tag: cvc5-1.0.0~6953^2^2 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7bf6de3859b8308e6b3243087f7b4036a252d60a;p=cvc5.git minor change with kshitij's change --- diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index 01a675324..5c664ba34 100644 --- 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 ) { } } if(ret == 0) { - Node sk = NodeManager::currentNM()->mkSkolem( "rsp_$$", NodeManager::currentNM()->stringType(), "Split RegExp" ); + Node sk = NodeManager::currentNM()->mkSkolem( "rsp", NodeManager::currentNM()->stringType(), "Split RegExp" ); retNode = NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, sk); if(!rest.isNull()) { retNode = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, retNode, rest)); @@ -1030,7 +1030,7 @@ void RegExpOpr::simplifyPRegExp( Node s, Node r, std::vector< Node > &new_nodes emptyflag = true; break; } else { - Node sk = NodeManager::currentNM()->mkSkolem( "rc_$$", s.getType(), "created for regular expression concat" ); + Node sk = NodeManager::currentNM()->mkSkolem( "rc", s.getType(), "created for regular expression concat" ); Node lem = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, sk, r[i]); nvec.push_back(lem); cc.push_back(sk); @@ -1090,8 +1090,8 @@ void RegExpOpr::simplifyPRegExp( Node s, Node r, std::vector< Node > &new_nodes } else { Node se = s.eqNode(d_emptyString); Node sinr = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s, r[0]); - Node sk1 = NodeManager::currentNM()->mkSkolem( "rs_$$", s.getType(), "created for regular expression star" ); - Node sk2 = NodeManager::currentNM()->mkSkolem( "rs_$$", s.getType(), "created for regular expression star" ); + Node sk1 = NodeManager::currentNM()->mkSkolem( "rs", s.getType(), "created for regular expression star" ); + Node sk2 = NodeManager::currentNM()->mkSkolem( "rs", s.getType(), "created for regular expression star" ); Node s1nz = sk1.eqNode(d_emptyString).negate(); Node s2nz = sk2.eqNode(d_emptyString).negate(); Node s1inr = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, sk1, r[0]); diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 21baa97dd..61d60d4cd 100644 --- 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().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 ced461c92..ef5da000f 100644 --- 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 ) );