diff options
author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2013-09-27 09:24:42 -0500 |
---|---|---|
committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2013-09-27 09:25:52 -0500 |
commit | 232728df0bb2bc101862cd78c666dfa5ef4ebfe9 (patch) | |
tree | ee0c4800b4c0c71c9f1ae2670925df1dc60f75f9 /src | |
parent | 956ecc806cc91bd52fd27c9ecc04011b630cfbc5 (diff) |
removes unsound cases, adds unrolling
Diffstat (limited to 'src')
-rw-r--r-- | src/parser/smt2/Smt2.g | 6 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 9 | ||||
-rw-r--r-- | src/theory/strings/Makefile.am | 4 | ||||
-rw-r--r-- | src/theory/strings/options | 2 | ||||
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 307 | ||||
-rw-r--r-- | src/theory/strings/theory_strings.h | 11 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_preprocess.cpp | 120 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_preprocess.h | 41 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_type_rules.h | 3 |
9 files changed, 379 insertions, 124 deletions
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 e1dc3531e..15c0f86e8 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 <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 92cf33de2..2385386ea 100644 --- 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 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; i<r.getNumChildren(); ++i) {
+ Node sk = NodeManager::currentNM()->mkSkolem( "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; i<r.getNumChildren(); ++i) {
+ simplifyRegExp( s, r[i], c_or );
+ }
+ Node eq = NodeManager::currentNM()->mkNode( kind::OR, c_or );
+ ret.push_back( eq );
+ }
+ break;
+ case kind::REGEXP_INTER:
+ for(unsigned i=0; i<r.getNumChildren(); ++i) {
+ simplifyRegExp( s, r[i], ret );
+ }
+ break;
+ case kind::REGEXP_STAR:
+ {
+ Node sk = NodeManager::currentNM()->mkSkolem( "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; i<t.getNumChildren(); i++ ){
+ Node tn = simplify( t[i] );
+ cc.push_back( tn );
+ changed = changed || tn!=t[i];
+ }
+ return changed ? NodeManager::currentNM()->mkNode( t.getKind(), cc ) : t;
+ }else{
+ return t;
+ }
+}
+
+void StringsPreprocess::simplify(std::vector< Node > &vec_node) {
+ for( unsigned i=0; i<vec_node.size(); i++ ){
+ vec_node[i] = simplify( vec_node[i] );
+ }
+}
+
+}/* CVC4::theory::strings namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h new file mode 100644 index 000000000..2b2e7dfea --- /dev/null +++ b/src/theory/strings/theory_strings_preprocess.h @@ -0,0 +1,41 @@ +/********************* */
+/*! \file theory_strings_preprocess.h
+ ** \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 "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__STRINGS__PREPROCESS_H
+#define __CVC4__THEORY__STRINGS__PREPROCESS_H
+
+#include <vector>
+#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"); } |