optimizing model generation for strings

2 files changed, 75 insertions, 51 deletions

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index ee413b13a..90eae244a 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -262,10 +262,12 @@ void TheoryStrings::preRegisterTerm(TNode n) {
     break;
   default:
     if(n.getKind() == kind::VARIABLE || n.getKind()==kind::SKOLEM) {
-      Node n_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n);
-      Node n_len_geq_zero = NodeManager::currentNM()->mkNode( kind::GEQ, n_len, d_zero);
-      Trace("strings-lemma") << "Strings: Add lemma " << n_len_geq_zero << std::endl;
-      d_out->lemma(n_len_geq_zero);
+	  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_geq_zero = NodeManager::currentNM()->mkNode( kind::GEQ, n_len, d_zero);
+		  Trace("strings-lemma") << "Strings: Add lemma " << n_len_geq_zero << std::endl;
+		  d_out->lemma(n_len_geq_zero);
+	  }
     }
     if (n.getType().isBoolean()) {
       // Get triggered for both equal and dis-equal
@@ -360,6 +362,7 @@ void TheoryStrings::check(Effort e) {
                     d_length_inst[n] = true;
                     Trace("strings-debug") << "get n: " << n << endl;
                     Node sk = NodeManager::currentNM()->mkSkolem( "lsym_$$", n.getType(), "created for concat lemma" );
+					d_length_intro_vars.push_back( sk );
                     Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, sk, n );
                     eq = Rewriter::rewrite(eq);
                     Trace("strings-lemma") << "Strings: Add lemma " << eq << std::endl;
@@ -744,10 +747,6 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
                                     return;
                                 }else{
                                     Trace("strings-solve-debug") << "Case 3 : must compare strings" << std::endl;
-                                    bool sendLemma = false;
-                                    Node loop_x;
-                                    Node loop_y;
-                                    Node loop_z;
                                     Node conc;
                                     std::vector< Node > antec;
                                     std::vector< Node > antec_new_lits;
@@ -836,7 +835,6 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
                                             Node sk_y= NodeManager::currentNM()->mkSkolem( "ldssym_$$", normal_forms[i][index_i].getType(), "created for loop detection split" );
                                             Node sk_z= NodeManager::currentNM()->mkSkolem( "ldssym_$$", normal_forms[i][index_i].getType(), "created for loop detection split" );
 
-                                            sendLemma = true;
                                             antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
                                             //t1 * ... * tn = y * z
                                             std::vector< Node > c1c;
@@ -870,11 +868,15 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
 											Node yz_imp_zz = NodeManager::currentNM()->mkNode( kind::IMPLIES, len_z_eq_zero, len_y_eq_zero);
 
                                             conc = NodeManager::currentNM()->mkNode( kind::AND, conc1, conc2, yz_imp_zz );//sk_z_len_gt_zero, yz_imp_zz
-                                            loop_x = normal_forms[other_n_index][other_index];
-                                            loop_y = sk_y;
-                                            loop_z = sk_z;
+                                            Node loop_x = normal_forms[other_n_index][other_index];
+                                            Node loop_y = sk_y;
+                                            Node loop_z = sk_z;
                                             //we will be done
                                             addNormalFormPair( normal_form_src[i], normal_form_src[j] );
+											Node ant = mkExplain( antec, antec_new_lits );
+											sendLemma( ant, conc, "Loop" );
+											addInductiveEquation( loop_x, loop_y, loop_z, ant );
+											return;
                                         } else {
 											// x = (yz)*y
 											Trace("strings-loop") << "We have that " << normal_forms[loop_n_index][loop_index] << " = (";
@@ -925,8 +927,12 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
                                         Trace("strings-solve-debug") << "No loops detected." << std::endl;
                                         if( normal_forms[i][index_i].getKind() == kind::CONST_STRING ||
                                             normal_forms[j][index_j].getKind() == kind::CONST_STRING) {
-                                            Node const_str = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? normal_forms[i][index_i] : normal_forms[j][index_j];
-                                            Node other_str = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? normal_forms[j][index_j] : normal_forms[i][index_i];
+											unsigned const_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? i : j;
+											unsigned const_index_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? index_i : index_j;
+											unsigned nconst_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? j : i;
+											unsigned nconst_index_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? index_j : index_i;
+                                            Node const_str = normal_forms[const_k][const_index_k];
+                                            Node other_str = normal_forms[nconst_k][nconst_index_k];
                                             if( other_str.getKind() == kind::CONST_STRING ) {
                                                 unsigned len_short = const_str.getConst<String>().size() <= other_str.getConst<String>().size() ? const_str.getConst<String>().size() : other_str.getConst<String>().size();
                                                 if( const_str.getConst<String>().strncmp(other_str.getConst<String>(), len_short) ) {
@@ -943,27 +949,43 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
                                                     success = true;
                                                 } else {
                                                     //curr_exp is conflict
-                                                    sendLemma = true;
                                                     antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
+													Node ant = mkExplain( antec, antec_new_lits );
+													sendLemma( ant, conc, "Conflict" );
+													return;
                                                 }
                                             } else {
                                                 Assert( other_str.getKind()!=kind::STRING_CONCAT );
                                                 antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
-                                                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( "ssym_$$", normal_forms[i][index_i].getType(), "created for split" );
-                                                // |sk| >= 0
-                                                //Node sk_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk );
-                                                //Node sk_len_geq_zero = NodeManager::currentNM()->mkNode( kind::GEQ, sk_len, d_zero);
-
-                                                Node eq1 = NodeManager::currentNM()->mkNode( kind::EQUAL, other_str, d_emptyString );
-                                                Node eq2_m = NodeManager::currentNM()->mkNode( kind::EQUAL, other_str,
-                                                            NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, firstChar, sk ) );
-                                                Node eq2 = eq2_m;//NodeManager::currentNM()->mkNode( kind::AND, eq2_m, sk_len_geq_zero );
-                                                conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 );
+												if( nconst_index_k==normal_forms[nconst_k].size()-1 ){
+													std::vector< Node > eqn;
+													for( unsigned r=0; r<2; r++ ){
+														int index_k = r==0 ? index_i : index_j;
+														int k = r==0 ? i : j;
+														std::vector< Node > eqnc;
+														for( unsigned index_l=index_k; index_l<normal_forms[k].size(); index_l++ ){
+															eqnc.push_back( normal_forms[k][index_l] );
+														}
+														eqn.push_back( mkConcat( eqnc ) );
+													}
+													conc = eqn[0].eqNode( eqn[1] );
+												}else{
+													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( "ssym_$$", normal_forms[i][index_i].getType(), "created for split" );
+
+													Node eq1 = NodeManager::currentNM()->mkNode( kind::EQUAL, other_str, d_emptyString );
+													Node eq2_m = NodeManager::currentNM()->mkNode( kind::EQUAL, other_str,
+																NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, firstChar, sk ) );
+													Node eq2 = eq2_m;//NodeManager::currentNM()->mkNode( kind::AND, eq2_m, sk_len_geq_zero );
+													conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 );
+												}
                                                 Trace("strings-solve-debug") << "Break normal form constant/variable " << std::endl;
-                                                sendLemma = true;
+
+												Node ant = mkExplain( antec, antec_new_lits );
+												sendLemma( ant, conc, "Constant Split" );
+												return;
                                             }
                                         }else{
                                             antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
@@ -979,33 +1001,18 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
                                             Node eq2 = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[j][index_j],
                                                         NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, normal_forms[i][index_i], sk ) );
                                             conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 );
-                                            sendLemma = true;
                                             // |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);
                                             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, "Split" );
+											return;
                                         }
                                     }
-                                    Trace("strings-solve-debug2") << "sendLemma/success : " << sendLemma << " " << success << std::endl;
-                                    if( sendLemma ){
-                                        Node ant = mkExplain( antec, antec_new_lits );
-                                        if( conc.isNull() ){
-                                            d_out->conflict(ant);
-                                            Trace("strings-conflict") << "CONFLICT : Strings conflict : " << ant << std::endl;
-                                            d_conflict = true;
-                                        }else{
-                                            Node lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, ant, conc );
-                                            Trace("strings-lemma") << "Strings compare lemma : " << lem << std::endl;
-                                            //d_out->lemma(lem);
-                                            d_lemma_cache.push_back( lem );
-                                        }
-                                        if( !loop_y.isNull() ){
-                                            addInductiveEquation( loop_x, loop_y, loop_z, ant );
-                                        }
-                                        return;
-                                    }
                                 }
                             }
                         }
@@ -1138,6 +1145,19 @@ void TheoryStrings::addInductiveEquation( Node x, Node y, Node z, Node exp ) {
     lste->push_back( exp );
 }
 
+void TheoryStrings::sendLemma( Node ant, Node conc, const char * c ) {
+	if( conc.isNull() ){
+		d_out->conflict(ant);
+		Trace("strings-conflict") << "CONFLICT : Strings conflict : " << ant << std::endl;
+		d_conflict = true;
+	}else{
+		Node lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, ant, conc );
+		Trace("strings-lemma") << "Strings " << c << " lemma : " << lem << std::endl;
+		//d_out->lemma(lem);
+		d_lemma_cache.push_back( lem );
+	}
+}
+
 Node TheoryStrings::mkConcat( std::vector< Node >& c ) {
     Node cc = c.size()>1 ? NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, c ) : ( c.size()==1 ? c[0] : d_emptyString );
 	return Rewriter::rewrite( cc );
@@ -1350,8 +1370,11 @@ bool TheoryStrings::checkCardinality() {
                 Node len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, cols[i][0] );
                 Node cons = NodeManager::currentNM()->mkNode( kind::GT, len, k_node );
                 Node lemma = NodeManager::currentNM()->mkNode( kind::IMPLIES, antc, cons );
-                Trace("strings-lemma") << "Strings cardinaliry lemma : " << lemma << std::endl;
-                d_out->lemma(lemma);
+				lemma = Rewriter::rewrite( lemma );
+				if( lemma!=d_true ){
+					Trace("strings-lemma") << "Strings cardinality lemma : " << lemma << std::endl;
+					d_out->lemma(lemma);
+				}
                 ei->d_cardinality_lem_k.set( int_k+1 );
                 return true;
             }
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index a566c944f..92cf33de2 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -113,7 +113,7 @@ class TheoryStrings : public Theory {
     eq::EqualityEngine d_equalityEngine;
     /** Are we in conflict */
     context::CDO<bool> d_conflict;
-
+	std::vector< Node > d_length_intro_vars;
     Node d_emptyString;
     Node d_true;
     Node d_false;
@@ -210,6 +210,7 @@ protected:
   //do pending merges
   void doPendingFacts();
 
+  void sendLemma( Node ant, Node conc, const char * c );
   /** mkConcat **/
   Node mkConcat( std::vector< Node >& c );
   /** mkExplain **/