diff options
| -rw-r--r-- | src/smt/smt_engine.cpp | 9 | ||||
| -rw-r--r-- | src/theory/sep/theory_sep.cpp | 38 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 187 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings.h | 5 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings_preprocess.cpp | 265 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings_preprocess.h | 19 | ||||
| -rw-r--r-- | test/regress/regress0/strings/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/strings/cmu-disagree-0707-dd.smt2 | 22 |
8 files changed, 247 insertions, 301 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 08495c936..b76b90e84 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3986,15 +3986,6 @@ void SmtEnginePrivate::processAssertions() { dumpAssertions("post-bv-to-bool", d_assertions); Trace("smt") << "POST bvToBool" << endl; } - if( d_smt.d_logic.isTheoryEnabled(THEORY_STRINGS) ) { - Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-strings-preprocess" << endl; - dumpAssertions("pre-strings-pp", d_assertions); - if( !options::stringLazyPreproc() ){ - ((theory::strings::TheoryStrings*)d_smt.d_theoryEngine->theoryOf(THEORY_STRINGS))->getPreprocess()->simplify( d_assertions.ref() ); - } - Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-strings-preprocess" << endl; - dumpAssertions("post-strings-pp", d_assertions); - } if( d_smt.d_logic.isTheoryEnabled(THEORY_SEP) ) { //separation logic solver needs to register the entire input ((theory::sep::TheorySep*)d_smt.d_theoryEngine->theoryOf(THEORY_SEP))->processAssertions( d_assertions.ref() ); diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index 8b63c3149..be0af4929 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -726,33 +726,19 @@ void TheorySep::check(Effort e) { Assert( d_label_model.find( s_lbl )!=d_label_model.end() ); std::vector< Node > conc; bool inst_success = true; - if( options::sepExp() ){ - //old refinement lemmas - for( std::map< int, Node >::iterator itl = d_label_map[s_atom][s_lbl].begin(); itl != d_label_map[s_atom][s_lbl].end(); ++itl ){ - int sub_index = itl->first; - std::map< Node, Node > visited; - Node c = applyLabel( s_atom[itl->first], mvals[sub_index], visited ); - Trace("sep-process-debug") << " applied inst : " << c << std::endl; - if( s_atom.getKind()==kind::SEP_STAR || sub_index==0 ){ - conc.push_back( c.negate() ); - }else{ - conc.push_back( c ); - } - } + //new refinement + //instantiate the label + std::map< Node, Node > visited; + Node inst = instantiateLabel( s_atom, s_lbl, s_lbl, o_b_lbl_mval, visited, d_pto_model, d_tmodel, tn, active_lbl ); + Trace("sep-inst-debug") << " applied inst : " << inst << std::endl; + if( inst.isNull() ){ + inst_success = false; }else{ - //new refinement - std::map< Node, Node > visited; - Node inst = instantiateLabel( s_atom, s_lbl, s_lbl, o_b_lbl_mval, visited, d_pto_model, d_tmodel, tn, active_lbl ); - Trace("sep-inst-debug") << " applied inst : " << inst << std::endl; - if( inst.isNull() ){ + inst = Rewriter::rewrite( inst ); + if( inst==( polarity ? d_true : d_false ) ){ inst_success = false; - }else{ - inst = Rewriter::rewrite( inst ); - if( inst==( polarity ? d_true : d_false ) ){ - inst_success = false; - } - conc.push_back( polarity ? inst : inst.negate() ); } + conc.push_back( polarity ? inst : inst.negate() ); } if( inst_success ){ std::vector< Node > lemc; @@ -761,11 +747,13 @@ void TheorySep::check(Effort e) { pol_atom = atom.negate(); } lemc.push_back( pol_atom ); + //TODO: add disjointness assumption + //lemc.push_back( s_lbl.eqNode( o_b_lbl_mval ).negate() ); //lemc.push_back( NodeManager::currentNM()->mkNode( kind::SUBSET, o_b_lbl_mval, s_lbl ).negate() ); lemc.insert( lemc.end(), conc.begin(), conc.end() ); Node lem = NodeManager::currentNM()->mkNode( kind::OR, lemc ); - if( std::find( d_refinement_lem[s_atom][s_lbl].begin(), d_refinement_lem[s_atom][s_lbl].end(), lem )==d_refinement_lem[s_atom][s_lbl].end() ){ + if( std::find( d_refinement_lem[s_atom][s_lbl].begin(), d_refinement_lem[s_atom][s_lbl].end(), lem )==d_refinement_lem[s_atom][s_lbl].end() ){ d_refinement_lem[s_atom][s_lbl].push_back( lem ); Trace("sep-process") << "-----> refinement lemma (#" << d_refinement_lem[s_atom][s_lbl].size() << ") : " << lem << std::endl; Trace("sep-lemma") << "Sep::Lemma : negated star/wand refinement : " << lem << std::endl; diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index c319aad01..493fbf1de 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -99,11 +99,11 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, d_equalityEngine.addFunctionKind(kind::STRING_IN_REGEXP); d_equalityEngine.addFunctionKind(kind::STRING_LENGTH); d_equalityEngine.addFunctionKind(kind::STRING_CONCAT); - d_equalityEngine.addFunctionKind(kind::STRING_STRCTN); - d_equalityEngine.addFunctionKind(kind::STRING_SUBSTR); - d_equalityEngine.addFunctionKind(kind::STRING_ITOS); - d_equalityEngine.addFunctionKind(kind::STRING_STOI); if( options::stringLazyPreproc() ){ + d_equalityEngine.addFunctionKind(kind::STRING_STRCTN); + d_equalityEngine.addFunctionKind(kind::STRING_SUBSTR); + d_equalityEngine.addFunctionKind(kind::STRING_ITOS); + d_equalityEngine.addFunctionKind(kind::STRING_STOI); d_equalityEngine.addFunctionKind(kind::STRING_U16TOS); d_equalityEngine.addFunctionKind(kind::STRING_STOU16); d_equalityEngine.addFunctionKind(kind::STRING_U32TOS); @@ -537,10 +537,12 @@ void TheoryStrings::check(Effort e) { atom = polarity ? fact : fact[0]; //run preprocess on memberships + /* if( options::stringLazyPreproc() ){ checkReduction( atom, polarity ? 1 : -1, 0 ); doPendingLemmas(); } + */ //assert pending fact assertPendingFact( atom, polarity, fact ); } @@ -632,6 +634,10 @@ void TheoryStrings::check(Effort e) { Assert( d_lemma_cache.empty() ); } +bool TheoryStrings::needsCheckLastEffort() { + return false; +} + void TheoryStrings::checkExtfReduction( int effort ) { Trace("strings-process-debug") << "Checking preprocess at effort " << effort << ", #to process=" << d_ext_func_terms.size() << "..." << std::endl; for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){ @@ -650,11 +656,7 @@ void TheoryStrings::checkReduction( Node atom, int pol, int effort ) { //determine the effort level to process the extf at // 0 - at assertion time, 1+ - after no other reduction is applicable int r_effort = -1; - if( atom.getKind()==kind::STRING_IN_REGEXP ){ - if( pol==1 && atom[1].getKind()==kind::REGEXP_RANGE ){ - r_effort = 0; - } - }else if( atom.getKind()==kind::STRING_STRCTN ){ + if( atom.getKind()==kind::STRING_STRCTN ){ if( pol==1 ){ r_effort = 1; }else{ @@ -665,7 +667,7 @@ void TheoryStrings::checkReduction( Node atom, int pol, int effort ) { std::vector< Node > lexp; Node lenx = getLength( x, lexp ); Node lens = getLength( s, lexp ); - if( areEqual(lenx, lens) ){ + if( areEqual( lenx, lens ) ){ d_ext_func_terms[atom] = false; //we can reduce to disequality when lengths are equal if( !areDisequal( x, s ) ){ @@ -676,8 +678,8 @@ void TheoryStrings::checkReduction( Node atom, int pol, int effort ) { } }else if( !areDisequal( lenx, lens ) ){ //split on their lenths - lenx = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, x); - lens = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s); + lenx = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, x ); + lens = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, s ); sendSplit( lenx, lens, "NEG-CTN-SP" ); }else{ r_effort = 2; @@ -688,81 +690,42 @@ void TheoryStrings::checkReduction( Node atom, int pol, int effort ) { if( options::stringLazyPreproc() ){ if( atom.getKind()==kind::STRING_SUBSTR ){ r_effort = 1; - }else{ + }else if( atom.getKind()!=kind::STRING_IN_REGEXP ){ r_effort = 2; } } } if( effort==r_effort ){ - if( d_preproc_cache.find( atom )==d_preproc_cache.end() ){ - d_preproc_cache[ atom ] = true; - Trace("strings-process-debug") << "Process reduction for " << atom << std::endl; - if( atom.getKind()==kind::STRING_IN_REGEXP ){ - if( atom[1].getKind()==kind::REGEXP_RANGE ){ - Node eq = d_one.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, atom[0])); - std::vector< Node > exp_vec; - exp_vec.push_back( atom ); - sendInference( d_empty_vec, exp_vec, eq, "RE-Range-Len", true ); - } - }else if( atom.getKind()==kind::STRING_STRCTN ){ + Node c_atom = pol==-1 ? atom.negate() : atom; + if( d_preproc_cache.find( c_atom )==d_preproc_cache.end() ){ + d_preproc_cache[ c_atom ] = true; + Trace("strings-process-debug") << "Process reduction for " << atom << ", pol = " << pol << std::endl; + if( atom.getKind()==kind::STRING_STRCTN && pol==1 ){ Node x = atom[0]; Node s = atom[1]; - if( pol==1 ){ - //positive contains reduces to a equality - Assert( !areEqual( s, d_emptyString ) && !areEqual( s, x ) ); - Node sk1 = mkSkolemCached( x, s, sk_id_ctn_pre, "sc1" ); - Node sk2 = mkSkolemCached( x, s, sk_id_ctn_post, "sc2" ); - Node eq = Rewriter::rewrite( x.eqNode( mkConcat( sk1, s, sk2 ) ) ); - std::vector< Node > exp_vec; - exp_vec.push_back( atom ); - sendInference( d_empty_vec, exp_vec, eq, "POS-CTN", true ); - }else{ - //negative contains reduces to forall - Node lenx = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, x); - Node lens = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s); - Node b1 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType()); - Node b1v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b1); - Node g1 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, NodeManager::currentNM()->mkNode( kind::GEQ, b1, d_zero ), - NodeManager::currentNM()->mkNode( kind::GEQ, NodeManager::currentNM()->mkNode( kind::MINUS, lenx, lens ), b1 ) ) ); - Node b2 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType()); - Node s2 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, x, NodeManager::currentNM()->mkNode( kind::PLUS, b1, b2 ), d_one); - Node s5 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, s, b2, d_one); - - Node b2v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b2);//, s1, s3, s4, s6); - - std::vector< Node > vec_nodes; - Node cc = NodeManager::currentNM()->mkNode( kind::GEQ, b2, d_zero ); - vec_nodes.push_back(cc); - cc = NodeManager::currentNM()->mkNode( kind::GT, lens, b2 ); - vec_nodes.push_back(cc); - - cc = s2.eqNode(s5).negate(); - vec_nodes.push_back(cc); - - Node conc = NodeManager::currentNM()->mkNode(kind::AND, vec_nodes); - conc = NodeManager::currentNM()->mkNode( kind::EXISTS, b2v, conc ); - conc = NodeManager::currentNM()->mkNode( kind::IMPLIES, g1, conc ); - conc = NodeManager::currentNM()->mkNode( kind::FORALL, b1v, conc ); - Node xlss = NodeManager::currentNM()->mkNode( kind::GT, lens, lenx ); - conc = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::OR, xlss, conc ) ); - - std::vector< Node > exp; - exp.push_back( atom.negate() ); - sendInference( d_empty_vec, exp, conc, "NEG-CTN-BRK", true ); - } + //positive contains reduces to a equality + Node sk1 = mkSkolemCached( x, s, sk_id_ctn_pre, "sc1" ); + Node sk2 = mkSkolemCached( x, s, sk_id_ctn_post, "sc2" ); + Node eq = Rewriter::rewrite( x.eqNode( mkConcat( sk1, s, sk2 ) ) ); + std::vector< Node > exp_vec; + exp_vec.push_back( atom ); + sendInference( d_empty_vec, exp_vec, eq, "POS-CTN", true ); + //we've reduced this atom + d_ext_func_terms[ atom ] = false; }else{ - // for STRING_SUBSTR, + // for STRING_SUBSTR, STRING_STRCTN with pol=-1, // STRING_STRIDOF, STRING_ITOS, STRING_U16TOS, STRING_U32TOS, STRING_STOI, STRING_STOU16, STRING_STOU32, STRING_STRREPL std::vector< Node > new_nodes; - Node res = d_preproc.decompose( atom, new_nodes ); - Assert( res==atom ); - if( !new_nodes.empty() ){ - Node nnlem = new_nodes.size()==1 ? new_nodes[0] : NodeManager::currentNM()->mkNode( kind::AND, new_nodes ); - nnlem = Rewriter::rewrite( nnlem ); - Trace("strings-red-lemma") << "Reduction_" << effort << " lemma : " << nnlem << std::endl; - Trace("strings-red-lemma") << "...from " << atom << std::endl; - sendInference( d_empty_vec, nnlem, "Reduction", true ); - } + Node res = d_preproc.simplify( atom, new_nodes ); + Assert( res!=atom ); + new_nodes.push_back( NodeManager::currentNM()->mkNode( res.getType().isBoolean() ? kind::IFF : kind::EQUAL, res, atom ) ); + Node nnlem = new_nodes.size()==1 ? new_nodes[0] : NodeManager::currentNM()->mkNode( kind::AND, new_nodes ); + nnlem = Rewriter::rewrite( nnlem ); + Trace("strings-red-lemma") << "Reduction_" << effort << " lemma : " << nnlem << std::endl; + Trace("strings-red-lemma") << "...from " << atom << std::endl; + sendInference( d_empty_vec, nnlem, "Reduction", true ); + //we've reduced this atom + d_ext_func_terms[ atom ] = false; } } } @@ -1424,10 +1387,24 @@ void TheoryStrings::checkExtfInference( Node n, Node nr, int effort ){ if( n_pol!=0 ){ //add original to explanation d_extf_exp[n].push_back( n_pol==1 ? n : n.negate() ); - if( nr.getKind()==kind::STRING_STRCTN ){ + + //d_extf_infer_cache stores whether we have made the inferences associated with a node n, + // this may need to be generalized if multiple inferences apply + + if( nr.getKind()==kind::STRING_IN_REGEXP ){ + if( n_pol==1 && nr[1].getKind()==kind::REGEXP_RANGE ){ + if( d_extf_infer_cache.find( nr )==d_extf_infer_cache.end() ){ + d_extf_infer_cache.insert( nr ); + //length of first argument is one + Node conc = d_one.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, nr[0]) ); + sendInference( d_extf_exp[n], conc, "RE-Range-Len", true ); + } + } + }else if( nr.getKind()==kind::STRING_STRCTN ){ if( ( n_pol==1 && nr[1].getKind()==kind::STRING_CONCAT ) || ( n_pol==-1 && nr[0].getKind()==kind::STRING_CONCAT ) ){ if( d_extf_infer_cache.find( nr )==d_extf_infer_cache.end() ){ d_extf_infer_cache.insert( nr ); + //one argument does (not) contain each of the components of the other argument int index = n_pol==1 ? 1 : 0; std::vector< Node > children; @@ -1441,6 +1418,7 @@ void TheoryStrings::checkExtfInference( Node n, Node nr, int effort ){ d_ext_func_terms[conc] = false; sendInference( d_extf_exp[n], n_pol==1 ? conc : conc.negate(), "CTN_Decompose" ); } + } }else{ //store this (reduced) assertion @@ -1726,7 +1704,13 @@ void TheoryStrings::checkFlatForms() { //explain why other components up to now are empty for( unsigned t=0; t<2; t++ ){ Node c = t==0 ? a : b; - int jj = t==0 ? d_flat_form_index[a][count] : ( inf_type==2 ? ( r==0 ? c.getNumChildren() : -1 ) : d_flat_form_index[b][count] ); + int jj; + if( inf_type==3 || ( t==1 && inf_type==2 ) ){ + //explain all the empty components for F_EndpointEq, all for the short end for F_EndpointEmp + jj = r==0 ? c.getNumChildren() : -1; + }else{ + jj = t==0 ? d_flat_form_index[a][count] : d_flat_form_index[b][count]; + } if( r==0 ){ for( int j=0; j<jj; j++ ){ if( areEqual( c[j], d_emptyString ) ){ @@ -1741,10 +1725,9 @@ void TheoryStrings::checkFlatForms() { } } } - //if( exp_n.empty() ){ - sendInference( exp, conc, inf_type==0? "F_Const" : ( inf_type==1 ? "F_LengthEq" : ( inf_type==2 ? "F_Endpoint" : "F_EndpointEq" ) ) ); - //}else{ - //} + //notice that F_EndpointEmp is not typically applied, since strict prefix equality ( a.b = a ) where a,b non-empty + // is conflicting by arithmetic len(a.b)=len(a)+len(b)!=len(a) when len(b)!=0. + sendInference( exp, conc, inf_type==0? "F_Const" : ( inf_type==1 ? "F_LengthEq" : ( inf_type==2 ? "F_EndpointEmp" : "F_EndpointEq" ) ) ); if( d_conflict ){ return; }else{ @@ -1894,6 +1877,7 @@ void TheoryStrings::checkNormalForms(){ Trace("strings-nf") << "**** 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") << " N[" << it->second << "] = " << it->first << std::endl; + //Trace("strings-nf") << " exp: " << eqc_to_exp[it->first] << std::endl; } Trace("strings-nf") << std::endl; } @@ -3356,11 +3340,20 @@ void TheoryStrings::checkLengthsEqc() { Node llt = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, lt ); //now, check if length normalization has occurred if( ei->d_normalized_length.get().isNull() ) { + Node nf = mkConcat( d_normal_forms[d_strings_eqc[i]] ); + if( Trace.isOn("strings-process-debug") ){ + Trace("strings-process-debug") << " normal form is " << nf << " from base " << d_normal_forms_base[d_strings_eqc[i]] << std::endl; + Trace("strings-process-debug") << " normal form exp is: " << std::endl; + for( unsigned j=0; j<d_normal_forms_exp[d_strings_eqc[i]].size(); j++ ){ + Trace("strings-process-debug") << " " << d_normal_forms_exp[d_strings_eqc[i]][j] << std::endl; + } + } + //if not, add the lemma std::vector< Node > ant; ant.insert( ant.end(), d_normal_forms_exp[d_strings_eqc[i]].begin(), d_normal_forms_exp[d_strings_eqc[i]].end() ); ant.push_back( d_normal_forms_base[d_strings_eqc[i]].eqNode( lt ) ); - Node lc = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, mkConcat( d_normal_forms[d_strings_eqc[i]] ) ); + Node lc = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, nf ); lc = Rewriter::rewrite( lc ); Node eq = llt.eqNode( lc ); if( llt!=lc ){ @@ -3610,10 +3603,30 @@ Node TheoryStrings::getNextDecisionRequest() { } } } - return Node::null(); } +Node TheoryStrings::ppRewrite(TNode atom) { + Trace("strings-ppr") << "TheoryStrings::ppRewrite " << atom << std::endl; + if( !options::stringLazyPreproc() ){ + //eager preprocess here + std::vector< Node > new_nodes; + std::map< Node, Node > visited; + Node ret = d_preproc.simplifyRec( atom, new_nodes, visited ); + if( ret!=atom ){ + Trace("strings-ppr") << " rewrote " << atom << " -> " << ret << ", with " << new_nodes.size() << " lemmas." << std::endl; + for( unsigned i=0; i<new_nodes.size(); i++ ){ + Trace("strings-ppr") << " lemma : " << new_nodes[i] << std::endl; + d_out->lemma( new_nodes[i] ); + } + return ret; + }else{ + Assert( new_nodes.empty() ); + } + } + return atom; +} + void TheoryStrings::collectExtendedFuncTerms( Node n, std::map< Node, bool >& visited ) { if( visited.find( n )==visited.end() ){ visited[n] = true; @@ -3623,6 +3636,7 @@ void TheoryStrings::collectExtendedFuncTerms( Node n, std::map< Node, bool >& vi n.getKind() == kind::STRING_STRREPL || n.getKind() == kind::STRING_STRCTN ){ if( d_ext_func_terms.find( n )==d_ext_func_terms.end() ){ Trace("strings-extf-debug2") << "Found extended function : " << n << std::endl; + Assert( options::stringLazyPreproc() ); d_ext_func_terms[n] = true; } } @@ -4108,7 +4122,8 @@ void TheoryStrings::checkMemberships() { Node r = atom[1]; std::vector< Node > rnfexp; - if(options::stringOpt1()) { + //if(options::stringOpt1()) { + if(true){ if(!x.isConst()) { x = getNormalString( x, rnfexp); changed = true; diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 77bf974e3..91ee775c6 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -320,6 +320,8 @@ public: Node expandDefinition(LogicRequest &logicRequest, Node n); /** Check at effort e */ void check(Effort e); + /** needs check last effort */ + bool needsCheckLastEffort(); /** Conflict when merging two constants */ void conflict(TNode a, TNode b); /** called when a new equivalence class is created */ @@ -451,7 +453,8 @@ private: public: //for finite model finding Node getNextDecisionRequest(); - + //ppRewrite + Node ppRewrite(TNode atom); public: /** statistics class */ class Statistics { diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 4c69a8eb3..51feb15e6 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -28,89 +28,43 @@ namespace CVC4 { namespace theory { namespace strings { -StringsPreprocess::StringsPreprocess( context::UserContext* u ) : d_cache( u ){ +StringsPreprocess::StringsPreprocess( context::UserContext* u ){ //Constants d_zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) ); + d_one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) ); } StringsPreprocess::~StringsPreprocess(){ } -/* -int StringsPreprocess::checkFixLenVar( Node t ) { - int ret = 2; - if(t.getKind() == kind::EQUAL) { - if(t[0].getType().isInteger() && t[0].isConst() && t[1].getKind() == kind::STRING_LENGTH) { - if(t[1][0].getKind() == kind::VARIABLE) { - ret = 0; - } - } else if(t[1].getType().isInteger() && t[1].isConst() && t[0].getKind() == kind::STRING_LENGTH) { - if(t[0][0].getKind() == kind::VARIABLE) { - ret = 1; - } - } - } - if(ret != 2) { - unsigned len = t[ret].getConst<Rational>().getNumerator().toUnsignedInt(); - if(len < 2) { - ret = 2; +Node StringsPreprocess::getUfForNode( Node n ) { + //TODO: use this for eager preprocess + Kind k = n.getKind(); + std::map< Kind, Node >::iterator it = d_uf.find( k ); + if( it==d_uf.end() ){ + std::vector< TypeNode > types; + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + types.push_back( n[i].getType() ); } + TypeNode typ = NodeManager::currentNM()->mkFunctionType( types, n.getType() ); + Node f = NodeManager::currentNM()->mkSkolem( "sop", typ, "op created for string op" ); + d_uf[k] = f; + return f; + }else{ + return it->second; } - if(!options::stringExp()) { - ret = 2; - } - return ret; } -*/ -Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { - NodeNodeMap::const_iterator i = d_cache.find(t); - if(i != d_cache.end()) { - return (*i).second.isNull() ? t : (*i).second; - } - Trace("strings-preprocess") << "StringsPreprocess::simplify: " << t << std::endl; +//returns an n such that t can be replaced by n, under the assumption of lemmas in new_nodes + +Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { + unsigned prev_new_nodes = new_nodes.size(); + Trace("strings-preprocess-debug") << "StringsPreprocess::simplify: " << t << std::endl; Node retNode = t; - /*int c_id = checkFixLenVar(t); - if( c_id != 2 ) { - int v_id = 1 - c_id; - int len = t[c_id].getConst<Rational>().getNumerator().toUnsignedInt(); - if(len > 1) { - Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) ); - std::vector< Node > vec; - for(int i=0; i<len; i++) { - Node num = NodeManager::currentNM()->mkConst( ::CVC4::Rational(i) ); - //Node sk = NodeManager::currentNM()->mkNode(kind::STRING_CHARAT, t[v_id][0], num); - Node sk = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufSubstr, t[v_id][0], num, one); - vec.push_back(sk); - Node cc = one.eqNode(NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk )); - new_nodes.push_back( cc ); - } - Node lem = t[v_id][0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, vec ) ); - lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, t, lem ); - new_nodes.push_back( lem ); - d_cache[t] = t; - retNode = t; - } - } else */ if( t.getKind() == kind::STRING_SUBSTR ) { - /* - Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ, - NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] ), - NodeManager::currentNM()->mkNode( kind::PLUS, t[1], t[2] ) ); - Node t1geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, t[1], d_zero); - Node t2geq0 = NodeManager::currentNM()->mkNode(kind::GT, t[2], d_zero); - Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1geq0, t2geq0 )); - Node sk1 = NodeManager::currentNM()->mkSkolem( "ss1", NodeManager::currentNM()->stringType(), "created for charat/substr" ); - Node sk3 = NodeManager::currentNM()->mkSkolem( "ss3", NodeManager::currentNM()->stringType(), "created for charat/substr" ); - Node x_eq_123 = t[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, t, sk3 ) ); - Node len_sk1_eq_i = t[1].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) ); - Node lenc = t[2].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t ) ); - Node lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::ITE, cond, - NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i, lenc ), - t.eqNode(NodeManager::currentNM()->mkConst( ::CVC4::String("") )) )); - */ + Node skt = NodeManager::currentNM()->mkSkolem( "sst", NodeManager::currentNM()->stringType(), "created for substr" ); Node t12 = NodeManager::currentNM()->mkNode( kind::PLUS, t[1], t[2] ); Node lt0 = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] ); //start point is greater than or equal zero @@ -123,7 +77,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { Node sk1 = NodeManager::currentNM()->mkSkolem( "ss1", NodeManager::currentNM()->stringType(), "created for substr" ); Node sk2 = NodeManager::currentNM()->mkSkolem( "ss2", NodeManager::currentNM()->stringType(), "created for substr" ); - Node b11 = t[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, t, sk2 ) ); + Node b11 = t[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, skt, sk2 ) ); //length of first skolem is second argument Node b12 = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ).eqNode( t[1] ); //length of second skolem is abs difference between end point and end of string @@ -132,11 +86,10 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { NodeManager::currentNM()->mkNode( kind::MINUS, lt0, t12 ), d_zero ) ); Node b1 = NodeManager::currentNM()->mkNode( kind::AND, b11, b12, b13 ); - Node b2 = t.eqNode( NodeManager::currentNM()->mkConst( ::CVC4::String("") ) ); - + Node b2 = skt.eqNode( NodeManager::currentNM()->mkConst( ::CVC4::String("") ) ); Node lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::ITE, cond, b1, b2 ) ); new_nodes.push_back( lemma ); - d_cache[t] = t; + retNode = skt; } else if( t.getKind() == kind::STRING_STRIDOF ) { Node sk2 = NodeManager::currentNM()->mkSkolem( "io2", NodeManager::currentNM()->stringType(), "created for indexof" ); Node sk3 = NodeManager::currentNM()->mkSkolem( "io3", NodeManager::currentNM()->stringType(), "created for indexof" ); @@ -180,19 +133,14 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { Node cond = skk.eqNode( negone ); Node rr = NodeManager::currentNM()->mkNode( kind::ITE, cond, left, right ); new_nodes.push_back( rr ); - if( options::stringLazyPreproc() ){ - new_nodes.push_back( t.eqNode( skk ) ); - d_cache[t] = Node::null(); - }else{ - d_cache[t] = skk; - retNode = skk; - } + retNode = skk; } else if( t.getKind() == kind::STRING_ITOS || t.getKind() == kind::STRING_U16TOS || t.getKind() == kind::STRING_U32TOS ) { //Node num = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::ITE, // NodeManager::currentNM()->mkNode(kind::GEQ, t[0], d_zero), // t[0], NodeManager::currentNM()->mkNode(kind::UMINUS, t[0]))); Node num = t[0]; - Node pret = NodeManager::currentNM()->mkNode(kind::STRING_ITOS, num); + //Node pret = NodeManager::currentNM()->mkNode(kind::STRING_ITOS, num); + Node pret = NodeManager::currentNM()->mkSkolem( "itost", NodeManager::currentNM()->stringType(), "created for itos" ); Node lenp = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, pret); Node nonneg = NodeManager::currentNM()->mkNode(kind::GEQ, t[0], d_zero); @@ -295,20 +243,11 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { t.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, NodeManager::currentNM()->mkConst(::CVC4::String("-")), pret)))); new_nodes.push_back( conc );*/ - if( options::stringLazyPreproc() && t!=pret ){ - new_nodes.push_back( t.eqNode( pret ) ); - d_cache[t] = Node::null(); - }else{ - d_cache[t] = pret; - retNode = pret; - } - //don't rewrite processed - if(t != pret) { - d_cache[pret] = pret; - } + retNode = pret; } else if( t.getKind() == kind::STRING_STOI || t.getKind() == kind::STRING_STOU16 || t.getKind() == kind::STRING_STOU32 ) { Node str = t[0]; - Node pret = NodeManager::currentNM()->mkNode(kind::STRING_STOI, str); + //Node pret = NodeManager::currentNM()->mkNode(kind::STRING_STOI, str); + Node pret = NodeManager::currentNM()->mkSkolem( "stoit", NodeManager::currentNM()->integerType(), "created for stoi" ); Node lenp = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, str); Node negone = NodeManager::currentNM()->mkConst( ::CVC4::Rational(-1) ); @@ -411,16 +350,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { Node conc = NodeManager::currentNM()->mkNode(kind::ITE, pret.eqNode(negone), NodeManager::currentNM()->mkNode(kind::OR, cc1, cc2), cc3); new_nodes.push_back( conc ); - if( options::stringLazyPreproc() && t!=pret ){ - new_nodes.push_back( t.eqNode( pret ) ); - d_cache[t] = Node::null(); - }else{ - d_cache[t] = pret; - retNode = pret; - } - if(t != pret) { - d_cache[pret] = pret; - } + retNode = pret; } else if( t.getKind() == kind::STRING_STRREPL ) { Node x = t[0]; Node y = t[1]; @@ -443,95 +373,88 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { new_nodes.push_back( rr ); rr = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::GT, NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, y), d_zero) ); new_nodes.push_back( rr ); - if( options::stringLazyPreproc() ){ - new_nodes.push_back( t.eqNode( skw ) ); - d_cache[t] = Node::null(); - }else{ - d_cache[t] = skw; - retNode = skw; - } + retNode = skw; } else if( t.getKind() == kind::STRING_STRCTN ){ - //TODO? - d_cache[t] = Node::null(); - } else{ - d_cache[t] = Node::null(); + Node x = t[0]; + Node s = t[1]; + //negative contains reduces to existential + Node lenx = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, x); + Node lens = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s); + Node b1 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType()); + Node b1v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b1); + Node body = NodeManager::currentNM()->mkNode( kind::AND, + NodeManager::currentNM()->mkNode( kind::LEQ, d_zero, b1 ), + NodeManager::currentNM()->mkNode( kind::LEQ, b1, NodeManager::currentNM()->mkNode( kind::MINUS, lenx, lens ) ), + NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, x, b1, lens), s ) + ); + retNode = NodeManager::currentNM()->mkNode( kind::EXISTS, b1v, body ); } - /*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], new_nodes ); - cc.push_back( tn ); - changed = changed || tn!=t[i]; - } - if(changed) { - Node n = NodeManager::currentNM()->mkNode( t.getKind(), cc ); - d_cache[t] = n; - retNode = n; - } else { - d_cache[t] = Node::null(); - retNode = t; - } - }*/ if( t!=retNode ){ - Trace("strings-preprocess-debug") << "StringsPreprocess::simplify: " << t << " -> " << retNode << std::endl; + Trace("strings-preprocess") << "StringsPreprocess::simplify: " << t << " -> " << retNode << std::endl; if(!new_nodes.empty()) { - Trace("strings-preprocess-debug") << " ... new nodes (" << new_nodes.size() << "):\n"; - for(unsigned int i=0; i<new_nodes.size(); ++i) { - Trace("strings-preprocess-debug") << "\t" << new_nodes[i] << "\n"; + Trace("strings-preprocess") << " ... new nodes (" << (new_nodes.size()-prev_new_nodes) << "):" << std::endl; + for(unsigned int i=prev_new_nodes; i<new_nodes.size(); ++i) { + Trace("strings-preprocess") << " " << new_nodes[i] << std::endl; } } } return retNode; } -Node StringsPreprocess::decompose(Node t, std::vector< Node > & new_nodes) { - NodeNodeMap::const_iterator i = d_cache.find(t); - if(i != d_cache.end()) { - return (*i).second.isNull() ? t : (*i).second; - } - - unsigned num = t.getNumChildren(); - if(num == 0) { - return simplify(t, new_nodes); +Node StringsPreprocess::simplifyRec( Node t, std::vector< Node > & new_nodes, std::map< Node, Node >& visited ){ + std::map< Node, Node >::iterator it = visited.find(t); + if( it!=visited.end() ){ + return it->second; }else{ - bool changed = false; - std::vector< Node > cc; - if (t.getMetaKind() == kind::metakind::PARAMETERIZED) { - cc.push_back(t.getOperator()); - } - for(unsigned i=0; i<t.getNumChildren(); i++) { - Node s = decompose(t[i], new_nodes); - cc.push_back( s ); - if(s != t[i]) { - changed = true; + Node retNode; + if( t.getNumChildren()==0 ){ + retNode = simplify( t, new_nodes ); + }else if( t.getKind()!=kind::FORALL ){ + bool changed = false; + std::vector< Node > cc; + if( t.getMetaKind() == kind::metakind::PARAMETERIZED ){ + cc.push_back( t.getOperator() ); } + for(unsigned i=0; i<t.getNumChildren(); i++) { + Node s = simplifyRec( t[i], new_nodes, visited ); + cc.push_back( s ); + if( s!=t[i] ) { + changed = true; + } + } + Node tmp = t; + if( changed ){ + tmp = NodeManager::currentNM()->mkNode( t.getKind(), cc ); + } + retNode = simplify( tmp, new_nodes ); } - if(changed) { - Node tmp = NodeManager::currentNM()->mkNode( t.getKind(), cc ); - return simplify(tmp, new_nodes); - } else { - return simplify(t, new_nodes); - } + visited[t] = retNode; + return retNode; } } -void StringsPreprocess::simplify(std::vector< Node > &vec_node) { +void StringsPreprocess::processAssertions( std::vector< Node > &vec_node ){ + std::map< Node, Node > visited; for( unsigned i=0; i<vec_node.size(); i++ ){ + Trace("strings-preprocess-debug") << "Preprocessing assertion " << vec_node[i] << std::endl; + //preprocess until fixed point std::vector< Node > new_nodes; - Node curr = decompose( vec_node[i], new_nodes ); - if( !new_nodes.empty() ){ - new_nodes.insert( new_nodes.begin(), curr ); - curr = NodeManager::currentNM()->mkNode( kind::AND, new_nodes ); + std::vector< Node > new_nodes_curr; + new_nodes_curr.push_back( vec_node[i] ); + while( !new_nodes_curr.empty() ){ + Node curr = new_nodes_curr.back(); + new_nodes_curr.pop_back(); + std::vector< Node > new_nodes_tmp; + curr = simplifyRec( curr, new_nodes_tmp, visited ); + new_nodes_curr.insert( new_nodes_curr.end(), new_nodes_tmp.begin(), new_nodes_tmp.end() ); + new_nodes.push_back( curr ); } - if( curr!=vec_node[i] ){ - curr = Rewriter::rewrite( curr ); - PROOF( ProofManager::currentPM()->addDependence(curr, vec_node[i]); ); - vec_node[i] = curr; + Node res = new_nodes.size()==1 ? new_nodes[0] : NodeManager::currentNM()->mkNode( kind::AND, new_nodes ); + if( res!=vec_node[i] ){ + res = Rewriter::rewrite( res ); + PROOF( ProofManager::currentPM()->addDependence( res, vec_node[i] ); ); + vec_node[i] = res; } } } diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h index abc7b5a91..18ef8cf17 100644 --- a/src/theory/strings/theory_strings_preprocess.h +++ b/src/theory/strings/theory_strings_preprocess.h @@ -31,19 +31,22 @@ namespace theory { namespace strings { class StringsPreprocess { - typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap; - NodeNodeMap d_cache; //Constants Node d_zero; -private: - //int checkFixLenVar( Node t ); - Node simplify( Node t, std::vector< Node > &new_nodes ); + Node d_one; + //mapping from kinds to UF + std::map< Kind, Node > d_uf; + //get UF for node + Node getUfForNode( Node n ); public: StringsPreprocess( context::UserContext* u ); ~StringsPreprocess(); - - Node decompose( Node t, std::vector< Node > &new_nodes ); - void simplify(std::vector< Node > &vec_node); + //simplify a node + Node simplify( Node t, std::vector< Node > &new_nodes ); + //recursive simplify + Node simplifyRec( Node t, std::vector< Node > &new_nodes, std::map< Node, Node >& visited ); + //simplify each node in vec_node + void processAssertions(std::vector< Node > &vec_node); }; }/* CVC4::theory::strings namespace */ diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am index 477d336e6..d23fd866d 100644 --- a/test/regress/regress0/strings/Makefile.am +++ b/test/regress/regress0/strings/Makefile.am @@ -78,7 +78,8 @@ TESTS = \ norn-31.smt2 \ strings-native-simple.cvc \ cmu-2db2-extf-reg.smt2 \ - norn-nel-bug-052116.smt2 + norn-nel-bug-052116.smt2 \ + cmu-disagree-0707-dd.smt2 FAILING_TESTS = diff --git a/test/regress/regress0/strings/cmu-disagree-0707-dd.smt2 b/test/regress/regress0/strings/cmu-disagree-0707-dd.smt2 new file mode 100644 index 000000000..c44dfa396 --- /dev/null +++ b/test/regress/regress0/strings/cmu-disagree-0707-dd.smt2 @@ -0,0 +1,22 @@ +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(set-option :strings-exp true) + +(declare-fun url () String) + +(assert +(and +(and +(and +(and + +(= (str.len (str.substr (str.substr url (str.indexof url "#" 2) (- (str.len url) (str.indexof url "#" 2))) (+ (str.indexof (str.substr url (str.indexof url "#" 2) (- (str.len url) (str.indexof url "#" 2))) "#" 0) 1) (- (str.len (str.substr url (str.indexof url "#" 2) (- (str.len url) (str.indexof url "#" 2)))) (+ (str.indexof (str.substr url (str.indexof url "#" 2) (- (str.len url) (str.indexof url "#" 2))) "#" 0) 1)))) 0) + +(not (= (str.substr url 0 (- (str.indexof url ":" 0) 0)) "http"))) +(> (str.indexof url ":" 0) 0)) +(>= (- (str.indexof url "#" 2) 2) 0)) +(>= (str.indexof url ":" 0) 0)) +) + +(check-sat) + |