From: Tianyi Liang Date: Tue, 12 Nov 2013 21:49:39 +0000 (-0600) Subject: add string progress measurements X-Git-Tag: cvc5-1.0.0~7260 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2c2ad5d3fde6f737116ee7a42b74be63df81ba8d;p=cvc5.git add string progress measurements --- diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 219a24ddc..4182374fb 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -361,10 +361,6 @@ void TheoryStrings::preRegisterTerm(TNode n) { NodeManager::currentNM()->mkNode( kind::GT, n_len, d_zero) ); Trace("strings-lemma") << "Strings::Lemma LENGTH geq 0 : " << n_len_geq_zero << std::endl; d_out->lemma(n_len_geq_zero); - - Node n_len_imp_empty = NodeManager::currentNM()->mkNode( kind::IMPLIES, n_len.eqNode( d_zero ), n.eqNode( d_emptyString) ); - Trace("strings-lemma") << "Strings::Lemma ZERO: " << n_len_geq_zero << std::endl; - d_out->lemma(n_len_imp_empty); } // FMF if( n.getKind() == kind::VARIABLE ) {//options::stringFMF() && @@ -533,7 +529,7 @@ void TheoryStrings::eqNotifyPreMerge(TNode t1, TNode t2){ d_pending.push_back( eq ); Node eq_exp = NodeManager::currentNM()->mkNode( kind::EQUAL, n, d_zero ); d_pending_exp[eq] = eq_exp; - Trace("strings-infer") << "Strings : Infer " << eq << " from " << eq_exp << std::endl; + Trace("strings-infer") << "Strings : Infer Empty : " << eq << " from " << eq_exp << std::endl; d_infer.push_back(eq); d_infer_exp.push_back(eq_exp); } @@ -1126,11 +1122,12 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v Node firstChar = const_str.getConst().size() == 1 ? const_str : NodeManager::currentNM()->mkConst( const_str.getConst().substr(0, 1) ); //split the string - Node sk = NodeManager::currentNM()->mkSkolem( "c_split_$$", normal_forms[i][index_i].getType(), "created for v/c split" ); + //Node sk = NodeManager::currentNM()->mkSkolem( "c_spt_$$", normal_forms[i][index_i].getType(), "created for v/c split" ); Node eq1 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::EQUAL, other_str, d_emptyString ) ); - Node eq2 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::EQUAL, other_str, - NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, firstChar, sk ) ) ); + Node eq2 = mkSplitEq( "c_spt_$$", "created for v/c split", other_str, firstChar, false ); + //Node eq2 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::EQUAL, other_str, + // NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, firstChar, sk ) ) ); 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; @@ -1160,19 +1157,21 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v } } - Node sk = NodeManager::currentNM()->mkSkolem( "v_split_$$", normal_forms[i][index_i].getType(), "created for v/v split" ); - Node eq1 = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[i][index_i], - NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, normal_forms[j][index_j], sk ) ); - Node eq2 = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[j][index_j], - NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, normal_forms[i][index_i], sk ) ); + //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 ); // |sk| > 0 - //Node sk_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk ); - //Node sk_gt_zero = NodeManager::currentNM()->mkNode( kind::GT, sk_len, d_zero); - Node sk_gt_zero = NodeManager::currentNM()->mkNode( kind::EQUAL, sk, d_emptyString).negate(); - Trace("strings-lemma") << "Strings lemma : " << sk_gt_zero << std::endl; - //d_out->lemma(sk_gt_zero); - d_lemma_cache.push_back( sk_gt_zero ); + ////Node sk_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk ); + ////Node sk_gt_zero = NodeManager::currentNM()->mkNode( kind::GT, sk_len, d_zero); + //Node sk_gt_zero = NodeManager::currentNM()->mkNode( kind::EQUAL, sk, d_emptyString).negate(); + //Trace("strings-lemma") << "Strings lemma : " << sk_gt_zero << std::endl; + ////d_out->lemma(sk_gt_zero); + //d_lemma_cache.push_back( sk_gt_zero ); Node ant = mkExplain( antec, antec_new_lits ); sendLemma( ant, conc, "VAR-SPLIT" ); @@ -2205,29 +2204,41 @@ Node TheoryStrings::getNextDecisionRequest() { void TheoryStrings::assertNode( Node lit ) { } -/* -Node TheoryStrings::mkSplitEq( const char * c, TypeNode tn, const char * info, Node lhs, Node rhs, bool lgtZero ) { +Node TheoryStrings::mkSplitEq( const char * c, const char * info, Node lhs, Node rhs, bool lgtZero ) { Node sk = NodeManager::currentNM()->mkSkolem( c, lhs.getType(), info ); Node eq = lhs.eqNode( mkConcat( rhs, sk ) ); eq = Rewriter::rewrite( eq ); - if( lgtZero ){ + if( lgtZero ) { d_var_lgtz[sk] = true; Node sk_gt_zero = NodeManager::currentNM()->mkNode( kind::EQUAL, sk, d_emptyString).negate(); - Trace("strings-lemma") << "Strings lemma : " << sk_gt_zero << std::endl; + Trace("strings-lemma") << "Strings::Lemma sk GT zero: " << sk_gt_zero << std::endl; d_lemma_cache.push_back( sk_gt_zero ); } //store it in proper map if( options::stringFMF() ){ d_var_split_graph_lhs[sk] = lhs; d_var_split_graph_rhs[sk] = rhs; - d_var_split_eq[sk] = eq; + //d_var_split_eq[sk] = eq; - int mpl = getMaxPossibleLength( sk ); - + //int mpl = getMaxPossibleLength( sk ); + Trace("strings-progress") << "Strings::Progress: Because of " << eq << std::endl; + Trace("strings-progress") << "Strings::Progress: \t" << lhs << "(up:" << getMaxPossibleLength(lhs) << ") is removed" << std::endl; + Trace("strings-progress") << "Strings::Progress: \t" << sk << "(up:" << getMaxPossibleLength(sk) << ") is added" << std::endl; } return eq; } -*/ + +int TheoryStrings::getMaxPossibleLength( Node x ) { + if( d_var_split_graph_lhs.find( x )==d_var_split_graph_lhs.end() ){ + if( x.getKind()==kind::CONST_STRING ){ + return x.getConst().size(); + }else{ + return d_curr_cardinality.get(); + } + }else{ + return getMaxPossibleLength( d_var_split_graph_lhs[x] ) - 1; + } +} }/* CVC4::theory::strings namespace */ }/* CVC4::theory namespace */ diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 0fdedcd8a..6ac8cf995 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -250,7 +250,11 @@ protected: private: //NodeIntMap d_var_lmin; //NodeIntMap d_var_lmax; - //Node mkSplitEq( const char * c, TypeNode tn, const char * info, Node lhs, Node rhs, bool lgtZero ); + std::map< Node, Node > d_var_split_graph_lhs; + std::map< Node, Node > d_var_split_graph_rhs; + std::map< Node, bool > d_var_lgtz; + Node mkSplitEq( const char * c, const char * info, Node lhs, Node rhs, bool lgtZero ); + int getMaxPossibleLength( Node x ); // Regular Expression private: