Minor improvements, add endpoint eq inference to strings.

3 files changed, 33 insertions, 24 deletions

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index a19bab836..ad878e0f3 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -675,25 +675,22 @@ bool TheoryStrings::doPreprocess( Node atom ) {
       subs_rhs.push_back( d_true );
       Node sres = res.substitute( subs_lhs.begin(), subs_lhs.end(), subs_rhs.begin(), subs_rhs.end() );
       sres = Rewriter::rewrite( sres );
+      Node plem;
       if( sres!=res ){
-        Node plem = NodeManager::currentNM()->mkNode( kind::IMPLIES, atom, sres );
-        plem = Rewriter::rewrite( plem );
-        Trace("strings-assert") << "(assert " << plem << ")" << std::endl;
-        d_out->lemma( plem );
-        Trace("strings-pp-lemma") << "Preprocess impl lemma : " << plem << std::endl;
-        Trace("strings-pp-lemma") << "...from " << atom << std::endl;
+        plem = NodeManager::currentNM()->mkNode( kind::IMPLIES, atom, sres );
       }else{
         Trace("strings-assertion-debug") << "...preprocessed to : " << res << std::endl;
-        Node plem = NodeManager::currentNM()->mkNode( kind::IFF, atom, res );
-        plem = Rewriter::rewrite( plem );
-        Trace("strings-assert") << "(assert " << plem << ")" << std::endl;
-        d_out->lemma( plem );
-        Trace("strings-pp-lemma") << "Preprocess eq lemma : " << plem << std::endl;
-        Trace("strings-pp-lemma") << "...from " << atom << std::endl;
+        plem = NodeManager::currentNM()->mkNode( kind::IFF, atom, res );
         //reduced by preprocess
         addFact = false;
         d_preproc_cache[ atom ] = false;
       }
+      plem = Rewriter::rewrite( plem );
+      Trace("strings-assert") << "(assert " << plem << ")" << std::endl;
+      Trace("strings-lemma") << "Strings::Lemma " << plem << " by preprocess" << std::endl;
+      d_out->lemma( plem );
+      Trace("strings-pp-lemma") << "Preprocess reduce lemma : " << plem << std::endl;
+      Trace("strings-pp-lemma") << "...from " << atom << std::endl;
     }else{
       Trace("strings-assertion-debug") << "...preprocess ok." << std::endl;
     }
@@ -2420,6 +2417,8 @@ void TheoryStrings::checkNormalForms() {
                     }else{
                       Node cc = d_flat_form[b][count];
                       if( cc!=curr ){
+                        Node ac = a[d_flat_form_index[a][count]];
+                        Node bc = b[d_flat_form_index[b][count]];
                         inelig.push_back( b );
                         Assert( !areEqual( curr, cc ) );
                         Node cc_c = d_eqc_to_const[cc];
@@ -2428,20 +2427,22 @@ void TheoryStrings::checkNormalForms() {
                           int index;
                           Node s = TheoryStringsRewriter::splitConstant( cc_c, curr_c, index, r==1 );
                           if( s.isNull() ){
-                            addToExplanation( a[d_flat_form_index[a][count]], d_eqc_to_const_base[curr], exp );
+                            addToExplanation( ac, d_eqc_to_const_base[curr], exp );
                             addToExplanation( d_eqc_to_const_exp[curr], exp );
-                            addToExplanation( b[d_flat_form_index[b][count]], d_eqc_to_const_base[cc], exp );
+                            addToExplanation( bc, d_eqc_to_const_base[cc], exp );
                             addToExplanation( d_eqc_to_const_exp[cc], exp );
                             conc = d_false;
                             inf_type = 0;
                             break;
                           }
+                        }else if( (d_flat_form[a].size()-1)==count && (d_flat_form[b].size()-1)==count ){
+                          conc = ac.eqNode( bc );
+                          inf_type = 3;
+                          break;
                         }else{
                           //if lengths are the same, apply LengthEq
                           Node lcc = getLength( cc );
                           if( areEqual( lcurr, lcc ) ){
-                            Node ac = a[d_flat_form_index[a][count]];
-                            Node bc = b[d_flat_form_index[b][count]];
                             //exp_n.push_back( getLength( curr, true ).eqNode( getLength( cc, true ) ) );
                             addToExplanation( lcurr, lcc, exp );
                             if( !lcc.isConst() ){
@@ -2487,7 +2488,7 @@ void TheoryStrings::checkNormalForms() {
                   }
                 }
                 //if( exp_n.empty() ){
-                sendInfer( mkAnd( exp ), conc, inf_type==0? "F_Const" : ( inf_type==1 ? "F_LengthEq" : "F_Endpoint" ) );
+                sendInfer( mkAnd( exp ), conc, inf_type==0? "F_Const" : ( inf_type==1 ? "F_LengthEq" : ( inf_type==2 ? "F_Endpoint" : "F_EndpointEq" ) ) );
                 //}else{
                 //}
                 if( d_conflict ){
@@ -3894,7 +3895,7 @@ void TheoryStrings::checkExtendedFuncsEval( int effort ) {
       if( !var.empty() ){
         Node nr = n.substitute( var.begin(), var.end(), sub.begin(), sub.end() );
         Node nrc = Rewriter::rewrite( nr );
-        if( nrc.isConst() || hasTerm( nrc ) ){
+        if( nrc.isConst() ){
           //mark as reduced
           d_ext_func_terms[n] = false;
           Trace("strings-extf-debug") << "  resolvable by evaluation..." << std::endl;
@@ -3947,7 +3948,13 @@ void TheoryStrings::checkExtendedFuncsEval( int effort ) {
             }
           }
         }else{
-          Trace("strings-extf-debug") << "  cannot rewrite extf : " << nrc << std::endl;
+          if( effort==1 ){
+            Trace("strings-extf") << "  cannot rewrite extf : " << nrc << std::endl;
+          }
+        }
+      }else{
+        if( effort==1 ){
+          Trace("strings-extf") << "  cannot rewrite extf : " << n << std::endl;
         }
       }
     }
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 6efa048ca..fc17198c2 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -35,6 +35,8 @@ Node TheoryStringsRewriter::simpleRegexpConsume( std::vector< Node >& mchildren,
         do_next = false;
         Node xc = mchildren[mchildren.size()-1];
         Node rc = children[children.size()-1];
+        Assert( rc.getKind()!=kind::REGEXP_CONCAT );
+        Assert( xc.getKind()!=kind::STRING_CONCAT );
         if( rc.getKind() == kind::STRING_TO_REGEXP ){
           if( xc==rc[0] ){
             children.pop_back();
@@ -88,7 +90,7 @@ Node TheoryStringsRewriter::simpleRegexpConsume( std::vector< Node >& mchildren,
               std::vector< Node > mchildren_s;
               std::vector< Node > children_s;
               mchildren_s.push_back( xc );
-              children_s.push_back( rc[i] );
+              getConcat( rc[i], children_s );
               Node ret = simpleRegexpConsume( mchildren_s, children_s, t );
               if( !ret.isNull() ){
                 // one conjunct cannot be satisfied, return false
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 92f834bff..cde3aef1c 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -119,11 +119,12 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const
     // no good.  Instead, return the quantifier itself.  If we're in
     // checkModel(), and the quantifier actually matters, we'll get an
     // assert-fail since the quantifier isn't a constant.
-    if(!d_equalityEngine->hasTerm(Rewriter::rewrite(n))) {
+    Node nr = Rewriter::rewrite(n);
+    if(!d_equalityEngine->hasTerm(nr)) {
       d_modelCache[n] = ret;
       return ret;
     } else {
-      ret = Rewriter::rewrite(n);
+      ret = nr;
     }
   } else {
     if(n.getKind() == kind::LAMBDA) {
@@ -193,8 +194,7 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const
         ret = NodeManager::currentNM()->mkConst(getCardinality(ret[0].getType().toType()).getFiniteCardinality() <= ret[1].getConst<Rational>().getNumerator());
       }
       if(ret.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT ){
-        //FIXME
-        ret = NodeManager::currentNM()->mkConst(false);
+        //do nothing
       }
       d_modelCache[n] = ret;
       return ret;