From 58007016d91fe1954e4579b952006c54ece0f2f7 Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Fri, 27 Sep 2013 09:24:42 -0500 Subject: [PATCH] removes unsound cases, adds unrolling --- src/parser/smt2/Smt2.g | 6 +- src/smt/smt_engine.cpp | 9 + src/theory/strings/Makefile.am | 4 +- src/theory/strings/options | 2 +- src/theory/strings/theory_strings.cpp | 307 +++++++++++------- src/theory/strings/theory_strings.h | 11 +- .../strings/theory_strings_preprocess.cpp | 120 +++++++ .../strings/theory_strings_preprocess.h | 41 +++ .../strings/theory_strings_type_rules.h | 3 + test/regress/regress0/strings/Makefile.am | 12 +- .../regress/regress0/strings/cardinality.smt2 | 2 +- test/regress/regress0/strings/loop002.smt2 | 7 - test/regress/regress0/strings/loop003.smt2 | 4 - test/regress/regress0/strings/loop004.smt2 | 4 - test/regress/regress0/strings/loop006.smt2 | 4 - test/regress/regress0/strings/loop007.smt2 | 10 + 16 files changed, 397 insertions(+), 149 deletions(-) create mode 100644 src/theory/strings/theory_strings_preprocess.cpp create mode 100644 src/theory/strings/theory_strings_preprocess.h create mode 100644 test/regress/regress0/strings/loop007.smt2 diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 8af543039..c84046570 100644 --- 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 91eae8915..201302baf 100644 --- 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 15bd04b88..38efa33f3 100644 --- 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 c90d654b1..9226f9999 100644 --- 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 df55bcf83..f9bb74486 100644 --- 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 +#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; i0 ) 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 & v addNormalFormPair( normal_form_src[i], normal_form_src[j] ); //add loop equations that we've accumulated for( unsigned r=0; r & 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 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().size() == 1 ? const_str : - NodeManager::currentNM()->mkConst( const_str.getConst().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().size() == 1 ? const_str : + NodeManager::currentNM()->mkConst( const_str.getConst().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; ilemma( d_lemma_cache[i] ); - } if( !d_lemma_cache.empty() ){ - d_lemma_cache.clear(); - return true; + for( unsigned i=0; ilemma( 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() NodeList; typedef context::CDHashMap NodeListMap; + typedef context::CDHashMap 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 index 000000000..d62fd4c9e --- /dev/null +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -0,0 +1,120 @@ +/********************* */ +/*! \file theory_strings_preprocess.cpp + ** \verbatim + ** Original author: Tianyi Liang + ** Major contributors: Tianyi Liang, Andrew Reynolds + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2013-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Strings Preprocess + ** + ** Strings Preprocess. + **/ + +#include "theory/strings/theory_strings_preprocess.h" +#include "expr/kind.h" + +namespace CVC4 { +namespace theory { +namespace strings { + +void StringsPreprocess::simplifyRegExp( Node s, Node r, std::vector< Node > &ret ) { + int k = r.getKind(); + switch( k ) { + case kind::STRING_TO_REGEXP: + { + Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, s, r[0] ); + ret.push_back( eq ); + } + break; + case kind::REGEXP_CONCAT: + { + std::vector< Node > cc; + for(unsigned i=0; imkSkolem( "recsym_$$", s.getType(), "created for regular expression concat" ); + simplifyRegExp( sk, r[i], ret ); + cc.push_back( sk ); + } + Node cc_eq = NodeManager::currentNM()->mkNode( kind::EQUAL, s, + NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, cc ) ); + ret.push_back( cc_eq ); + } + break; + case kind::REGEXP_OR: + { + std::vector< Node > c_or; + for(unsigned i=0; imkNode( kind::OR, c_or ); + ret.push_back( eq ); + } + break; + case kind::REGEXP_INTER: + for(unsigned i=0; imkSkolem( "ressym_$$", s.getType(), "created for regular expression star" ); + Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, + NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk, s ), + NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, s, sk )); + ret.push_back( eq ); + simplifyRegExp( sk, r[0], ret ); + } + break; + case kind::REGEXP_OPT: + { + Node eq_empty = NodeManager::currentNM()->mkNode( kind::EQUAL, s, NodeManager::currentNM()->mkConst( ::CVC4::String("") ) ); + std::vector< Node > rr; + simplifyRegExp( s, r[0], rr ); + Node nrr = rr.size()==1 ? rr[0] : NodeManager::currentNM()->mkNode( kind::AND, rr ); + ret.push_back( NodeManager::currentNM()->mkNode( kind::OR, eq_empty, nrr) ); + } + break; + default: + //TODO:case kind::REGEXP_PLUS: + //TODO: special sym: sigma, none, all + break; + } +} + +Node StringsPreprocess::simplify( Node t ) { + if( t.getKind() == kind::STRING_IN_REGEXP ){ + // t0 in t1 + //rewrite it + std::vector< Node > ret; + simplifyRegExp( t[0], t[1], ret ); + + return ret.size() == 1 ? ret[0] : NodeManager::currentNM()->mkNode( kind::AND, ret ); + }else if( t.getNumChildren()>0 ){ + std::vector< Node > cc; + if (t.getMetaKind() == kind::metakind::PARAMETERIZED) { + cc.push_back(t.getOperator()); + } + bool changed = false; + for( unsigned i=0; imkNode( t.getKind(), cc ) : t; + }else{ + return t; + } +} + +void StringsPreprocess::simplify(std::vector< Node > &vec_node) { + for( unsigned i=0; i +#include "theory/theory.h" + +namespace CVC4 { +namespace theory { +namespace strings { + +class StringsPreprocess { +private: + void simplifyRegExp( Node s, Node r, std::vector< Node > &ret ); + Node simplify( Node t ); +public: +void simplify(std::vector< Node > &vec_node); +}; + +}/* CVC4::theory::strings namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__STRINGS__PREPROCESS_H */ diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h index bf284ea7b..9c3d6c71e 100644 --- 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 699a7ff3c..2b0954cad 100644 --- 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 5c4771d71..2baac51ce 100644 --- 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 a47b959f5..2f96241dc 100644 --- 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 a535f7583..b4fbcf7d5 100644 --- 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 7b39bf2d3..cc9a19a9e 100644 --- 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 8c3690c61..cd5dd86ce 100644 --- 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 index 000000000..8d789edb3 --- /dev/null +++ b/test/regress/regress0/strings/loop007.smt2 @@ -0,0 +1,10 @@ +(set-logic ALL_SUPPORTED) +(set-info :status sat) + +(declare-fun x () String) +(declare-fun y () String) + +(assert (= (str.++ x y "aa") (str.++ "aa" y x))) +(assert (= (str.len x) 1)) + +(check-sat) \ No newline at end of file -- 2.30.2