add string progress measurements

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 219a24ddc5c0ae7b2559c4ab1b341fa4a0400ea4..4182374fb39a4448b7511ce5f5f03d70317edb5f 100644 (file)
--- 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<String>().size() == 1 ? const_str :
                                                                                                                NodeManager::currentNM()->mkConst( const_str.getConst<String>().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<String>().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 0fdedcd8a6d1d9e58783b8e0b58c633658e8fd7a..6ac8cf99592d5fcbd6c6f4aa9af3b13e01ab6760 100644 (file)
--- 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: