From: ajreynol Date: Wed, 20 Jul 2016 16:08:11 +0000 (-0500) Subject: Infer conflicts in strings based on abstracting equality as contains. Minor cleanup. X-Git-Tag: cvc5-1.0.0~6040^2~40 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ae7434f94a1bc66ee12474414985249a71881b6c;p=cvc5.git Infer conflicts in strings based on abstracting equality as contains. Minor cleanup. --- diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index d9416fbc6..53fcce26b 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -175,7 +175,7 @@ void TheorySep::preRegisterTermRec(TNode t, std::map< TNode, bool >& visited ) { std::map< TypeNode, Node >::iterator it = d_nil_ref.find( tn ); if( it==d_nil_ref.end() ){ Trace("sep-prereg") << "...set as reference." << std::endl; - d_nil_ref[tn] = t; + setNilRef( tn, t ); }else{ Node nr = it->second; Trace("sep-prereg") << "...reference is " << nr << "." << std::endl; @@ -999,7 +999,7 @@ Node TheorySep::getBaseLabel( TypeNode tn ) { ss << "__Lb"; TypeNode ltn = NodeManager::currentNM()->mkSetType(tn); //TypeNode ltn = NodeManager::currentNM()->mkSetType(NodeManager::currentNM()->mkRefType(tn)); - Node n_lbl = NodeManager::currentNM()->mkSkolem( ss.str(), ltn, "" ); + Node n_lbl = NodeManager::currentNM()->mkSkolem( ss.str(), ltn, "base label" ); d_base_label[tn] = n_lbl; //make reference bound Trace("sep") << "Make reference bound label for " << tn << std::endl; @@ -1046,13 +1046,25 @@ Node TheorySep::getNilRef( TypeNode tn ) { std::map< TypeNode, Node >::iterator it = d_nil_ref.find( tn ); if( it==d_nil_ref.end() ){ Node nil = NodeManager::currentNM()->mkSepNil( tn ); - d_nil_ref[tn] = nil; + setNilRef( tn, nil ); return nil; }else{ return it->second; } } +void TheorySep::setNilRef( TypeNode tn, Node n ) { + Assert( n.getType()==tn ); + d_nil_ref[tn] = n; + /* + //must add unit lemma to ensure nil is always a term in model construction + Node k = NodeManager::currentNM()->mkSkolem( "nk", tn ); + Node eq = NodeManager::currentNM()->mkNode( tn.isBoolean() ? kind::IFF : kind::EQUAL, k, n ); + d_out->lemma( eq ); + */ + //TODO: must not occur in base label +} + Node TheorySep::mkUnion( TypeNode tn, std::vector< Node >& locs ) { Node u; if( locs.empty() ){ @@ -1082,7 +1094,7 @@ Node TheorySep::getLabel( Node atom, int child, Node lbl ) { ss << "__Lc" << child; TypeNode ltn = NodeManager::currentNM()->mkSetType(refType); //TypeNode ltn = NodeManager::currentNM()->mkSetType(NodeManager::currentNM()->mkRefType(refType)); - Node n_lbl = NodeManager::currentNM()->mkSkolem( ss.str(), ltn, "" ); + Node n_lbl = NodeManager::currentNM()->mkSkolem( ss.str(), ltn, "sep label" ); d_label_map[atom][lbl][child] = n_lbl; d_label_map_parent[n_lbl] = lbl; return n_lbl; diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h index 85d987cc9..98a4f63c5 100644 --- a/src/theory/sep/theory_sep.h +++ b/src/theory/sep/theory_sep.h @@ -248,6 +248,7 @@ class TheorySep : public Theory { //get the base label for the spatial assertion Node getBaseLabel( TypeNode tn ); Node getNilRef( TypeNode tn ); + void setNilRef( TypeNode tn, Node n ); Node getLabel( Node atom, int child, Node lbl ); Node applyLabel( Node n, Node lbl, std::map< Node, Node >& visited ); void getLabelChildren( Node atom, Node lbl, std::vector< Node >& children, std::vector< Node >& labels ); diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index e3dc0ac72..774926315 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -1270,24 +1270,26 @@ void TheoryStrings::checkExtfEval( int effort ) { std::vector< Node > sub; for( std::map< Node, std::vector< Node > >::iterator itv = itit->second.d_rep_vars.begin(); itv != itit->second.d_rep_vars.end(); ++itv ){ Node nr = itv->first; - std::map< Node, Node >::iterator itc = d_eqc_to_const.find( nr ); Node s; Node b; Node e; if( effort>=3 ){ //model values s = d_valuation.getModel()->getRepresentative( nr ); - }else if( itc!=d_eqc_to_const.end() ){ - //constant equivalence classes - b = d_eqc_to_const_base[nr]; - s = itc->second; - e = d_eqc_to_const_exp[nr]; - }else if( effort>=1 && effort<3 ){ - //normal forms - b = d_normal_forms_base[nr]; - std::vector< Node > expt; - s = getNormalString( b, expt ); - e = mkAnd( expt ); + }else{ + std::map< Node, Node >::iterator itc = d_eqc_to_const.find( nr ); + if( itc!=d_eqc_to_const.end() ){ + //constant equivalence classes + b = d_eqc_to_const_base[nr]; + s = itc->second; + e = d_eqc_to_const_exp[nr]; + }else if( effort>=1 && effort<3 ){ + //normal forms + b = d_normal_forms_base[nr]; + std::vector< Node > expt; + s = getNormalString( b, expt ); + e = mkAnd( expt ); + } } if( !s.isNull() ){ bool added = false; @@ -1543,6 +1545,14 @@ Node TheoryStrings::getSymbolicDefinition( Node n, std::vector< Node >& exp ) { } } +Node TheoryStrings::getConstantEqc( Node eqc ) { + std::map< Node, Node >::iterator it = d_eqc_to_const.find( eqc ); + if( it!=d_eqc_to_const.end() ){ + return it->second; + }else{ + return Node::null(); + } +} void TheoryStrings::debugPrintFlatForms( const char * tc ){ for( unsigned k=0; k::iterator itc = d_eqc_to_const.find( eqc ); - if( itc!=d_eqc_to_const.end() ){ - c = itc->second; //use? + Node c = getConstantEqc( eqc ); + if( !c.isNull() ){ + //if equivalence class is constant, all component constants in flat forms must be contained in it, in order + std::map< Node, std::vector< Node > >::iterator it = d_eqc.find( eqc ); + if( it!=d_eqc.end() ){ + for( unsigned i=0; isecond.size(); i++ ){ + Node n = it->second[i]; + int firstc, lastc; + if( !TheoryStringsRewriter::canConstantContainList( c, d_flat_form[n], firstc, lastc ) ){ + Trace("strings-ff-debug") << "Flat form for " << n << " cannot be contained in constant " << c << std::endl; + Trace("strings-ff-debug") << " indices = " << firstc << "/" << lastc << std::endl; + //conflict, explanation is n = base ^ base = c ^ relevant porition of ( n = f[n] ) + std::vector< Node > exp; + Assert( d_eqc_to_const_base.find( eqc )!=d_eqc_to_const_base.end() ); + addToExplanation( n, d_eqc_to_const_base[eqc], exp ); + Assert( d_eqc_to_const_exp.find( eqc )!=d_eqc_to_const_exp.end() ); + if( !d_eqc_to_const_exp[eqc].isNull() ){ + exp.push_back( d_eqc_to_const_exp[eqc] ); + } + for( int e=firstc; e<=lastc; e++ ){ + if( d_flat_form[n][e].isConst() ){ + Assert( e>=0 && e<(int)d_flat_form_index[n].size() ); + Assert( d_flat_form_index[n][e]>=0 && d_flat_form_index[n][e]<(int)n.getNumChildren() ); + addToExplanation( d_flat_form[n][e], n[d_flat_form_index[n][e]], exp ); + } + } + Node conc = d_false; + sendInference( exp, conc, "F_NCTN" ); + return; + } + } + } } + } + + //(2) scan lists, unification to infer conflicts and equalities + for( unsigned k=0; k >::iterator it = d_eqc.find( eqc ); if( it!=d_eqc.end() && it->second.size()>1 ){ //iterate over start index @@ -1659,7 +1705,7 @@ void TheoryStrings::checkFlatForms() { } }else{ Node curr = d_flat_form[a][count]; - Node curr_c = d_eqc_to_const[curr]; + Node curr_c = getConstantEqc( curr ); Node ac = a[d_flat_form_index[a][count]]; std::vector< Node > lexp; Node lcurr = getLength( ac, lexp ); @@ -1685,7 +1731,7 @@ void TheoryStrings::checkFlatForms() { Node bc = b[d_flat_form_index[b][count]]; inelig.push_back( b ); Assert( !areEqual( curr, cc ) ); - Node cc_c = d_eqc_to_const[cc]; + Node cc_c = getConstantEqc( cc ); if( !curr_c.isNull() && !cc_c.isNull() ){ //check for constant conflict int index; @@ -1761,7 +1807,7 @@ void TheoryStrings::checkFlatForms() { } //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" ) ) ); + sendInference( exp, conc, inf_type==0 ? "F_Const" : ( inf_type==1 ? "F_Unify" : ( inf_type==2 ? "F_EndpointEmp" : "F_EndpointEq" ) ) ); if( d_conflict ){ return; }else{ @@ -2020,6 +2066,7 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc ) { bool TheoryStrings::getNormalForms( Node &eqc, std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src, std::vector< std::vector< Node > > &normal_forms_exp, std::vector< std::map< Node, std::map< bool, int > > >& normal_forms_exp_depend ) { + //constant for equivalence class Trace("strings-process-debug") << "Get normal forms " << eqc << std::endl; eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); while( !eqc_i.isFinished() ){ @@ -2114,8 +2161,8 @@ bool TheoryStrings::getNormalForms( Node &eqc, std::vector< std::vector< Node > ++eqc_i; } - if(Trace.isOn("strings-solve")) { - if( !normal_forms.empty() ) { + if( !normal_forms.empty() ) { + if(Trace.isOn("strings-solve")) { Trace("strings-solve") << "--- Normal forms for equivlance class " << eqc << " : " << std::endl; for( unsigned i=0; i } else { Trace("strings-solve") << "--- Single normal form for equivalence class " << eqc << std::endl; } + + //if equivalence class is constant, approximate as containment, infer conflicts + Node c = getConstantEqc( eqc ); + if( !c.isNull() ){ + Trace("strings-solve") << "Eqc is constant " << c << std::endl; + for( unsigned i=0; i exp; + Assert( d_eqc_to_const_base.find( eqc )!=d_eqc_to_const_base.end() ); + addToExplanation( n, d_eqc_to_const_base[eqc], exp ); + Assert( d_eqc_to_const_exp.find( eqc )!=d_eqc_to_const_exp.end() ); + if( !d_eqc_to_const_exp[eqc].isNull() ){ + exp.push_back( d_eqc_to_const_exp[eqc] ); + } + //TODO: this can be minimized based on firstc/lastc, normal_forms_exp_depend + exp.insert( exp.end(), normal_forms_exp[i].begin(), normal_forms_exp[i].end() ); + Node conc = d_false; + sendInference( exp, conc, "N_NCTN" ); + return true; + } + } + } } + return true; } @@ -2203,7 +2278,7 @@ bool TheoryStrings::processNEqc( std::vector< std::vector< Node > > &normal_form unsigned index = 0; bool success; do{ - //simple check + //first, make progress with simple checks if( processSimpleNEq( normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend, i, j, index, false ) ){ //added a lemma, return return true; @@ -2221,7 +2296,7 @@ bool TheoryStrings::processNEqc( std::vector< std::vector< Node > > &normal_form Node length_term_j = getLength( normal_forms[j][index], lexp ); //check length(normal_forms[i][index]) == length(normal_forms[j][index]) if( !areDisequal(length_term_i, length_term_j) && !areEqual(length_term_i, length_term_j) && - normal_forms[i][index].getKind()!=kind::CONST_STRING && normal_forms[j][index].getKind()!=kind::CONST_STRING ) { + normal_forms[i][index].getKind()!=kind::CONST_STRING && normal_forms[j][index].getKind()!=kind::CONST_STRING ) { //AJR: remove the latter 2 conditions? //length terms are equal, merge equivalence classes if not already done so Node length_eq = NodeManager::currentNM()->mkNode( kind::EQUAL, length_term_i, length_term_j ); Trace("strings-solve-debug") << "Non-simple Case 1 : string lengths neither equal nor disequal" << std::endl; @@ -2388,8 +2463,8 @@ bool TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal do { success = false; //if we are at the end - if(index==normal_forms[i].size() || index==normal_forms[j].size() ) { - if( index==normal_forms[i].size() && index==normal_forms[j].size() ) { + if( index==normal_forms[i].size() || index==normal_forms[j].size() ){ + if( index==normal_forms[i].size() && index==normal_forms[j].size() ){ //we're done } else { //the remainder must be empty @@ -2403,7 +2478,7 @@ bool TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal Node eq = normal_forms[k][index_k].eqNode( d_emptyString ); //Trace("strings-lemma") << "Strings: Infer " << eq << " from " << eq_exp << std::endl; Assert( !areEqual( d_emptyString, normal_forms[k][index_k] ) ); - sendInference( curr_exp, eq, "EQ_Endpoint" ); + sendInference( curr_exp, eq, "N_EndpointEmp" ); index_k++; } return true; @@ -2428,7 +2503,7 @@ bool TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal //temp_exp.insert(temp_exp.end(), curr_exp.begin(), curr_exp.end() ); getExplanationVectorForPrefix( normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend, i, j, index, isRev, temp_exp ); temp_exp.push_back(length_eq); - sendInference( temp_exp, eq, "LengthEq" ); + sendInference( temp_exp, eq, "N_Unify" ); return true; }else if( ( normal_forms[i][index].getKind()!=kind::CONST_STRING && index==normal_forms[i].size()-1 ) || ( normal_forms[j][index].getKind()!=kind::CONST_STRING && index==normal_forms[j].size()-1 ) ){ @@ -2453,7 +2528,7 @@ bool TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal } if( !areEqual( eqn[0], eqn[1] ) ) { conc = eqn[0].eqNode( eqn[1] ); - sendInference( antec, conc, "ENDPOINT", true ); + sendInference( antec, conc, "N_EndpointEq", true ); return true; }else{ Assert( normal_forms[i].size()==normal_forms[j].size() ); @@ -2483,12 +2558,12 @@ bool TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal normal_forms[l][index] = normal_forms[k][index]; index++; success = true; - } else { + }else{ std::vector< Node > antec; //curr_exp is conflict //antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() ); getExplanationVectorForPrefix( normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend, i, j, index, isRev, antec ); - sendInference( antec, d_false, "Const Conflict", true ); + sendInference( antec, d_false, "N_Const", true ); return true; } } diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 99abd94ce..e9d93a488 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -188,6 +188,8 @@ private: std::map< Node, Node > d_eqc_to_const; std::map< Node, Node > d_eqc_to_const_base; std::map< Node, Node > d_eqc_to_const_exp; + Node getConstantEqc( Node eqc ); + std::map< Node, Node > d_eqc_to_len_term; std::vector< Node > d_strings_eqc; Node d_emptyString_r; diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 75243b84d..bb03d8d0f 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -1502,22 +1502,12 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) { } } }else if( node[0].isConst() ){ - CVC4::String t = node[0].getConst(); - if( t.size()==0 ){ + if( node[0].getConst().size()==0 ){ return NodeManager::currentNM()->mkNode( kind::EQUAL, node[0], node[1] ); }else if( node[1].getKind()==kind::STRING_CONCAT ){ - //must find constant components in order - size_t pos = 0; - for(unsigned i=0; i(); - size_t new_pos = t.find(s,pos); - if( new_pos==std::string::npos ) { - return NodeManager::currentNM()->mkConst( false ); - }else{ - pos = new_pos + s.size(); - } - } + int firstc, lastc; + if( !canConstantContainConcat( node[0], node[1], firstc, lastc ) ){ + return NodeManager::currentNM()->mkConst( false ); } } } @@ -1710,3 +1700,51 @@ Node TheoryStringsRewriter::splitConstant( Node a, Node b, int& index, bool isRe return Node::null(); } } + +bool TheoryStringsRewriter::canConstantContainConcat( Node c, Node n, int& firstc, int& lastc ) { + Assert( c.isConst() ); + CVC4::String t = c.getConst(); + Assert( n.getKind()==kind::STRING_CONCAT ); + //must find constant components in order + size_t pos = 0; + firstc = -1; + lastc = -1; + for(unsigned i=0; i(); + size_t new_pos = t.find(s,pos); + if( new_pos==std::string::npos ) { + return false; + }else{ + pos = new_pos + s.size(); + } + } + } + return true; +} + +bool TheoryStringsRewriter::canConstantContainList( Node c, std::vector< Node >& l, int& firstc, int& lastc ) { + Assert( c.isConst() ); + CVC4::String t = c.getConst(); + //must find constant components in order + size_t pos = 0; + firstc = -1; + lastc = -1; + for(unsigned i=0; i(); + size_t new_pos = t.find(s,pos); + if( new_pos==std::string::npos ) { + return false; + }else{ + pos = new_pos + s.size(); + } + } + } + return true; +} + diff --git a/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h index 59588eda2..20fdd3164 100644 --- a/src/theory/strings/theory_strings_rewriter.h +++ b/src/theory/strings/theory_strings_rewriter.h @@ -61,6 +61,10 @@ public: static void getConcat( Node n, std::vector< Node >& c ); static Node mkConcat( Kind k, std::vector< Node >& c ); static Node splitConstant( Node a, Node b, int& index, bool isRev ); + /** return true if constant c can contain the concat n/list l in order + firstc/lastc store which indices were used */ + static bool canConstantContainConcat( Node c, Node n, int& firstc, int& lastc ); + static bool canConstantContainList( Node c, std::vector< Node >& l, int& firstc, int& lastc ); };/* class TheoryStringsRewriter */ }/* CVC4::theory::strings namespace */ diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am index adfc29f01..b09377bf7 100644 --- a/test/regress/regress0/strings/Makefile.am +++ b/test/regress/regress0/strings/Makefile.am @@ -81,7 +81,8 @@ TESTS = \ norn-nel-bug-052116.smt2 \ cmu-disagree-0707-dd.smt2 \ cmu-5042-0707-2.smt2 \ - cmu-dis-0707-3.smt2 + cmu-dis-0707-3.smt2 \ + nf-ff-contains-abs.smt2 FAILING_TESTS = diff --git a/test/regress/regress0/strings/nf-ff-contains-abs.smt2 b/test/regress/regress0/strings/nf-ff-contains-abs.smt2 new file mode 100644 index 000000000..eb6792666 --- /dev/null +++ b/test/regress/regress0/strings/nf-ff-contains-abs.smt2 @@ -0,0 +1,15 @@ +(set-logic QF_S) +(set-info :status unsat) +(declare-fun a () String) +(declare-fun b () String) +(declare-fun c () String) +(declare-fun d () String) +(declare-fun e () String) +(declare-fun f () String) +(declare-fun g () String) +(assert (= (str.++ "abc" a "def" b "gg" c) (str.++ e g f))) +(assert (or (= a "a") (= a "aaa"))) +(assert (or (= b "b") (= b "bbb"))) +(assert (or (= c "c") (= c "ccc"))) +(assert (or (= g (str.++ ";" d)) (= g (str.++ d ";")))) +(check-sat)