From: ajreynol Date: Mon, 19 Oct 2015 16:10:02 +0000 (+0200) Subject: Improve stratification of strings extended function reductions, add regressions.... X-Git-Tag: cvc5-1.0.0~6200 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=497b027d87c0cdd9cf3da25acf3d9b0969020a57;p=cvc5.git Improve stratification of strings extended function reductions, add regressions. Eliminate preprocess for regexp. --- diff --git a/src/theory/strings/options b/src/theory/strings/options index ff2b4de5a..e44f388f4 100644 --- a/src/theory/strings/options +++ b/src/theory/strings/options @@ -33,7 +33,9 @@ option stringIgnNegMembership strings-inm --strings-inm bool :default false # the cardinality of the characters used by the theory of strings, default 128 (for standard ASCII) or 256 (for extended ASCII) option stringLazyPreproc strings-lazy-pp --strings-lazy-pp bool :default true - perform string preprocessing lazily + perform string preprocessing lazily upon assertion +option stringLazyPreproc2 strings-lazy-pp2 --strings-lazy-pp2 bool :default true + perform string preprocessing lazily upon failure to reduce option stringLenGeqZ strings-len-geqz --strings-len-geqz bool :default false strings length greater than zero lemmas diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 618296a95..ad1163d05 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -27,8 +27,6 @@ #include "theory/strings/theory_strings_rewriter.h" #include -#define LAZY_ADD_MEMBERSHIP - using namespace std; using namespace CVC4::context; @@ -76,7 +74,6 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu d_proxy_var_to_length(u), d_neg_ctn_eqlen(u), d_neg_ctn_ulen(u), - d_pos_ctn_cached(u), d_neg_ctn_cached(u), d_ext_func_terms(c), d_regexp_memberships(c), @@ -461,7 +458,6 @@ void TheoryStrings::preRegisterTerm(TNode n) { d_equalityEngine.addTerm(n[1]); break; } - //case kind::STRING_SUBSTR: default: { if( n.getType().isString() ) { registerTerm(n); @@ -519,14 +515,12 @@ void TheoryStrings::check(Effort e) { atom = polarity ? fact : fact[0]; //run preprocess on memberships - bool addFact = true; if( options::stringLazyPreproc() ){ - addFact = doPreprocess( atom ); + checkReduction( atom, polarity ? 1 : -1, 0 ); + doPendingLemmas(); } //assert pending fact - if( addFact ){ - assertPendingFact( atom, polarity, fact ); - } + assertPendingFact( atom, polarity, fact ); } doPendingFacts(); @@ -610,57 +604,75 @@ void TheoryStrings::check(Effort e) { Assert( d_lemma_cache.empty() ); } -bool TheoryStrings::doPreprocess( Node atom ) { - bool addFact = true; - NodeBoolMap::const_iterator it = d_preproc_cache.find( atom ); - if( it==d_preproc_cache.end() ){ - d_preproc_cache[ atom ] = true; - std::vector< Node > new_nodes; - Node res = d_preproc.decompose( atom, new_nodes ); - Assert( res==atom ); - /* - if( atom!=res ){ - //check if reduction/deduction - std::vector< Node > subs_lhs; - std::vector< Node > subs_rhs; - subs_lhs.push_back( atom ); - subs_rhs.push_back( d_true ); - Node sres = res.substitute( subs_lhs.begin(), subs_lhs.end(), subs_rhs.begin(), subs_rhs.end() ); - sres = Rewriter::rewrite( sres ); - Node plem; - if( sres!=res ){ - plem = NodeManager::currentNM()->mkNode( kind::IMPLIES, atom, sres ); - }else{ - Trace("strings-assertion-debug") << "...preprocessed to : " << res << std::endl; - plem = NodeManager::currentNM()->mkNode( kind::IFF, atom, res ); - //reduced by preprocess - addFact = false; - d_preproc_cache[ atom ] = 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 ){ + Trace("strings-process-debug2") << (*it).first << ", active=" << !(*it).second << std::endl; + if( (*it).second ){ + Node n = (*it).first; + checkReduction( n, d_extf_pol[n], effort ); + if( hasProcessed() ){ + return; } - plem = Rewriter::rewrite( plem ); - Trace("strings-assert") << "(assert " << plem << ")" << std::endl; - Trace("strings-lemma") << "Strings::Lemma " << plem << " by preprocess reduction" << std::endl; - d_out->lemma( plem ); - Trace("strings-pp-lemma") << "Preprocess reduction lemma : " << plem << std::endl; - Trace("strings-pp-lemma") << "...from " << atom << std::endl; - }else{ - Trace("strings-assertion-debug") << "...preprocess ok." << std::endl; } - */ - 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-assertion-debug") << "...new nodes : " << nnlem << std::endl; - Trace("strings-pp-lemma") << "Preprocess lemma : " << nnlem << std::endl; - Trace("strings-pp-lemma") << "...from " << atom << std::endl; - Trace("strings-lemma") << "Strings::Lemma " << nnlem << " by preprocess" << std::endl; - Trace("strings-assert") << "(assert " << nnlem << ")" << std::endl; - d_out->lemma( nnlem ); + } +} + +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( pol==1 ){ + r_effort = 1; } }else{ - addFact = (*it).second; + if( options::stringLazyPreproc() ){ + if( atom.getKind()==kind::STRING_SUBSTR ){ + r_effort = options::stringLazyPreproc2() ? 1 : 0; + }else{ + r_effort = options::stringLazyPreproc2() ? 2 : 0; + } + } + } + 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])); + sendLemma( atom, eq, "RE-Range-Len" ); + } + }else if( atom.getKind()==kind::STRING_STRCTN ){ + Node x = atom[0]; + Node s = atom[1]; + //would have already reduced by now + 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 ) ) ); + sendLemma( atom, eq, "POS-CTN" ); + }else{ + // for STRING_SUBSTR, + // 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; + sendLemma( d_true, nnlem, "Reduction" ); + } + } + } } - return addFact; } TheoryStrings::EqcInfo::EqcInfo( context::Context* c ) : d_const_term(c), d_length_term(c), d_cardinality_lem_k(c), d_normalized_length(c) { @@ -792,22 +804,16 @@ void TheoryStrings::assertPendingFact(Node atom, bool polarity, Node exp) { d_equalityEngine.assertEquality( atom, polarity, exp ); } else { if( atom.getKind()==kind::STRING_IN_REGEXP ) { -#ifdef LAZY_ADD_MEMBERSHIP if( d_ext_func_terms.find( atom )==d_ext_func_terms.end() ){ Trace("strings-extf-debug") << "Found extended function (membership) : " << atom << std::endl; d_ext_func_terms[atom] = true; } -#else - addMembership( polarity ? atom : atom.negate() ); -#endif } d_equalityEngine.assertPredicate( atom, polarity, exp ); } //collect extended function terms in the atom - if( options::stringExp() ){ - std::map< Node, bool > visited; - collectExtendedFuncTerms( atom, visited ); - } + std::map< Node, bool > visited; + collectExtendedFuncTerms( atom, visited ); } void TheoryStrings::doPendingFacts() { @@ -2522,74 +2528,76 @@ Node TheoryStrings::checkCycles( Node eqc, std::vector< Node >& curr, std::vecto void TheoryStrings::checkNormalForms() { - Trace("strings-process") << "Normalize equivalence classes...." << std::endl; - //calculate normal forms for each equivalence class, possibly adding splitting lemmas - d_normal_forms.clear(); - d_normal_forms_exp.clear(); - std::map< Node, Node > nf_to_eqc; - std::map< Node, Node > eqc_to_exp; - for( unsigned i=0; i visited; - std::vector< Node > nf; - std::vector< Node > nf_exp; - normalizeEquivalenceClass(eqc, visited, nf, nf_exp); - Trace("strings-debug") << "Finished normalizing eqc..." << std::endl; - if( d_conflict ) { - return; - } else if ( d_pending.empty() && d_lemma_cache.empty() ) { - Node nf_term = mkConcat( nf ); - if( nf_to_eqc.find( nf_term )!=nf_to_eqc.end() ) { - //Trace("strings-debug") << "Merge because of normal form : " << eqc << " and " << nf_to_eqc[nf_term] << " both have normal form " << nf_term << std::endl; - //two equivalence classes have same normal form, merge - nf_exp.push_back( eqc_to_exp[nf_to_eqc[nf_term]] ); - Node eq = eqc.eqNode( nf_to_eqc[nf_term] ); - sendInfer( mkAnd( nf_exp ), eq, "Normal_Form" ); - } else { - nf_to_eqc[nf_term] = eqc; - eqc_to_exp[eqc] = mkAnd( nf_exp ); + // simple extended func reduction + checkExtfReduction( 1 ); + if( !hasProcessed() ){ + Trace("strings-process") << "Normalize equivalence classes...." << std::endl; + //calculate normal forms for each equivalence class, possibly adding splitting lemmas + d_normal_forms.clear(); + d_normal_forms_exp.clear(); + std::map< Node, Node > nf_to_eqc; + std::map< Node, Node > eqc_to_exp; + for( unsigned i=0; i visited; + std::vector< Node > nf; + std::vector< Node > nf_exp; + normalizeEquivalenceClass(eqc, visited, nf, nf_exp); + Trace("strings-debug") << "Finished normalizing eqc..." << std::endl; + if( d_conflict ) { + return; + } else if ( d_pending.empty() && d_lemma_cache.empty() ) { + Node nf_term = mkConcat( nf ); + if( nf_to_eqc.find( nf_term )!=nf_to_eqc.end() ) { + //Trace("strings-debug") << "Merge because of normal form : " << eqc << " and " << nf_to_eqc[nf_term] << " both have normal form " << nf_term << std::endl; + //two equivalence classes have same normal form, merge + nf_exp.push_back( eqc_to_exp[nf_to_eqc[nf_term]] ); + Node eq = eqc.eqNode( nf_to_eqc[nf_term] ); + sendInfer( mkAnd( nf_exp ), eq, "Normal_Form" ); + } else { + nf_to_eqc[nf_term] = eqc; + eqc_to_exp[eqc] = mkAnd( nf_exp ); + } } + Trace("strings-process-debug") << "Done verifying normal forms are the same for " << eqc << std::endl; } - Trace("strings-process-debug") << "Done verifying normal forms are the same for " << eqc << std::endl; - } - if(Trace.isOn("strings-nf")) { - 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; + if(Trace.isOn("strings-nf")) { + 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") << std::endl; } - Trace("strings-nf") << std::endl; - } - if( !hasProcessed() ){ - checkExtendedFuncsEval( 1 ); - Trace("strings-process-debug") << "Done check extended functions re-eval, addedFact = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl; if( !hasProcessed() ){ - if( !options::stringEagerLen() ){ - checkLengthsEqc(); - if( hasProcessed() ){ - return; + checkExtendedFuncsEval( 1 ); + Trace("strings-process-debug") << "Done check extended functions re-eval, addedFact = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl; + if( !hasProcessed() ){ + if( !options::stringEagerLen() ){ + checkLengthsEqc(); + if( hasProcessed() ){ + return; + } } + //process disequalities between equivalence classes + checkDeqNF(); + Trace("strings-process-debug") << "Done check disequalities, addedFact = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl; } - //process disequalities between equivalence classes - checkDeqNF(); - Trace("strings-process-debug") << "Done check disequalities, addedFact = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl; } } Trace("strings-solve") << "Finished check normal forms, #lemmas = " << d_lemma_cache.size() << ", conflict = " << d_conflict << std::endl; } void TheoryStrings::checkDeqNF() { - if( !d_conflict && d_lemma_cache.empty() ){ - std::vector< std::vector< Node > > cols; - std::vector< Node > lts; - separateByLength( d_strings_eqc, cols, lts ); - for( unsigned i=0; i1 && d_lemma_cache.empty() ){ + std::vector< std::vector< Node > > cols; + std::vector< Node > lts; + separateByLength( d_strings_eqc, cols, lts ); + for( unsigned i=0; i1 && d_lemma_cache.empty() ){ Trace("strings-solve") << "- Verify disequalities are processed for " << cols[i][0]; printConcat( d_normal_forms[cols[i][0]], "strings-solve" ); Trace("strings-solve") << "... #eql = " << cols[i].size() << std::endl; - //must ensure that normal forms are disequal for( unsigned j=0; j& exp ) { } void TheoryStrings::checkExtendedFuncs() { - std::map< bool, std::vector< Node > > pnContains; - std::map< bool, std::vector< Node > > pnMem; - for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){ - if( (*it).second ){ - Node n = (*it).first; - if( n.getKind()==kind::STRING_STRCTN ) { - bool pol = areEqual( n, d_true ); - Assert( pol || areEqual( n, d_false ) ); - pnContains[pol].push_back( n ); - } -#ifdef LAZY_ADD_MEMBERSHIP - else if( n.getKind()==kind::STRING_IN_REGEXP ) { - bool pol = areEqual( n, d_true ); - Assert( pol || areEqual( n, d_false ) ); - pnMem[pol].push_back( n ); + if( options::stringExp() ){ + checkExtfReduction( 2 ); + } + if( !hasProcessed() ){ + //collect all remaining extended functions + std::vector< Node > pnContains; + std::map< bool, std::vector< Node > > pnMem; + for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){ + if( (*it).second ){ + Node n = (*it).first; + if( n.getKind()==kind::STRING_STRCTN ) { + if( d_extf_pol[n]!=1 ){ + Assert( d_extf_pol[n]==-1 ); + pnContains.push_back( n ); + } + }else if( n.getKind()==kind::STRING_IN_REGEXP ) { + bool pol = d_extf_pol[n]==1; + Assert( d_extf_pol[n]==1 || d_extf_pol[n]==-1 ); + pnMem[pol].push_back( n ); + } } -#endif } - } - - checkPosContains( pnContains[true] ); - Trace("strings-process") << "Done check positive contain constraints, addedLemma = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl; - if( !hasProcessed() ) { - checkNegContains( pnContains[false] ); - Trace("strings-process") << "Done check negative contain constraints, addedLemma = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl; + Trace("strings-process-debug") << "Checking negative contains..." << std::endl; + checkNegContains( pnContains ); + Trace("strings-process-debug") << "Done check negative contain constraints, addedLemma = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl; if( !hasProcessed() ) { Trace("strings-process") << "Adding memberships..." << std::endl; //add all non-evaluated memberships -#ifdef LAZY_ADD_MEMBERSHIP for( std::map< bool, std::vector< Node > >::iterator it=pnMem.begin(); it != pnMem.end(); ++it ){ for( unsigned i=0; isecond.size(); i++ ){ Trace("strings-process-debug") << " add membership : " << it->second[i] << ", pol = " << it->first << std::endl; addMembership( it->first ? it->second[i] : it->second[i].negate() ); } } -#endif checkMemberships(); Trace("strings-process") << "Done check memberships, addedLemma = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl; } } } -void TheoryStrings::checkPosContains( std::vector< Node >& posContains ) { - for( unsigned i=0; i& negContains ) { + for( unsigned i=0; imkNode( kind::AND, atom.negate(), eq ) ); + Node xneqs = x.eqNode(s).negate(); + d_neg_ctn_eqlen.insert( atom ); + sendLemma( antc, xneqs, "NEG-CTN-EQL" ); } - } else { - Trace("strings-ctn") << "... is satisfied." << std::endl; - } - } - } -} + }else if( !areDisequal(lenx, lens) ){ + if(d_neg_ctn_ulen.find(atom) == d_neg_ctn_ulen.end()) { + lenx = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, x); + lens = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s); + d_neg_ctn_ulen.insert( atom ); + sendSplit(lenx, lens, "NEG-CTN-SP"); + } + }else{ + if(d_neg_ctn_cached.find(atom) == d_neg_ctn_cached.end()) { + lenx = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, x); + 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); -void TheoryStrings::checkNegContains( std::vector< Node >& negContains ) { - //check for conflicts - for( unsigned i=0; imkNode( kind::AND, atom.negate(), atom[1].eqNode( d_emptyString ) ); - Node conc = Node::null(); - sendLemma( ant, conc, "NEG-CTN Conflict 1" ); - } else if( areEqual( atom[1], atom[0] ) ) { - Node ant = NodeManager::currentNM()->mkNode( kind::AND, atom.negate(), atom[1].eqNode( atom[0] ) ); - Node conc = Node::null(); - sendLemma( ant, conc, "NEG-CTN Conflict 2" ); - } - } - } - if( !d_conflict ){ - //check for lemmas - if(options::stringExp()) { - for( unsigned i=0; imkNode( kind::AND, atom.negate(), eq ) ); - Node xneqs = x.eqNode(s).negate(); - d_neg_ctn_eqlen.insert( atom ); - sendLemma( antc, xneqs, "NEG-CTN-EQL" ); - } - } else if(!areDisequal(lenx, lens)) { - if(d_neg_ctn_ulen.find(atom) == d_neg_ctn_ulen.end()) { - lenx = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, x); - lens = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s); - d_neg_ctn_ulen.insert( atom ); - sendSplit(lenx, lens, "NEG-CTN-SP"); - } - } else { - if(d_neg_ctn_cached.find(atom) == d_neg_ctn_cached.end()) { - lenx = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, x); - 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 ) ); - - d_neg_ctn_cached.insert( atom ); - sendLemma( atom.negate(), conc, "NEG-CTN-BRK" ); - //d_pending_req_phase[xlss] = true; - } + 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 ) ); + + d_neg_ctn_cached.insert( atom ); + sendLemma( atom.negate(), conc, "NEG-CTN-BRK" ); + //d_pending_req_phase[xlss] = true; } } - } else { - if( !negContains.empty() ){ - throw LogicException("Strings Incomplete (due to Negative Contain) by default, try --strings-exp option."); - } + } + } else { + if( !negContains.empty() ){ + throw LogicException("Strings Incomplete (due to Negative Contain) by default, try --strings-exp option."); } } } diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index bc53528f8..52bc37cb8 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -171,9 +171,6 @@ private: // extended functions inferences cache NodeSet d_extf_infer_cache; - bool doPreprocess( Node atom ); - - private: NodeSet d_congruent; std::map< Node, Node > d_eqc_to_const; @@ -244,6 +241,9 @@ private: void checkExtfInference( Node n, Node nr, int effort ); void collectVars( Node n, std::map< Node, std::vector< Node > >& vars, std::map< Node, bool >& visited ); Node getSymbolicDefinition( Node n, std::vector< Node >& exp ); + //check extf reduction + void checkExtfReduction( int effort ); + void checkReduction( Node atom, int pol, int effort ); //flat forms check void checkFlatForms(); Node checkCycles( Node eqc, std::vector< Node >& curr, std::vector< Node >& exp ); @@ -382,7 +382,6 @@ private: // Special String Functions NodeSet d_neg_ctn_eqlen; NodeSet d_neg_ctn_ulen; - NodeSet d_pos_ctn_cached; NodeSet d_neg_ctn_cached; //extended string terms and whether they have been reduced NodeBoolMap d_ext_func_terms; diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 8224d6352..ccce5a86d 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -30,29 +30,6 @@ StringsPreprocess::StringsPreprocess( context::UserContext* u ) : d_cache( u ){ d_zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) ); } -void StringsPreprocess::processRegExp( Node s, Node r, std::vector< Node > &new_nodes ) { - CVC4::Kind k = r.getKind(); - switch( k ) { - case kind::REGEXP_RANGE: { - Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) ); - Node eq = one.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s)); - new_nodes.push_back( eq ); - break; - } - case kind::REGEXP_STAR: - case kind::REGEXP_CONCAT: - case kind::REGEXP_LOOP: { - //do nothing - break; - } - default: { - //all others should be rewritten by now - Trace("strings-error") << "Unsupported term: " << r << " in processRegExp." << std::endl; - Assert( false, "Unsupported Term" ); - } - } -} - /* int StringsPreprocess::checkFixLenVar( Node t ) { int ret = 2; @@ -110,31 +87,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { retNode = t; } } else */ - if( t.getKind() == kind::STRING_IN_REGEXP ) { - //process any reductions - std::vector< Node > ret; - processRegExp( t[0], t[1], ret ); - Node conc; - if( !ret.empty() ){ - conc = ret.size()==1 ? ret[0] : NodeManager::currentNM()->mkNode( kind::AND, ret ); - } - if( options::stringLazyPreproc() ){ - //implication as lemma - if( !conc.isNull() ){ - new_nodes.push_back( NodeManager::currentNM()->mkNode( kind::IMPLIES, t, conc ) ); - } - d_cache[t] = t; - }else{ - //rewrite as conjunction - Node n = t; - if( !conc.isNull() ){ - n = NodeManager::currentNM()->mkNode( kind::AND, t, conc ); - n = Rewriter::rewrite( n ); - } - d_cache[t] = n; - retNode = n; - } - } else if( t.getKind() == kind::STRING_SUBSTR ) { + if( t.getKind() == kind::STRING_SUBSTR ) { /* Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] ), diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h index 22eb9eb91..08805fddc 100644 --- a/src/theory/strings/theory_strings_preprocess.h +++ b/src/theory/strings/theory_strings_preprocess.h @@ -37,7 +37,6 @@ class StringsPreprocess { Node d_zero; private: //int checkFixLenVar( Node t ); - void processRegExp( Node s, Node r, std::vector< Node > &new_nodes ); Node simplify( Node t, std::vector< Node > &new_nodes ); public: StringsPreprocess( context::UserContext* u ); diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am index 962340a91..4d1da2efb 100644 --- a/test/regress/regress0/strings/Makefile.am +++ b/test/regress/regress0/strings/Makefile.am @@ -70,15 +70,14 @@ TESTS = \ norn-ab.smt2 \ idof-rewrites.smt2 \ bug682.smt2 \ - bug686dd.smt2 - -FAILING_TESTS = - -EXTRA_DIST = $(TESTS) \ + bug686dd.smt2 \ + idof-handg.smt2 \ fmf001.smt2 \ type002.smt2 -# somewhat slow after changes on Oct 6: idof-handg.smt2 +FAILING_TESTS = + +EXTRA_DIST = $(TESTS) # and make sure to distribute it EXTRA_DIST +=