From: Tianyi Liang Date: Sat, 25 Jan 2014 18:49:19 +0000 (-0600) Subject: replace charat uf with internal one X-Git-Tag: cvc5-1.0.0~7122 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=160572318e251a98a58b3f506c31fb233070d477;p=cvc5.git replace charat uf with internal one --- diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index effbbca2e..4deb0a9d9 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -44,7 +44,6 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu d_length_nodes(c), //d_var_lmin( c ), //d_var_lmax( c ), - d_charAtUF(), d_str_pos_ctn( c ), d_str_neg_ctn( c ), d_reg_exp_mem( c ), @@ -55,10 +54,11 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu d_equalityEngine.addFunctionKind(kind::STRING_LENGTH); d_equalityEngine.addFunctionKind(kind::STRING_CONCAT); d_equalityEngine.addFunctionKind(kind::STRING_STRCTN); - //d_equalityEngine.addFunctionKind(kind::STRING_CHARAT_TOTAL); + d_equalityEngine.addFunctionKind(kind::STRING_CHARAT_TOTAL); //d_equalityEngine.addFunctionKind(kind::STRING_SUBSTR_TOTAL); d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) ); + d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) ); d_emptyString = NodeManager::currentNM()->mkConst( ::CVC4::String("") ); d_true = NodeManager::currentNM()->mkConst( true ); d_false = NodeManager::currentNM()->mkConst( false ); @@ -384,13 +384,19 @@ void TheoryStrings::preRegisterTerm(TNode n) { default: if(n.getType().isString() && n.getKind() != kind::CONST_STRING && n.getKind()!=kind::STRING_CONCAT ) { if( std::find( d_length_intro_vars.begin(), d_length_intro_vars.end(), n )==d_length_intro_vars.end() ) { - Node n_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n); - Node n_len_eq_z = n_len.eqNode( d_zero ); - Node n_len_geq_zero = NodeManager::currentNM()->mkNode( kind::OR, n_len_eq_z, - NodeManager::currentNM()->mkNode( kind::GT, n_len, d_zero) ); - Trace("strings-lemma") << "Strings::Lemma LENGTH >= 0 : " << n_len_geq_zero << std::endl; - d_out->lemma(n_len_geq_zero); - d_out->requirePhase( n_len_eq_z, true ); + if(n.getKind() == kind::STRING_CHARAT_TOTAL) { + Node lenc_eq_one = d_one.eqNode(NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n)); + Trace("strings-lemma") << "Strings::Lemma LEN(CHAR) = 1 : " << lenc_eq_one << std::endl; + d_out->lemma(lenc_eq_one); + } else { + Node n_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n); + Node n_len_eq_z = n_len.eqNode( d_zero ); + Node n_len_geq_zero = NodeManager::currentNM()->mkNode( kind::OR, n_len_eq_z, + NodeManager::currentNM()->mkNode( kind::GT, n_len, d_zero) ); + Trace("strings-lemma") << "Strings::Lemma LENGTH >= 0 : " << n_len_geq_zero << std::endl; + d_out->lemma(n_len_geq_zero); + d_out->requirePhase( n_len_eq_z, true ); + } } // FMF if( n.getKind() == kind::VARIABLE ) {//options::stringFMF() && @@ -469,14 +475,14 @@ void TheoryStrings::check(Effort e) { addedLemma = checkLengthsEqc(); Trace("strings-process") << "Done check lengths, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; if(!d_conflict && !addedLemma) { - addedLemma = checkCardinality(); - Trace("strings-process") << "Done check cardinality, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; + addedLemma = checkContains(); + Trace("strings-process") << "Done check contain constraints, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; if( !d_conflict && !addedLemma ) { addedLemma = checkMemberships(); Trace("strings-process") << "Done check membership constraints, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; if( !d_conflict && !addedLemma ) { - addedLemma = checkContains(); - Trace("strings-process") << "Done check contain constraints, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; + addedLemma = checkCardinality(); + Trace("strings-process") << "Done check cardinality, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; } } } @@ -994,12 +1000,11 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms bool success; do { - //---------------------do simple stuff first + //simple check if( processSimpleNEq( normal_forms, normal_form_src, curr_exp, i, j, index_i, index_j, false ) ){ //added a lemma, return return true; } - //---------------------- success = false; //if we are at the end @@ -1097,11 +1102,6 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms } } - //Node sk = NodeManager::currentNM()->mkSkolem( "v_spt_$$", normal_forms[i][index_i].getType(), "created for v/v split" ); - //Node eq1 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[i][index_i], - // NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, normal_forms[j][index_j], sk ) ) ); - //Node eq2 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[j][index_j], - // NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, normal_forms[i][index_i], sk ) ) ); 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 ); @@ -1358,10 +1358,10 @@ bool TheoryStrings::processDeq( Node ni, Node nj ) { std::vector< Node > nfj; nfj.insert( nfj.end(), d_normal_forms[nj].begin(), d_normal_forms[nj].end() ); - //int revRet = processReverseDeq( nfi, nfj, ni, nj ); - //if( revRet!=0 ){ - // return revRet==-1; - //} + int revRet = processReverseDeq( nfi, nfj, ni, nj ); + if( revRet!=0 ){ + return revRet==-1; + } nfi.clear(); nfi.insert( nfi.end(), d_normal_forms[ni].begin(), d_normal_forms[ni].end() ); @@ -2366,19 +2366,8 @@ bool TheoryStrings::checkNegContains() { Node g1 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, NodeManager::currentNM()->mkNode( kind::GEQ, b1, d_zero ), NodeManager::currentNM()->mkNode( kind::GEQ, NodeManager::currentNM()->mkNode( kind::MINUS, lenx, lens ), b1 ) ) ); Node b2 = NodeManager::currentNM()->mkBoundVar("bj", NodeManager::currentNM()->integerType()); - if(d_charAtUF.isNull()) { - std::vector< TypeNode > argTypes; - argTypes.push_back(NodeManager::currentNM()->stringType()); - argTypes.push_back(NodeManager::currentNM()->integerType()); - d_charAtUF = NodeManager::currentNM()->mkSkolem("charAt", - NodeManager::currentNM()->mkFunctionType( - argTypes, - NodeManager::currentNM()->stringType()), - "total charat", - NodeManager::SKOLEM_EXACT_NAME); - } - Node s2 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_charAtUF, x, NodeManager::currentNM()->mkNode( kind::PLUS, b1, b2 )); - Node s5 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_charAtUF, s, b2); + Node s2 = NodeManager::currentNM()->mkNode(kind::STRING_CHARAT_TOTAL, x, NodeManager::currentNM()->mkNode( kind::PLUS, b1, b2 )); + Node s5 = NodeManager::currentNM()->mkNode(kind::STRING_CHARAT_TOTAL, s, b2); Node s1 = NodeManager::currentNM()->mkBoundVar("s1", NodeManager::currentNM()->stringType()); Node s3 = NodeManager::currentNM()->mkBoundVar("s3", NodeManager::currentNM()->stringType()); @@ -2398,10 +2387,6 @@ bool TheoryStrings::checkNegContains() { vec_nodes.push_back(cc); cc = s2.eqNode(s5).negate(); vec_nodes.push_back(cc); - cc = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s2).eqNode(NodeManager::currentNM()->mkConst( Rational(1))); - vec_nodes.push_back(cc); - cc = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s5).eqNode(NodeManager::currentNM()->mkConst( Rational(1))); - vec_nodes.push_back(cc); cc = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s1).eqNode(NodeManager::currentNM()->mkNode( kind::PLUS, b1, b2 )); vec_nodes.push_back(cc); cc = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s4).eqNode(b2); diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 1f69c81be..1dae73360 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -114,6 +114,7 @@ private: Node d_true; Node d_false; Node d_zero; + Node d_one; // Options bool d_all_warning; bool d_opt_fmf; @@ -286,7 +287,6 @@ private: int getMaxPossibleLength( Node x ); // Special String Functions - Node d_charAtUF; NodeList d_str_pos_ctn; NodeList d_str_neg_ctn; std::map< Node, bool > d_str_ctn_eqlen; diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 11642a4d2..00d02e015 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -27,12 +27,6 @@ StringsPreprocess::StringsPreprocess() { std::vector< TypeNode > argTypes; argTypes.push_back(NodeManager::currentNM()->stringType()); argTypes.push_back(NodeManager::currentNM()->integerType()); - d_charAtUF = NodeManager::currentNM()->mkSkolem("charAt", - NodeManager::currentNM()->mkFunctionType( - argTypes, - NodeManager::currentNM()->stringType()), - "total charat", - NodeManager::SKOLEM_EXACT_NAME); } void StringsPreprocess::simplifyRegExp( Node s, Node r, std::vector< Node > &ret, std::vector< Node > &nn ) { @@ -137,14 +131,11 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { int v_id = 1 - c_id; int len = t[c_id].getConst().getNumerator().toUnsignedInt(); if(len > 1) { - Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) ); std::vector< Node > vec; for(int i=0; imkConst( ::CVC4::Rational(i) ); - Node sk = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_charAtUF, t[v_id][0], num); + Node sk = NodeManager::currentNM()->mkNode(kind::STRING_CHARAT_TOTAL, t[v_id][0], num); vec.push_back(sk); - Node lem = one.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk ) ); - new_nodes.push_back( lem ); } Node lem = t[v_id][0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, vec ) ); lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, t, lem ); @@ -189,26 +180,6 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { tp = NodeManager::currentNM()->mkNode( kind::IMPLIES, lenxgti, tp ); new_nodes.push_back( tp ); - d_cache[t] = sk2; - retNode = sk2; - } else if( t.getKind() == kind::STRING_CHARAT_TOTAL ){ - Node sk1 = NodeManager::currentNM()->mkSkolem( "ca1_$$", NodeManager::currentNM()->stringType(), "created for charat" ); - Node sk2 = NodeManager::currentNM()->mkSkolem( "ca2_$$", NodeManager::currentNM()->stringType(), "created for charat" ); - Node sk3 = NodeManager::currentNM()->mkSkolem( "ca3_$$", NodeManager::currentNM()->stringType(), "created for charat" ); - Node x = simplify( t[0], new_nodes ); - Node lenxgti = NodeManager::currentNM()->mkNode( kind::GT, - NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, x ), t[1] ); - Node x_eq_123 = NodeManager::currentNM()->mkNode( kind::EQUAL, - NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk2, sk3 ), x ); - Node len_sk1_eq_i = NodeManager::currentNM()->mkNode( kind::EQUAL, t[1], - NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) ); - Node len_sk2_eq_1 = NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkConst( Rational( 1 ) ), - NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2 ) ); - - Node tp = NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i, len_sk2_eq_1 ); - tp = NodeManager::currentNM()->mkNode( kind::IMPLIES, lenxgti, tp ); - new_nodes.push_back( tp ); - d_cache[t] = sk2; retNode = sk2; } else if( t.getKind() == kind::STRING_STRIDOF ){ @@ -278,7 +249,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { throw LogicException("string replace not supported in this release"); } } else if(t.getKind() == kind::STRING_CHARAT) { - Node sk2 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_charAtUF, t[0], t[1]); + Node sk2 = NodeManager::currentNM()->mkNode(kind::STRING_CHARAT_TOTAL, t[0], t[1]); Node sk1 = NodeManager::currentNM()->mkSkolem( "ca1_$$", NodeManager::currentNM()->stringType(), "created for charat" ); Node sk3 = NodeManager::currentNM()->mkSkolem( "ca3_$$", NodeManager::currentNM()->stringType(), "created for charat" ); Node x = simplify( t[0], new_nodes ); @@ -288,16 +259,12 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { Node len_sk1_eq_i = t[1].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) ); Node tp = NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i ); tp = NodeManager::currentNM()->mkNode( kind::IMPLIES, lenxgti, tp ); - Node len_sk2_eq_1 = NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkConst( Rational( 1 ) ), - NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2 ) ); - tp = NodeManager::currentNM()->mkNode( kind::AND, len_sk2_eq_1, tp ); - new_nodes.push_back( tp ); d_cache[t] = sk2; retNode = sk2; } else if(t.getKind() == kind::STRING_SUBSTR) { - InternalError("CharAt and Substr should not be reached here."); + InternalError("Substr should not be reached here."); } else if( t.getNumChildren()>0 ) { std::vector< Node > cc; if (t.getMetaKind() == kind::metakind::PARAMETERIZED) { diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h index 27808f0b2..99312ddc0 100644 --- a/src/theory/strings/theory_strings_preprocess.h +++ b/src/theory/strings/theory_strings_preprocess.h @@ -31,7 +31,6 @@ namespace strings { class StringsPreprocess { // NOTE: this class is NOT context-dependent std::hash_map d_cache; - Node d_charAtUF; private: bool checkStarPlus( Node t ); int checkFixLenVar( Node t ); diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 78731d469..86af2ffa8 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -323,16 +323,22 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { } else if(node.getKind() == kind::STRING_LENGTH) { if(node[0].isConst()) { retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational( node[0].getConst().size() ) ); + } else if(node[0].getKind() == kind::STRING_CHARAT_TOTAL) { + retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational( 1 ) ); } else if(node[0].getKind() == kind::STRING_CONCAT) { Node tmpNode = rewriteConcatString(node[0]); if(tmpNode.isConst()) { retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational( tmpNode.getConst().size() ) ); + } else if(tmpNode.getKind() == kind::STRING_CHARAT_TOTAL) { + retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational( 1 ) ); } else { // it has to be string concat std::vector node_vec; for(unsigned int i=0; imkConst( ::CVC4::Rational( tmpNode[i].getConst().size() ) ) ); + } else if(tmpNode[i].getKind() == kind::STRING_CHARAT_TOTAL) { + node_vec.push_back( NodeManager::currentNM()->mkConst( ::CVC4::Rational( 1 ) ) ); } else { node_vec.push_back( NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, tmpNode[i]) ); } @@ -360,7 +366,7 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { retNode = NodeManager::currentNM()->mkConst( false ); } } - } else if(node.getKind() == kind::STRING_CHARAT) { + } else if(node.getKind() == kind::STRING_CHARAT || node.getKind() == kind::STRING_CHARAT_TOTAL) { if( node[0].isConst() && node[1].isConst() ) { int i = node[1].getConst().getNumerator().toUnsignedInt(); if( node[0].getConst().size() > (unsigned) i ) {