From: Andrew Reynolds Date: Thu, 22 Aug 2019 14:55:31 +0000 (-0500) Subject: Local substitutions for context-depdendent simplification in strings (#3204) X-Git-Tag: cvc5-1.0.0~4002 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b58bdc9c5672430cf15914c64129136b24050152;p=cvc5.git Local substitutions for context-depdendent simplification in strings (#3204) --- diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 93a166824..1eb2e8e00 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -368,47 +368,58 @@ bool TheoryStrings::getCurrentSubstitution( int effort, std::vector< Node >& var for( unsigned i=0; i=3 ){ - //model values - Node mv = d_valuation.getModel()->getRepresentative( n ); - Trace("strings-subs") << " model val : " << mv << std::endl; - subs.push_back( mv ); - }else{ - Node nr = getRepresentative( n ); - std::map< Node, Node >::iterator itc = d_eqc_to_const.find( nr ); - if( itc!=d_eqc_to_const.end() ){ - //constant equivalence classes - Trace("strings-subs") << " constant eqc : " << d_eqc_to_const_exp[nr] << " " << d_eqc_to_const_base[nr] << " " << nr << std::endl; - subs.push_back( itc->second ); - if( !d_eqc_to_const_exp[nr].isNull() ){ - exp[n].push_back( d_eqc_to_const_exp[nr] ); - } - if( !d_eqc_to_const_base[nr].isNull() ){ - addToExplanation( n, d_eqc_to_const_base[nr], exp[n] ); - } - }else if( effort>=1 && effort<3 && n.getType().isString() ){ - //normal forms - NormalForm& nfnr = getNormalForm(nr); - Node ns = getNormalString(nfnr.d_base, exp[n]); - subs.push_back( ns ); - Trace("strings-subs") << " normal eqc : " << ns << " " << nfnr.d_base - << " " << nr << std::endl; - if (!nfnr.d_base.isNull()) - { - addToExplanation(n, nfnr.d_base, exp[n]); - } - }else{ - //representative? - //Trace("strings-subs") << " representative : " << nr << std::endl; - //addToExplanation( n, nr, exp[n] ); - //subs.push_back( nr ); - subs.push_back( n ); - } - } + Node s = getCurrentSubstitutionFor(effort, n, exp[n]); + subs.push_back(s); } return true; } +Node TheoryStrings::getCurrentSubstitutionFor(int effort, + Node n, + std::vector& exp) +{ + if (effort >= 3) + { + // model values + Node mv = d_valuation.getModel()->getRepresentative(n); + Trace("strings-subs") << " model val : " << mv << std::endl; + return mv; + } + Node nr = getRepresentative(n); + std::map::iterator itc = d_eqc_to_const.find(nr); + if (itc != d_eqc_to_const.end()) + { + // constant equivalence classes + Trace("strings-subs") << " constant eqc : " << d_eqc_to_const_exp[nr] + << " " << d_eqc_to_const_base[nr] << " " << nr + << std::endl; + if (!d_eqc_to_const_exp[nr].isNull()) + { + exp.push_back(d_eqc_to_const_exp[nr]); + } + if (!d_eqc_to_const_base[nr].isNull()) + { + addToExplanation(n, d_eqc_to_const_base[nr], exp); + } + return itc->second; + } + else if (effort >= 1 && n.getType().isString()) + { + Assert(effort < 3); + // normal forms + NormalForm& nfnr = getNormalForm(nr); + Node ns = getNormalString(nfnr.d_base, exp); + Trace("strings-subs") << " normal eqc : " << ns << " " << nfnr.d_base + << " " << nr << std::endl; + if (!nfnr.d_base.isNull()) + { + addToExplanation(n, nfnr.d_base, exp); + } + return ns; + } + return n; +} + bool TheoryStrings::doReduction(int effort, Node n, bool& isCd) { Assert(d_extf_info_tmp.find(n) != d_extf_info_tmp.end()); @@ -1589,7 +1600,9 @@ void TheoryStrings::checkInit() { getExtTheory()->markCongruent( nc, n ); } //this node is congruent to another one, we can ignore it - Trace("strings-process-debug") << " congruent term : " << n << std::endl; + Trace("strings-process-debug") + << " congruent term : " << n << " (via " << nc << ")" + << std::endl; d_congruent.insert( n ); congruent[k]++; }else if( k==kind::STRING_CONCAT && c.size()==1 ){ @@ -1746,15 +1759,12 @@ void TheoryStrings::checkConstantEquivalenceClasses( TermIndex* ti, std::vector< void TheoryStrings::checkExtfEval( int effort ) { Trace("strings-extf-list") << "Active extended functions, effort=" << effort << " : " << std::endl; d_extf_info_tmp.clear(); + NodeManager* nm = NodeManager::currentNM(); bool has_nreduce = false; std::vector< Node > terms = getExtTheory()->getActive(); - std::vector< Node > sterms; - std::vector< std::vector< Node > > exp; - getExtTheory()->getSubstitutedTerms( effort, terms, sterms, exp ); - for( unsigned i=0; i::iterator itcit = d_eqc_to_const.find(r); @@ -1762,13 +1772,39 @@ void TheoryStrings::checkExtfEval( int effort ) { { einfo.d_const = itcit->second; } - Trace("strings-extf-debug") << "Check extf " << n << " == " << sn - << ", constant = " << einfo.d_const - << ", effort=" << effort << "..." << std::endl; - //do the inference + // Get the current values of the children of n. + // Notice that we look up the value of the direct children of n, and not + // their free variables. In other words, given a term: + // t = (str.replace "B" (str.replace x "A" "B") "C") + // we may build the explanation that: + // ((str.replace x "A" "B") = "B") => t = (str.replace "B" "B" "C") + // instead of basing this on the free variable x: + // (x = "A") => t = (str.replace "B" (str.replace "A" "A" "B") "C") + // Although both allow us to infer t = "C", it is important to use the + // first kind of inference since it ensures that its subterms have the + // expected values. Otherwise, we may in rare cases fail to realize that + // the subterm (str.replace x "A" "B") does not currently have the correct + // value, say in this example that (str.replace x "A" "B") != "B". + std::vector exp; + std::vector schildren; + bool schanged = false; + for (const Node& nc : n) + { + Node sc = getCurrentSubstitutionFor(effort, nc, exp); + schildren.push_back(sc); + schanged = schanged || sc != nc; + } + // If there is information involving the children, attempt to do an + // inference and/or mark n as reduced. Node to_reduce; - if( n!=sn ){ - einfo.d_exp.insert(einfo.d_exp.end(), exp[i].begin(), exp[i].end()); + if (schanged) + { + Node sn = nm->mkNode(n.getKind(), schildren); + Trace("strings-extf-debug") + << "Check extf " << n << " == " << sn + << ", constant = " << einfo.d_const << ", effort=" << effort << "..." + << std::endl; + einfo.d_exp.insert(einfo.d_exp.end(), exp.begin(), exp.end()); // inference is rewriting the substituted node Node nrc = Rewriter::rewrite( sn ); //if rewrites to a constant, then do the inference and mark as reduced @@ -1876,8 +1912,10 @@ void TheoryStrings::checkExtfEval( int effort ) { } to_reduce = nrc; } - }else{ - to_reduce = sterms[i]; + } + else + { + to_reduce = n; } //if not reduced if( !to_reduce.isNull() ){ diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 3d4b28e7f..94811636c 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -305,7 +305,21 @@ private: std::map< Node, Node > d_eqc_to_const_base; std::map< Node, Node > d_eqc_to_const_exp; Node getConstantEqc( Node eqc ); - + /** + * Get the current substitution for term n. + * + * This method returns a term that n is currently equal to in the current + * context. It updates exp to contain an explanation of why it is currently + * equal to that term. + * + * The argument effort determines what kind of term to return, either + * a constant in the equivalence class of n (effort=0), the normal form of + * n (effort=1,2) or the model value of n (effort>=3). The latter is only + * valid at LAST_CALL effort. If a term of the above form cannot be returned, + * then n itself is returned. + */ + Node getCurrentSubstitutionFor(int effort, Node n, std::vector& exp); + std::map< Node, Node > d_eqc_to_len_term; std::vector< Node > d_strings_eqc; Node d_emptyString_r; diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 5579885c3..8fa0c2791 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1814,6 +1814,7 @@ set(regress_2_tests regress2/strings/cmu-disagree-0707-dd.smt2 regress2/strings/cmu-prereg-fmf.smt2 regress2/strings/cmu-repl-len-nterm.smt2 + regress2/strings/issue3203.smt2 regress2/strings/issue918.smt2 regress2/strings/non_termination_regular_expression6.smt2 regress2/strings/norn-dis-0707-3.smt2 diff --git a/test/regress/regress2/strings/issue3203.smt2 b/test/regress/regress2/strings/issue3203.smt2 new file mode 100644 index 000000000..89c203889 --- /dev/null +++ b/test/regress/regress2/strings/issue3203.smt2 @@ -0,0 +1,17 @@ +(set-logic ALL_SUPPORTED) +(set-option :strings-exp true) +(set-info :status unsat) +(declare-fun a () String) +(declare-fun b () String) +(declare-fun d () String) +(declare-fun e () String) +(declare-fun f () Int) +(declare-fun g () String) +(declare-fun h () String) +(assert (or + (not (= ( str.replace "B" ( str.at "A" f) "") "B")) + (not (= ( str.replace "B" ( str.replace "B" g "") "") + ( str.at ( str.replace ( str.replace a d "") "C" "") ( str.indexof "B" ( str.replace ( str.replace a d "") "C" "") 0)))))) +(assert (= a (str.++ (str.++ d "C") g))) +(assert (= b (str.++ e g))) +(check-sat)