removes unsound cases, adds unrolling

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 8af5430397f0f8909f752ab7a2afc9bf7acfb650..c84046570cde109b485febddf8d6340fcb9eaf18 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1619,15 +1619,15 @@ BV2NAT_TOK : 'bv2nat';
 INT2BV_TOK : 'int2bv';
 
 //STRING
-STRCST_TOK : 'str.const';
+//STRCST_TOK : 'str.cst';
 STRCON_TOK : 'str.++';
 STRLEN_TOK : 'str.len';
+//STRSUB_TOK : 'str.sub' ;
 STRINRE_TOK : 'str.in.re';
 STRTORE_TOK : 'str.to.re';
-//STRSUB_TOK : 'str.sub' ;
 RECON_TOK : 're.++';
 REOR_TOK : 're.or';
-REINTER_TOK : 're.inter';
+REINTER_TOK : 're.itr';
 RESTAR_TOK : 're.*';
 REPLUS_TOK : 're.+';
 REOPT_TOK : 're.opt';

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 91eae8915c84c1baa9d7dc9a9479ef22b3fe4a1b..201302baf847656bacb2a7bcd5c273bccaa0596a 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -75,6 +75,7 @@
 #include "theory/quantifiers/macros.h"
 #include "theory/datatypes/options.h"
 #include "theory/quantifiers/first_order_reasoning.h"
+#include "theory/strings/theory_strings_preprocess.h"
 
 using namespace std;
 using namespace CVC4;
@@ -2855,6 +2856,14 @@ void SmtEnginePrivate::processAssertions() {
 
   // Assertions ARE guaranteed to be rewritten by this point
 
+  if( d_smt.d_logic.isTheoryEnabled(THEORY_STRINGS) ){
+       CVC4::theory::strings::StringsPreprocess sp;
+       sp.simplify( d_assertionsToPreprocess );
+    for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
+               d_assertionsToPreprocess[i] = Rewriter::rewrite( d_assertionsToPreprocess[i] );
+       }
+  }
+
   dumpAssertions("pre-skolem-quant", d_assertionsToPreprocess);
   if( options::preSkolemQuant() ){
     //apply pre-skolemization to existential quantifiers

diff --git a/src/theory/strings/Makefile.am b/src/theory/strings/Makefile.am
index 15bd04b8827927dfa876f3319d86ef0d8a0c5162..38efa33f31f36c162ef1be733e8d9e3fc0ba26cc 100644 (file)
--- a/src/theory/strings/Makefile.am
+++ b/src/theory/strings/Makefile.am
@@ -11,7 +11,9 @@ libstrings_la_SOURCES = \
        theory_strings_rewriter.h \
        theory_strings_rewriter.cpp \
        theory_strings_type_rules.h \
-       type_enumerator.h
+       type_enumerator.h \
+       theory_strings_preprocess.h \
+       theory_strings_preprocess.cpp
 
 EXTRA_DIST = \
        kinds

diff --git a/src/theory/strings/options b/src/theory/strings/options
index c90d654b17ed0192065a7adb18af18f7415458e6..9226f99993d9e2836f195c1425a45d866d3518eb 100644 (file)
--- a/src/theory/strings/options
+++ b/src/theory/strings/options
@@ -5,7 +5,7 @@
 
 module STRINGS "theory/strings/options.h" Strings theory
 
-option stringCharCardinality str-cardinality --str-cardinality=N int16_t :default 256 :read-write
+option stringCharCardinality str-alphabet-card --str-alphabet-card=N int16_t :default 256 :read-write
  the cardinality of the characters used by the theory of string, default 256
 
 endmodule

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index df55bcf838fed816741f1d1052b863df11feec14..f9bb74486e692e4b0ecd4aa07f5163f2c288e450 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -26,6 +26,8 @@
 #include "theory/strings/type_enumerator.h"
 #include <cmath>
 
+#define STR_UNROLL_INDUCTION
+
 using namespace std;
 using namespace CVC4::context;
 
@@ -44,7 +46,10 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu
     d_ind_map1(c),
     d_ind_map2(c),
     d_ind_map_exp(c),
-    d_ind_map_lemma(c)
+    d_ind_map_lemma(c),
+       //d_lit_to_decide_index( c, 0 ),
+       //d_lit_to_decide( c ),
+       d_lit_to_unroll( c )
 {
     // The kinds we are treating as function application in congruence
     d_equalityEngine.addFunctionKind(kind::STRING_IN_REGEXP);
@@ -63,6 +68,14 @@ TheoryStrings::~TheoryStrings() {
 
 }
 
+Node TheoryStrings::getRepresentative( Node t ) {
+       if( d_equalityEngine.hasTerm( t ) ){
+               return d_equalityEngine.getRepresentative( t );
+       }else{
+               return t;
+       }
+}
+
 void TheoryStrings::setMasterEqualityEngine(eq::EqualityEngine* eq) {
   d_equalityEngine.setMasterEqualityEngine(eq);
 }
@@ -182,7 +195,7 @@ void TheoryStrings::collectModelInfo( TheoryModel* m, bool fullModel ) {
             Node cst = ei ? ei->d_const_term : Node::null();
                        if( cst.isNull() ){
                                Assert( d_normal_forms.find( col[i][j] )!=d_normal_forms.end() );
-                               if( d_normal_forms[col[i][j]].size()==1 && d_normal_forms[col[i][j]][0]==col[i][j] ){
+                               if( d_normal_forms[col[i][j]].size()==1 ){//&& d_normal_forms[col[i][j]][0]==col[i][j] ){
                                        pure_eq.push_back( col[i][j] );
                                }
                        }else{
@@ -218,10 +231,21 @@ void TheoryStrings::collectModelInfo( TheoryModel* m, bool fullModel ) {
        for( unsigned i=0; i<nodes.size(); i++ ){
                if( processed.find( nodes[i] )==processed.end() ){
                        Assert( d_normal_forms.find( nodes[i] )!=d_normal_forms.end() );
+                       Trace("strings-model") << "Construct model for " << nodes[i] << " based on normal form ";
+                       for( unsigned j=0; j<d_normal_forms[nodes[i]].size(); j++ ) {
+                               if( j>0 ) Trace("strings-model") << " ++ ";
+                               Trace("strings-model") << d_normal_forms[nodes[i]][j];
+                               Node r = getRepresentative( d_normal_forms[nodes[i]][j] );
+                               if( !r.isConst() && processed.find( r )==processed.end() ){
+                                       Trace("strings-model") << "(UNPROCESSED)";
+                               }
+                       }
+                       Trace("strings-model") << std::endl;
                        std::vector< Node > nc;
                        for( unsigned j=0; j<d_normal_forms[nodes[i]].size(); j++ ) {
-                               Assert( processed.find( d_normal_forms[nodes[i]][j] )!=processed.end() );
-                               nc.push_back(processed[d_normal_forms[nodes[i]][j]]);
+                               Node r = getRepresentative( d_normal_forms[nodes[i]][j] );
+                               Assert( r.isConst() || processed.find( r )!=processed.end() );
+                               nc.push_back(r.isConst() ? r : processed[r]);
                        }
                        Node cc = mkConcat( nc );
                        Assert( cc.getKind()==kind::CONST_STRING );
@@ -295,33 +319,16 @@ void TheoryStrings::check(Effort e) {
     polarity = fact.getKind() != kind::NOT;
     atom = polarity ? fact : fact[0];
     if (atom.getKind() == kind::EQUAL) {
-      //head
-      //if(atom[0].getKind() == kind::CONST_STRING) {
-          //if(atom[1].getKind() == kind::STRING_CONCAT) {
-          //}
-      //}
-      //tail
       d_equalityEngine.assertEquality(atom, polarity, fact);
     } else {
       d_equalityEngine.assertPredicate(atom, polarity, fact);
     }
-    switch(atom.getKind()) {
-        case kind::EQUAL:
-            if(polarity) {
-                //if(atom[0].isString() && atom[1].isString()) {
-                    //dealPositiveWordEquation(atom);
-                //}
-            } else {
-                // TODO: Word Equation negaitive
-            }
-            break;
-        case kind::STRING_IN_REGEXP:
-            // TODO: membership
-            break;
-        default:
-            //possibly error
-            break;
-    }
+#ifdef STR_UNROLL_INDUCTION
+       //check if it is a literal to unroll?
+       if( d_lit_to_unroll.find( atom )!=d_lit_to_unroll.end() ){
+               Trace("strings-ind") << "Strings-ind : Possibly unroll for : " << atom << ", polarity = " << polarity << std::endl;
+       }
+#endif
   }
   doPendingFacts();
 
@@ -607,9 +614,11 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
         //nf.push_back( eqc );
         if( eqc.getKind()==kind::STRING_CONCAT ){
             for( unsigned i=0; i<eqc.getNumChildren(); i++ ){
-                nf.push_back( eqc[i] );
+                               if( !d_equalityEngine.hasTerm(d_emptyString) || !d_equalityEngine.areEqual( eqc[i], d_emptyString ) ){
+                                       nf.push_back( eqc[i] );
+                               }
             }
-        }else{
+        }else if( !d_equalityEngine.hasTerm(d_emptyString) || !d_equalityEngine.areEqual( eqc, d_emptyString ) ){
             nf.push_back( eqc );
         }
         Trace("strings-process") << "Return process equivalence class " << eqc << " : already visited." << std::endl;
@@ -665,7 +674,10 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
                                 addNormalFormPair( normal_form_src[i], normal_form_src[j] );
                                 //add loop equations that we've accumulated
                                 for( unsigned r=0; r<loop_eqs_x.size(); r++ ){
-                                    addInductiveEquation( loop_eqs_x[r], loop_eqs_y[r], loop_eqs_z[r], loop_exps[r] );
+                                    if( addInductiveEquation( loop_eqs_x[r], loop_eqs_y[r], loop_eqs_z[r], loop_exps[r], "Discovered Loop Induction" ) ){
+                                                                               //added a lemma, we are done
+                                                                               return;
+                                                                       }
                                 }
                             }else{
                                 //the remainder must be empty
@@ -684,7 +696,6 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
                                     Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, d_emptyString, normal_forms[k][index_k] );
                                     Trace("strings-lemma") << "Strings : Infer " << eq << " from " << eq_exp << std::endl;
                                                                        Assert( !d_equalityEngine.areEqual( d_emptyString, normal_forms[k][index_k] ) );
-                                    //d_equalityEngine.assertEquality( eq, true, eq_exp );
                                     d_pending.push_back( eq );
                                     d_pending_exp[eq] = eq_exp;
                                     d_infer.push_back(eq);
@@ -737,8 +748,29 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
                                     d_infer.push_back(eq);
                                     d_infer_exp.push_back(eq_exp);
                                     return;
-                                }else{
-                                    Trace("strings-solve-debug") << "Case 3 : must compare strings" << std::endl;
+                                                               }else if( ( normal_forms[i][index_i].getKind()!=kind::CONST_STRING && index_i==normal_forms[i].size()-1 ) || 
+                                                                                 ( normal_forms[j][index_j].getKind()!=kind::CONST_STRING && index_j==normal_forms[j].size()-1 ) ){
+                                                                       Trace("strings-solve-debug") << "Case 3 : at endpoint" << std::endl;
+                                    Node conc;
+                                    std::vector< Node > antec;
+                                                                       antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
+                                    std::vector< Node > antec_new_lits;
+                                                                       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] );
+                                                                       Node ant = mkExplain( antec, antec_new_lits );
+                                                                       sendLemma( ant, conc, "Endpoint" );
+                                                                       return;
+                                                               }else{
+                                    Trace("strings-solve-debug") << "Case 4 : must compare strings" << std::endl;
                                     Node conc;
                                     std::vector< Node > antec;
                                     std::vector< Node > antec_new_lits;
@@ -787,7 +819,7 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
                                                                                }
                                                                                term_s = mkConcat( sc );
                                                                                Trace("strings-loop") << "Find y,z from t,s = " << term_t << ", " << term_s << std::endl;
-                                                                               /*TODO: incomplete start */
+                                                                               /*TODO: incomplete start 
                                                                                if( term_t==term_s ){
                                                                                        found_size_y = -2;
                                                                                }else if( term_t.getKind()==kind::STRING_CONCAT && term_s.getKind()==kind::STRING_CONCAT ){
@@ -820,12 +852,12 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
                                                                                                }
                                                                                        }
                                                                                }
-                                                                               /*TODO: end incomplete*/
+                                                                               TODO: end incomplete*/
                                         if( found_size_y==-1 ){
                                                                                        Trace("strings-loop") << "Must add lemma." << std::endl;
                                             //need to break
-                                            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" );
+                                            Node sk_y= NodeManager::currentNM()->mkSkolem( "ysym_$$", normal_forms[i][index_i].getType(), "created for loop detection split" );
+                                            Node sk_z= NodeManager::currentNM()->mkSkolem( "zsym_$$", normal_forms[i][index_i].getType(), "created for loop detection split" );
 
                                             antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
                                             //t1 * ... * tn = y * z
@@ -864,31 +896,16 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
                                                                                        //Node len_x_gt_len_y = NodeManager::currentNM()->mkNode( kind::GT, 
                                                                                        //                                              NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, normal_forms[other_n_index][other_index]),
                                                                                        //                                              sk_y_len );
-                                            //Node sk_x_rest = NodeManager::currentNM()->mkSkolem( "ldissym_$$", normal_forms[i][index_i].getType(), "created for induction" );
-                                                                                       //Node x_eq_y_rest = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[other_n_index][other_index], 
-                                                                                       //                                              NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk_y, sk_x_rest ) );
-                                                                                       
+                                                                                       Node ant = mkExplain( antec, antec_new_lits );
                                                                                        conc = NodeManager::currentNM()->mkNode( kind::AND, conc1, conc2 );//, x_eq_y_rest );// , z_neq_empty //, len_x_gt_len_y
+
                                                                                        //Node x_eq_empty = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[other_n_index][other_index], d_emptyString);
                                                                                        //conc = NodeManager::currentNM()->mkNode( kind::OR, x_eq_empty, conc );
 
-                                            
-                                                                                       Node loop_x = normal_forms[other_n_index][other_index];
-                                                                                       Node loop_y = sk_y;
-                                                                                       Node loop_z = sk_z;
-
-                                                                                       //Node loop_x = sk_x_rest;
-                                                                                       //std::vector< Node > skc;
-                                                                                       //skc.push_back( sk_y );
-                                                                                       //skc.push_back( sk_z );
-                                            //Node loop_y = d_emptyString;
-                                            //Node loop_z = mkConcat( skc );
-
                                             //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 );
+                                                                                       addInductiveEquation( normal_forms[other_n_index][other_index], sk_y, sk_z, ant, "Loop Induction" );
                                                                                        return;
                                         } else {
                                                                                        // x = (yz)*y
@@ -970,30 +987,16 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
                                             } else {
                                                 Assert( other_str.getKind()!=kind::STRING_CONCAT );
                                                 antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
-                                                                                               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 );
-                                                                                               }
+                                                                                               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;
 
                                                                                                Node ant = mkExplain( antec, antec_new_lits );
@@ -1002,25 +1005,26 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
                                             }
                                         }else{
                                             antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
-                                            Node ldeq = NodeManager::currentNM()->mkNode( kind::EQUAL, length_term_i, length_term_j ).negate();
-                                            if( d_equalityEngine.areDisequal( length_term_i, length_term_j, true ) ){
-                                                antec.push_back( ldeq );
-                                            }else{
-                                                antec_new_lits.push_back(ldeq);
-                                            }
-                                            Node sk = NodeManager::currentNM()->mkSkolem( "ssym_$$", normal_forms[i][index_i].getType(), "created for 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 ) );
-                                            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 ldeq = NodeManager::currentNM()->mkNode( kind::EQUAL, length_term_i, length_term_j ).negate();
+                                                                                       if( d_equalityEngine.areDisequal( length_term_i, length_term_j, true ) ){
+                                                                                               antec.push_back( ldeq );
+                                                                                       }else{
+                                                                                               antec_new_lits.push_back(ldeq);
+                                                                                       }
+                                                                                       Node sk = NodeManager::currentNM()->mkSkolem( "ssym_$$", normal_forms[i][index_i].getType(), "created for 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 ) );
+                                                                                       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 );
+                                                                                       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" );
@@ -1120,8 +1124,39 @@ bool TheoryStrings::isNormalFormPair2( Node n1, Node n2 ) {
   return false;
 }
 
-void TheoryStrings::addInductiveEquation( Node x, Node y, Node z, Node exp ) {
+bool TheoryStrings::addInductiveEquation( Node x, Node y, Node z, Node exp, const char * c ) {
     Trace("strings-solve-debug") << "add inductive equation for " << x << " = (" << y << " " << z << ")* " << y << std::endl;
+#ifdef STR_UNROLL_INDUCTION
+       Node w = NodeManager::currentNM()->mkSkolem( "wsym_$$", x.getType(), "created for induction" );
+       Node x_eq_y_w = NodeManager::currentNM()->mkNode( kind::EQUAL, x, 
+                                                       NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, y, w ) );
+       Node lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, x_eq_y_w );
+       Trace("strings-lemma") << "Strings " << c << " lemma : " << lem << std::endl;
+       d_lemma_cache.push_back( lem );
+
+       //add initial induction
+       Node lit1 = w.eqNode( d_emptyString );
+       lit1 = Rewriter::rewrite( lit1 );
+       Node wp = NodeManager::currentNM()->mkSkolem( "wpsym_$$", x.getType(), "created for induction" );
+       Node lit2 = w.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, z, y, wp ) );
+       lit2 = Rewriter::rewrite( lit2 );
+       Node split_lem = NodeManager::currentNM()->mkNode( kind::OR, lit1, lit2 );
+       Trace("strings-ind") << "Strings : Lemma " << c << " for unrolling " << split_lem << std::endl;
+       Trace("strings-lemma") << "Strings : Lemma " << c << " for unrolling " << split_lem << std::endl;
+       d_lemma_cache.push_back( split_lem );
+
+       //d_lit_to_decide.push_back( lit1 );
+       d_lit_to_unroll[lit2] = true;
+       d_pending_req_phase[lit1] = true;
+       d_pending_req_phase[lit2] = false;
+
+       x = w;
+       std::vector< Node > skc;
+       skc.push_back( y );
+       skc.push_back( z );
+       y = d_emptyString;
+       z = mkConcat( skc );
+#endif
 
     NodeListMap::iterator itr_x_y = d_ind_map1.find(x);
     NodeList* lst1;
@@ -1157,6 +1192,11 @@ void TheoryStrings::addInductiveEquation( Node x, Node y, Node z, Node exp ) {
     lst1->push_back( y );
     lst2->push_back( z );
     lste->push_back( exp );
+#ifdef STR_UNROLL_INDUCTION
+       return true;
+#else
+       return false;
+#endif
 }
 
 void TheoryStrings::sendLemma( Node ant, Node conc, const char * c ) {
@@ -1268,6 +1308,7 @@ bool TheoryStrings::checkNormalForms() {
 
   bool addedFact = false;
   do {
+         Trace("strings-process") << "Check Normal Forms........next round" << std::endl;
     //calculate normal forms for each equivalence class, possibly adding splitting lemmas
     d_normal_forms.clear();
     d_normal_forms_exp.clear();
@@ -1275,11 +1316,12 @@ bool TheoryStrings::checkNormalForms() {
     std::map< Node, Node > eqc_to_exp;
       eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
       d_lemma_cache.clear();
+          d_pending_req_phase.clear();
       while( !eqcs_i.isFinished() ){
         Node eqc = (*eqcs_i);
         //if eqc.getType is string
         if (eqc.getType().isString()) {
-            Trace("strings-process") << "Verify normal forms are the same for " << eqc << std::endl;
+            Trace("strings-process") << "- Verify normal forms are the same for " << eqc << std::endl;
             std::vector< Node > visited;
             std::vector< Node > nf;
             std::vector< Node > nf_exp;
@@ -1319,16 +1361,25 @@ bool TheoryStrings::checkNormalForms() {
         }
         ++eqcs_i;
       }
+         Trace("strings-nf-debug") << "**** Normal forms are : " << std::endl;
+         for( std::map< Node, Node >::iterator it = nf_to_eqc.begin(); it != nf_to_eqc.end(); ++it ){
+               Trace("strings-nf-debug") << "  normal_form(" << it->second << ") = " << it->first << std::endl;
+         }
+         Trace("strings-nf-debug") << std::endl;
       addedFact = !d_pending.empty();
       doPendingFacts();
       if( !d_conflict ){
-          for( unsigned i=0; i<d_lemma_cache.size(); i++ ){
-              Trace("strings-pending") << "Process pending lemma : " << d_lemma_cache[i] << std::endl;
-              d_out->lemma( d_lemma_cache[i] );
-          }
           if( !d_lemma_cache.empty() ){
-            d_lemma_cache.clear();
-            return true;
+                         for( unsigned i=0; i<d_lemma_cache.size(); i++ ){
+                                 Trace("strings-pending") << "Process pending lemma : " << d_lemma_cache[i] << std::endl;
+                                 d_out->lemma( d_lemma_cache[i] );
+                         }
+                         for( std::map< Node, bool >::iterator it = d_pending_req_phase.begin(); it != d_pending_req_phase.end(); ++it ){
+                               d_out->requirePhase( it->first, it->second );
+                         }
+                       d_lemma_cache.clear();
+                   d_pending_req_phase.clear();
+                       return true;
           }
       }
   } while (!d_conflict && addedFact);
@@ -1428,6 +1479,7 @@ bool TheoryStrings::checkInductiveEquations() {
     Trace("strings-ind")  << "We are sat, with these inductive equations : " << std::endl;
     for( NodeListMap::const_iterator it = d_ind_map1.begin(); it != d_ind_map1.end(); ++it ){
         Node x = (*it).first;
+               Trace("strings-ind-debug") << "Check eq for " << x << std::endl;
         NodeList* lst1 = (*it).second;
         NodeList* lst2 = (*d_ind_map2.find(x)).second;
         NodeList* lste = (*d_ind_map_exp.find(x)).second;
@@ -1439,21 +1491,25 @@ bool TheoryStrings::checkInductiveEquations() {
         while( i1!=lst1->end() ){
             Node y = *i1;
             Node z = *i2;
+                       //Trace("strings-ind-debug") << "Check y=" << y << " , z=" << z << std::endl;
             //if( il==lstl->end() ) {
                                std::vector< Node > nf_y, nf_z, exp_y, exp_z;
                                
-                               getFinalNormalForm( y, nf_y, exp_y);
-                               getFinalNormalForm( z, nf_z, exp_z);
-                               std::vector< Node > vec_empty;
-                               Node nexp_y = mkExplain( exp_y, vec_empty );
-                               Node nexp_z = mkExplain( exp_z, vec_empty );
+                               //getFinalNormalForm( y, nf_y, exp_y);
+                               //getFinalNormalForm( z, nf_z, exp_z);
+                               //std::vector< Node > vec_empty;
+                               //Node nexp_y = mkExplain( exp_y, vec_empty );
+                               //Trace("strings-ind-debug") << "Check nexp_y=" << nexp_y << std::endl;
+                               //Node nexp_z = mkExplain( exp_z, vec_empty );
 
-                               Node exp = *ie;
+                               //Node exp = *ie;
+                               //Trace("strings-ind-debug") << "Check exp=" << exp << std::endl;
 
-                               exp = NodeManager::currentNM()->mkNode( kind::AND, exp, nexp_y, nexp_z );
-                               exp = Rewriter::rewrite( exp );
+                               //exp = NodeManager::currentNM()->mkNode( kind::AND, exp, nexp_y, nexp_z );
+                               //exp = Rewriter::rewrite( exp );
 
-                               Trace("strings-ind") << "Inductive equation : " << x << " = ( ";
+                               Trace("strings-ind") << "Inductive equation : " << x << " = ( " << y << " ++ " << z << " )* " << y << std::endl;
+                               /*
                                for( std::vector< Node >::const_iterator itr = nf_y.begin(); itr != nf_y.end(); ++itr) {
                                        Trace("strings-ind") << (*itr) << " ";
                                }
@@ -1466,6 +1522,7 @@ bool TheoryStrings::checkInductiveEquations() {
                                        Trace("strings-ind") << (*itr) << " ";
                                }
                                Trace("strings-ind") << std::endl;
+                               */
                                /*
                                Trace("strings-ind") << "Explanation is : " << exp << std::endl;
                                std::vector< Node > nf_yz;
@@ -1520,12 +1577,17 @@ bool TheoryStrings::checkInductiveEquations() {
             ++i2;
             ++ie;
             //++il;
-            hasEq = true;
+                       if( !d_equalityEngine.hasTerm( d_emptyString ) || !d_equalityEngine.areEqual( y, d_emptyString ) || !d_equalityEngine.areEqual( x, d_emptyString ) ){
+                               hasEq = true;
+                       }
         }
     }
     if( hasEq ){
+               Trace("strings-ind") << "It is incomplete." << std::endl;
         d_out->setIncomplete();
-    }
+    }else{
+               Trace("strings-ind") << "We can answer SAT." << std::endl;
+       }
   return false;
 }
 
@@ -1601,7 +1663,18 @@ void TheoryStrings::seperateIntoCollections( std::vector< Node >& n, std::vector
   }
 }
 
-
+/*
+Node TheoryStrings::getNextDecisionRequest() {
+       if( d_lit_to_decide_index.get()<d_lit_to_decide.size() ){
+               Node l = d_lit_to_decide[d_lit_to_decide_index.get()];
+               d_lit_to_decide_index.set( d_lit_to_decide_index.get() + 1 );
+               Trace("strings-ind") << "Strings-ind : decide on " << l << std::endl;
+               return l;
+       }else{
+               return Node::null();
+       }
+}
+*/
 }/* CVC4::theory::strings namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */

diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 92cf33de2761a851e2d505304a4930003dc0878b..2385386ea97a7d75fb55274c6d7e58eb4522ea26 100644 (file)
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -36,6 +36,7 @@ namespace strings {
 class TheoryStrings : public Theory {
   typedef context::CDChunkList<Node> NodeList;
   typedef context::CDHashMap<Node, NodeList*, NodeHashFunction> NodeListMap;
+  typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
   public:
 
   TheoryStrings(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe);
@@ -45,7 +46,7 @@ class TheoryStrings : public Theory {
 
   std::string identify() const { return std::string("TheoryStrings"); }
 
-
+  Node getRepresentative( Node t );
   public:
 
   void propagate(Effort e);
@@ -122,6 +123,8 @@ class TheoryStrings : public Theory {
       std::map< Node, Node > d_pending_exp;
       std::vector< Node > d_pending;
       std::vector< Node > d_lemma_cache;
+         std::map< Node, bool > d_pending_req_phase;
+
   bool hasTerm( Node a );
   bool areEqual( Node a, Node b );
   /** inferences */
@@ -137,7 +140,11 @@ class TheoryStrings : public Theory {
   NodeListMap d_ind_map2;
   NodeListMap d_ind_map_exp;
   NodeListMap d_ind_map_lemma;
-  void addInductiveEquation( Node x, Node y, Node z, Node exp );
+  bool addInductiveEquation( Node x, Node y, Node z, Node exp, const char * c );
+
+  //for unrolling inductive equations
+  NodeBoolMap d_lit_to_unroll;
+
 
   /////////////////////////////////////////////////////////////////////////////
   // MODEL GENERATION

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
new file mode 100644 (file)
index 0000000..d62fd4c
--- /dev/null
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -0,0 +1,120 @@
+/*********************                                                        */\r
+/*! \file theory_strings_preprocess.cpp\r
+ ** \verbatim\r
+ ** Original author: Tianyi Liang\r
+ ** Major contributors: Tianyi Liang, Andrew Reynolds\r
+ ** Minor contributors (to current version): none\r
+ ** This file is part of the CVC4 prototype.\r
+ ** Copyright (c) 2013-2013  New York University and The University of Iowa\r
+ ** See the file COPYING in the top-level source directory for licensing\r
+ ** information.\endverbatim\r
+ **\r
+ ** \brief Strings Preprocess\r
+ **\r
+ ** Strings Preprocess.\r
+ **/\r
+\r
+#include "theory/strings/theory_strings_preprocess.h"\r
+#include "expr/kind.h"\r
+\r
+namespace CVC4 {\r
+namespace theory {\r
+namespace strings {\r
+\r
+void StringsPreprocess::simplifyRegExp( Node s, Node r, std::vector< Node > &ret ) {\r
+       int k = r.getKind();\r
+       switch( k ) {\r
+               case kind::STRING_TO_REGEXP:\r
+               {\r
+                       Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, s, r[0] );\r
+                       ret.push_back( eq );\r
+               }\r
+                       break;\r
+               case kind::REGEXP_CONCAT:\r
+               {\r
+                       std::vector< Node > cc;\r
+                       for(unsigned i=0; i<r.getNumChildren(); ++i) {\r
+                               Node sk = NodeManager::currentNM()->mkSkolem( "recsym_$$", s.getType(), "created for regular expression concat" );\r
+                               simplifyRegExp( sk, r[i], ret );\r
+                               cc.push_back( sk );\r
+                       }\r
+                       Node cc_eq = NodeManager::currentNM()->mkNode( kind::EQUAL, s, \r
+                                               NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, cc ) );\r
+                       ret.push_back( cc_eq );\r
+               }\r
+                       break;\r
+               case kind::REGEXP_OR:\r
+               {\r
+                       std::vector< Node > c_or;\r
+                       for(unsigned i=0; i<r.getNumChildren(); ++i) {\r
+                               simplifyRegExp( s, r[i], c_or );\r
+                       }\r
+                       Node eq = NodeManager::currentNM()->mkNode( kind::OR, c_or );\r
+                       ret.push_back( eq );\r
+               }\r
+                       break;\r
+               case kind::REGEXP_INTER:\r
+                       for(unsigned i=0; i<r.getNumChildren(); ++i) {\r
+                               simplifyRegExp( s, r[i], ret );\r
+                       }\r
+                       break;\r
+               case kind::REGEXP_STAR:\r
+               {\r
+                       Node sk = NodeManager::currentNM()->mkSkolem( "ressym_$$", s.getType(), "created for regular expression star" );\r
+                       Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL,\r
+                                               NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk, s ),\r
+                                               NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, s, sk ));\r
+                       ret.push_back( eq );\r
+                       simplifyRegExp( sk, r[0], ret );\r
+               }\r
+                       break;\r
+               case kind::REGEXP_OPT:\r
+               {\r
+                       Node eq_empty = NodeManager::currentNM()->mkNode( kind::EQUAL, s, NodeManager::currentNM()->mkConst( ::CVC4::String("") ) );\r
+                       std::vector< Node > rr;\r
+                       simplifyRegExp( s, r[0], rr );\r
+                       Node nrr = rr.size()==1 ? rr[0] : NodeManager::currentNM()->mkNode( kind::AND, rr );\r
+                       ret.push_back( NodeManager::currentNM()->mkNode( kind::OR, eq_empty, nrr) );\r
+               }\r
+                       break;\r
+               default:\r
+                       //TODO:case kind::REGEXP_PLUS:\r
+                       //TODO: special sym: sigma, none, all\r
+                       break;\r
+       }\r
+}\r
+\r
+Node StringsPreprocess::simplify( Node t ) {\r
+       if( t.getKind() == kind::STRING_IN_REGEXP ){\r
+               // t0 in t1\r
+               //rewrite it\r
+               std::vector< Node > ret;\r
+               simplifyRegExp( t[0], t[1], ret );\r
+\r
+               return ret.size() == 1 ? ret[0] : NodeManager::currentNM()->mkNode( kind::AND, ret );\r
+    }else if( t.getNumChildren()>0 ){\r
+               std::vector< Node > cc;\r
+               if (t.getMetaKind() == kind::metakind::PARAMETERIZED) {\r
+                       cc.push_back(t.getOperator());\r
+               }\r
+               bool changed = false;\r
+               for( unsigned i=0; i<t.getNumChildren(); i++ ){\r
+                       Node tn = simplify( t[i] );\r
+                       cc.push_back( tn );\r
+                       changed = changed || tn!=t[i];\r
+               }\r
+               return changed ? NodeManager::currentNM()->mkNode( t.getKind(), cc ) : t;\r
+       }else{\r
+               return t;\r
+       }\r
+}\r
+\r
+void StringsPreprocess::simplify(std::vector< Node > &vec_node) {\r
+       for( unsigned i=0; i<vec_node.size(); i++ ){\r
+               vec_node[i] = simplify( vec_node[i] );\r
+       }\r
+}\r
+\r
+}/* CVC4::theory::strings namespace */\r
+}/* CVC4::theory namespace */\r
+}/* CVC4 namespace */\r

diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h
new file mode 100644 (file)
index 0000000..2b2e7df
--- /dev/null
+++ b/src/theory/strings/theory_strings_preprocess.h
@@ -0,0 +1,41 @@
+/*********************                                                        */\r
+/*! \file theory_strings_preprocess.h\r
+ ** \verbatim\r
+ ** Original author: Tianyi Liang\r
+ ** Major contributors: Tianyi Liang, Andrew Reynolds\r
+ ** Minor contributors (to current version): none\r
+ ** This file is part of the CVC4 prototype.\r
+ ** Copyright (c) 2013-2013  New York University and The University of Iowa\r
+ ** See the file COPYING in the top-level source directory for licensing\r
+ ** information.\endverbatim\r
+ **\r
+ ** \brief Strings Preprocess\r
+ **\r
+ ** Strings Preprocess.\r
+ **/\r
+\r
+#include "cvc4_private.h"\r
+\r
+#ifndef __CVC4__THEORY__STRINGS__PREPROCESS_H\r
+#define __CVC4__THEORY__STRINGS__PREPROCESS_H\r
+\r
+#include <vector>\r
+#include "theory/theory.h"\r
+\r
+namespace CVC4 {\r
+namespace theory {\r
+namespace strings {\r
+\r
+class StringsPreprocess {\r
+private:\r
+       void simplifyRegExp( Node s, Node r, std::vector< Node > &ret );\r
+       Node simplify( Node t );\r
+public:\r
+void simplify(std::vector< Node > &vec_node);\r
+};\r
+\r
+}/* CVC4::theory::strings namespace */\r
+}/* CVC4::theory namespace */\r
+}/* CVC4 namespace */\r
+\r
+#endif /* __CVC4__THEORY__STRINGS__PREPROCESS_H */\r

diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h
index bf284ea7bb218aa06e478467110cfdd96fefb460..9c3d6c71e6c4f7e1832705590680c517ab03c8e9 100644 (file)
--- a/src/theory/strings/theory_strings_type_rules.h
+++ b/src/theory/strings/theory_strings_type_rules.h
@@ -181,6 +181,9 @@ public:
     if (!t.isString()) {
       throw TypeCheckingExceptionPrivate(n, "expecting string terms");
     }
+       if( (*it).getKind() != kind::CONST_STRING ) {
+      throw TypeCheckingExceptionPrivate(n, "expecting constant string terms");
+       }
     if(++it != it_end) {
       throw TypeCheckingExceptionPrivate(n, "too many terms");
     }

diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am
index 699a7ff3c3d172fbb9f886a1948ef84c8ebd11c7..2b0954cad0a04af371fa35432305eb1b8d9a5aaf 100644 (file)
--- a/test/regress/regress0/strings/Makefile.am
+++ b/test/regress/regress0/strings/Makefile.am
@@ -26,11 +26,13 @@ TESTS =     \
   str004.smt2 \
   str005.smt2 \
   model001.smt2 \
-  loop001.smt2
-# loop002.smt2 \
-# loop003.smt2 \
-# loop004.smt2 \
-# loop005.smt2 \
+  loop001.smt2 \
+  loop002.smt2 \
+  loop003.smt2 \
+  loop007.smt2
+
+# loop004.smt2
+# loop005.smt2
 # loop006.smt2
 
 FAILING_TESTS =

diff --git a/test/regress/regress0/strings/cardinality.smt2 b/test/regress/regress0/strings/cardinality.smt2
index 5c4771d713003988d57114fa67691b51a1943c1c..2baac51ce1339d9decab1c5c1d995c5e48ae0ee7 100644 (file)
--- a/test/regress/regress0/strings/cardinality.smt2
+++ b/test/regress/regress0/strings/cardinality.smt2
@@ -1,7 +1,7 @@
 (set-logic ALL_SUPPORTED)
 (set-info :status unsat)
 
-(set-option :str-cardinality 2)
+(set-option :str-alphabet-card 2)
 
 (declare-fun x () String)
 (declare-fun y () String)

diff --git a/test/regress/regress0/strings/loop002.smt2 b/test/regress/regress0/strings/loop002.smt2
index a47b959f5d08e3fdee6058cc0e35c07e82638481..2f96241dc3e220176e6b8618bcf1a2f19a08fdd8 100644 (file)
--- a/test/regress/regress0/strings/loop002.smt2
+++ b/test/regress/regress0/strings/loop002.smt2
@@ -1,16 +1,9 @@
-; COMMAND-LINE: --no-check-models
-; EXPECT: sat
-; EXIT: 10
-;
 (set-logic ALL_SUPPORTED)
 (set-info :status sat)
 
 (declare-fun x () String)
 (declare-fun y () String)
 (declare-fun z () String)
-(declare-fun w () String)
-(declare-fun w1 () String)
-(declare-fun w2 () String)
 
 (assert (= (str.++ x "ba") (str.++ "ab" x)))
 

diff --git a/test/regress/regress0/strings/loop003.smt2 b/test/regress/regress0/strings/loop003.smt2
index a535f7583e6579cc6b7ab3fd47307caa158e4740..b4fbcf7d5c964a9dd18b9e7a006188ce72c36d5d 100644 (file)
--- a/test/regress/regress0/strings/loop003.smt2
+++ b/test/regress/regress0/strings/loop003.smt2
@@ -1,7 +1,3 @@
-; COMMAND-LINE: --no-check-models
-; EXPECT: sat
-; EXIT: 10
-;
 (set-logic ALL_SUPPORTED)
 (set-info :status sat)
 

diff --git a/test/regress/regress0/strings/loop004.smt2 b/test/regress/regress0/strings/loop004.smt2
index 7b39bf2d34fe858d9163f0c2243ac7d867728c04..cc9a19a9ecdef596fc0a9a4b1d286270cc18b761 100644 (file)
--- a/test/regress/regress0/strings/loop004.smt2
+++ b/test/regress/regress0/strings/loop004.smt2
@@ -1,7 +1,3 @@
-; COMMAND-LINE: --no-check-models
-; EXPECT: sat
-; EXIT: 10
-;
 (set-logic ALL_SUPPORTED)
 (set-info :status sat)
 

diff --git a/test/regress/regress0/strings/loop006.smt2 b/test/regress/regress0/strings/loop006.smt2
index 8c3690c61ca7dc142003c67c5e510a159e6d2f56..cd5dd86cedd57312898090383249e23fc13a8a8a 100644 (file)
--- a/test/regress/regress0/strings/loop006.smt2
+++ b/test/regress/regress0/strings/loop006.smt2
@@ -1,7 +1,3 @@
-; COMMAND-LINE: --no-check-models
-; EXPECT: sat
-; EXIT: 10
-;
 (set-logic ALL_SUPPORTED)
 (set-info :status sat)
 

diff --git a/test/regress/regress0/strings/loop007.smt2 b/test/regress/regress0/strings/loop007.smt2
new file mode 100644 (file)
index 0000000..8d789ed
--- /dev/null
+++ b/test/regress/regress0/strings/loop007.smt2
@@ -0,0 +1,10 @@
+(set-logic ALL_SUPPORTED)\r
+(set-info :status sat)\r
+\r
+(declare-fun x () String)\r
+(declare-fun y () String)\r
+\r
+(assert (= (str.++ x y "aa") (str.++ "aa" y x)))\r
+(assert (= (str.len x) 1))\r
+\r
+(check-sat)
\ No newline at end of file