From: Andrew Reynolds Date: Tue, 23 Apr 2019 18:40:27 +0000 (-0500) Subject: Refactor normal forms in strings (#2897) X-Git-Tag: cvc5-1.0.0~4169 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=53cade050e191c7c0dc0ebfae716a21162bd9b22;p=cvc5.git Refactor normal forms in strings (#2897) --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 372888d36..cff31dbcd 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -625,6 +625,8 @@ libcvc4_add_sources( theory/shared_terms_database.h theory/sort_inference.cpp theory/sort_inference.h + theory/strings/normal_form.cpp + theory/strings/normal_form.h theory/strings/regexp_elim.cpp theory/strings/regexp_elim.h theory/strings/regexp_operation.cpp diff --git a/src/theory/strings/normal_form.cpp b/src/theory/strings/normal_form.cpp new file mode 100644 index 000000000..c70845d64 --- /dev/null +++ b/src/theory/strings/normal_form.cpp @@ -0,0 +1,163 @@ +/********************* */ +/*! \file normal_form.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of normal form data structure for the theory of + ** strings. + **/ + +#include "theory/strings/normal_form.h" + +#include "options/strings_options.h" +#include "theory/rewriter.h" + +using namespace std; +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace strings { + +void NormalForm::init(Node base) +{ + Assert(base.getType().isString()); + Assert(base.getKind() != STRING_CONCAT); + d_base = base; + d_nf.clear(); + d_isRev = false; + d_exp.clear(); + d_expDep.clear(); + + // add to normal form + if (!base.isConst() || !base.getConst().isEmptyString()) + { + d_nf.push_back(base); + } +} + +void NormalForm::reverse() +{ + std::reverse(d_nf.begin(), d_nf.end()); + d_isRev = !d_isRev; +} + +void NormalForm::splitConstant(unsigned index, Node c1, Node c2) +{ + Assert(Rewriter::rewrite(NodeManager::currentNM()->mkNode( + STRING_CONCAT, d_isRev ? c2 : c1, d_isRev ? c1 : c2)) + == d_nf[index]); + d_nf.insert(d_nf.begin() + index + 1, c2); + d_nf[index] = c1; + // update the dependency indices + // notice this is not critical for soundness: not doing the below incrementing + // will only lead to overapproximating when antecedants are required in + // explanations + for (const std::pair >& pe : d_expDep) + { + for (const std::pair& pep : pe.second) + { + // See if this can be incremented: it can if this literal is not relevant + // to the current index, and hence it is not relevant for both c1 and c2. + Assert(pep.second >= 0 && pep.second <= d_nf.size()); + bool increment = (pep.first == d_isRev) + ? pep.second > index + : (d_nf.size() - 1 - pep.second) < index; + if (increment) + { + d_expDep[pe.first][pep.first] = pep.second + 1; + } + } + } +} + +void NormalForm::addToExplanation(Node exp, + unsigned new_val, + unsigned new_rev_val) +{ + if (std::find(d_exp.begin(), d_exp.end(), exp) == d_exp.end()) + { + d_exp.push_back(exp); + } + for (unsigned k = 0; k < 2; k++) + { + unsigned val = k == 0 ? new_val : new_rev_val; + std::map::iterator itned = d_expDep[exp].find(k == 1); + if (itned == d_expDep[exp].end()) + { + Trace("strings-process-debug") + << "Deps : set dependency on " << exp << " to " << val + << " isRev=" << (k == 0) << std::endl; + d_expDep[exp][k == 1] = val; + } + else + { + Trace("strings-process-debug") + << "Deps : Multiple dependencies on " << exp << " : " << itned->second + << " " << val << " isRev=" << (k == 0) << std::endl; + // if we already have a dependency (in the case of non-linear string + // equalities), it is min/max + bool cmp = val > itned->second; + if (cmp == (k == 1)) + { + d_expDep[exp][k == 1] = val; + } + } + } +} + +void NormalForm::getExplanation(int index, std::vector& curr_exp) +{ + if (index == -1 || !options::stringMinPrefixExplain()) + { + curr_exp.insert(curr_exp.end(), d_exp.begin(), d_exp.end()); + return; + } + for (const Node& exp : d_exp) + { + int dep = static_cast(d_expDep[exp][d_isRev]); + if (dep <= index) + { + curr_exp.push_back(exp); + Trace("strings-explain-prefix-debug") << " include : "; + } + else + { + Trace("strings-explain-prefix-debug") << " exclude : "; + } + Trace("strings-explain-prefix-debug") << exp << std::endl; + } +} + +void NormalForm::getExplanationForPrefixEq(NormalForm& nfi, + NormalForm& nfj, + int index_i, + int index_j, + std::vector& curr_exp) +{ + Assert(nfi.d_isRev == nfj.d_isRev); + Trace("strings-explain-prefix") + << "Get explanation for prefix " << index_i << ", " << index_j + << ", reverse = " << nfi.d_isRev << std::endl; + // get explanations + nfi.getExplanation(index_i, curr_exp); + nfj.getExplanation(index_j, curr_exp); + Trace("strings-explain-prefix") + << "Included " << curr_exp.size() << " / " + << (nfi.d_exp.size() + nfj.d_exp.size()) << std::endl; + if (nfi.d_base != nfj.d_base) + { + Node eq = nfi.d_base.eqNode(nfj.d_base); + curr_exp.push_back(eq); + } +} + +} // namespace strings +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/strings/normal_form.h b/src/theory/strings/normal_form.h new file mode 100644 index 000000000..73036e68f --- /dev/null +++ b/src/theory/strings/normal_form.h @@ -0,0 +1,159 @@ +/********************* */ +/*! \file normal_form.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Normal form datastructure for the theory of strings. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__STRINGS__NORMAL_FORM_H +#define __CVC4__THEORY__STRINGS__NORMAL_FORM_H + +#include +#include +#include "expr/node.h" + +namespace CVC4 { +namespace theory { +namespace strings { + +/** normal forms + * + * Stores information regarding the "normal form" of terms t in the current + * context. Normal forms can be associated with terms, or with string + * equivalence classes. For the latter, the normal form of an equivalence class + * exists if exactly one unique normal form is associated to a subset of its + * terms. + * + * In the following we use example where assertions are: + * { x = y, y = z, y = u ++ v, u = u1 ++ u2 } + * and equivalence class [x] = { x, y, z, u ++ v }, whose normal form is + * (u1, u2, v) + */ +class NormalForm +{ + public: + NormalForm() : d_isRev(false) {} + /** + * The "base" of the normal form. This is some term in the equivalence + * class of t that the normal form is based on. This is an arbitrary term + * which is used as the reference point for explanations. In the above + * running example, let us assume the base of [x] is y. + */ + Node d_base; + /** the normal form, (u1, u2, v), in the above example */ + std::vector d_nf; + /** is the normal form d_nf stored in reverse order? */ + bool d_isRev; + /** + * The explanation for the normal form, this is a set of literals such that + * d_exp => d_base = d_nf + * In the above example, this is the set of equalities + * { y = u ++ v, u = u1 ++ u2 } + * If u ++ v was chosen as the base, then the first literal could be omitted. + */ + std::vector d_exp; + /** + * Map from literals in the vector d_exp to integers indicating indices in + * d_nf for which that literal L is relevant for explaining d_base = d_nf. + * + * In particular: + * - false maps to an (ideally maximal) index relative to the start of d_nf + * such that L is required for explaining why d_base has a prefix that + * includes the term at that index, + * - true maps to an (ideally maximal) index relative to the end of d_nf + * such that L is required for explaining why d_base has a suffix that + * includes the term at that index. + * We call these the forward and backwards dependency indices. + * + * In the above example: + * y = u ++ v : false -> 0, true -> 0 + * u = u1 ++ u2 : false -> 0, true -> 1 + * When explaining y = u1 ++ u2 ++ v, the equality y = u ++ v is required + * for explaining any prefix/suffix of y and its normal form. More + * interestingly, the equality u = u1 ++ u2 is not required for explaining + * that v is a suffix of y, since its reverse index in this map is 1, + * indicating that "u2" is the first position in u1 ++ u2 ++ v that it is + * required for explaining. + * + * This information is used to minimize explanations when conflicts arise, + * thereby strengthening conflict clauses and lemmas. + * + * For example, say u ++ v = y = x = u ++ w and w and v are distinct + * constants, using this dependency information, we could construct a + * conflict: + * x = y ^ y = u ++ v ^ x = u ++ w + * that does not include u = u1 ++ u2, because the conflict only pertains + * to the last position in the normal form of y. + */ + std::map > d_expDep; + /** initialize + * + * Initialize the normal form with base node base. If base is not the empty + * string, then d_nf is set to the singleton list containing base, otherwise + * d_nf is empty. + */ + void init(Node base); + /** reverse the content of normal form d_nf + * + * This operation is done in contexts where the normal form is being scanned + * in reverse order. + */ + void reverse(); + /** split constant + * + * Splits the constant in d_nf at index to constants c1 and c2. + * + * Notice this function depends on whether the normal form has been reversed + * d_isRev, as this impacts how the dependency indices are updated. + */ + void splitConstant(unsigned index, Node c1, Node c2); + /** add to explanation + * + * This adds exp to the explanation vector d_exp with new forward and + * backwards dependency indices new_val and new_rev_val. + * + * If exp already has dependencies, we update the forward dependency + * index to the minimum of the previous value and the new value, and + * similarly update the backwards dependency index to the maximum. + */ + void addToExplanation(Node exp, unsigned new_val, unsigned new_rev_val); + /** get explanation + * + * This gets the explanation for the prefix (resp. suffix) of the normal + * form up to index when d_isRev is false (resp. true). In particular; + * + * If index is -1, then this method adds all literals in d_exp to curr_exp. + * + * If index>=0, this method adds all literals in d_exp to curr_exp whose + * forward (resp. backwards) dependency index is less than index + * when isRev is false (resp. true). + */ + void getExplanation(int index, std::vector& curr_exp); + /** get explanation for prefix equality + * + * This adds to curr_exp the reason why the prefix of nfi up to index index_i + * is equivalent to the prefix of nfj up to index_j. The values of + * nfi.d_isRev and nfj.d_isRev affect how dependency indices are updated + * during this call. + */ + static void getExplanationForPrefixEq(NormalForm& nfi, + NormalForm& nfj, + int index_i, + int index_j, + std::vector& curr_exp); +}; + +} // namespace strings +} // namespace theory +} // namespace CVC4 + +#endif /* __CVC4__THEORY__STRINGS__NORMAL_FORM_H */ diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 8731bd1a5..c2b87fbef 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -253,13 +253,13 @@ Node TheoryStrings::getNormalString(Node x, std::vector& nf_exp) if (!x.isConst()) { Node xr = getRepresentative(x); - if (d_normal_forms.find(xr) != d_normal_forms.end()) + std::map::iterator it = d_normal_form.find(xr); + if (it != d_normal_form.end()) { - Node ret = mkConcat(d_normal_forms[xr]); - nf_exp.insert(nf_exp.end(), - d_normal_forms_exp[xr].begin(), - d_normal_forms_exp[xr].end()); - addToExplanation(x, d_normal_forms_base[xr], nf_exp); + NormalForm& nf = it->second; + Node ret = mkConcat(nf.d_nf); + nf_exp.insert(nf_exp.end(), nf.d_exp.begin(), nf.d_exp.end()); + addToExplanation(x, nf.d_base, nf_exp); Trace("strings-debug") << "Term: " << x << " has a normal form " << ret << std::endl; return ret; @@ -400,11 +400,14 @@ bool TheoryStrings::getCurrentSubstitution( int effort, std::vector< Node >& var } }else if( effort>=1 && effort<3 && n.getType().isString() ){ //normal forms - Node ns = getNormalString( d_normal_forms_base[nr], exp[n] ); + NormalForm& nfnr = getNormalForm(nr); + Node ns = getNormalString(nfnr.d_base, exp[n]); subs.push_back( ns ); - Trace("strings-subs") << " normal eqc : " << ns << " " << d_normal_forms_base[nr] << " " << nr << std::endl; - if( !d_normal_forms_base[nr].isNull() ) { - addToExplanation( n, d_normal_forms_base[nr], exp[n] ); + 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? @@ -671,8 +674,8 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m) //check if col[i][j] has only variables if (!eqc.isConst()) { - Assert(d_normal_forms.find(eqc) != d_normal_forms.end()); - if (d_normal_forms[eqc].size() == 1) + NormalForm& nfe = getNormalForm(eqc); + if (nfe.d_nf.size() == 1) { // does it have a code and the length of these equivalence classes are // one? @@ -795,20 +798,31 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m) //step 4 : assign constants to all other equivalence classes for( unsigned i=0; i0 ) 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)"; + NormalForm& nf = getNormalForm(nodes[i]); + if (Trace.isOn("strings-model")) + { + Trace("strings-model") + << "Construct model for " << nodes[i] << " based on normal form "; + for (unsigned j = 0, size = nf.d_nf.size(); j < size; j++) + { + Node n = nf.d_nf[j]; + if (j > 0) + { + Trace("strings-model") << " ++ "; + } + Trace("strings-model") << n; + Node r = getRepresentative(n); + 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 nf_to_eqc; std::map eqc_to_nf; std::map eqc_to_exp; @@ -2490,16 +2503,17 @@ void TheoryStrings::checkNormalFormsEq() { return; } - Node nf_term = mkConcat(d_normal_forms[eqc]); + NormalForm& nfe = getNormalForm(eqc); + Node nf_term = mkConcat(nfe.d_nf); std::map::iterator itn = nf_to_eqc.find(nf_term); if (itn != nf_to_eqc.end()) { + NormalForm& nfe_eq = getNormalForm(itn->second); // two equivalence classes have same normal form, merge std::vector nf_exp; - nf_exp.push_back(mkAnd(d_normal_forms_exp[eqc])); + nf_exp.push_back(mkAnd(nfe.d_exp)); nf_exp.push_back(eqc_to_exp[itn->second]); - Node eq = - d_normal_forms_base[eqc].eqNode(d_normal_forms_base[itn->second]); + Node eq = nfe.d_base.eqNode(nfe_eq.d_base); sendInference(nf_exp, eq, "Normal_Form"); if( hasProcessed() ){ return; @@ -2509,7 +2523,7 @@ void TheoryStrings::checkNormalFormsEq() { nf_to_eqc[nf_term] = eqc; eqc_to_nf[eqc] = nf_term; - eqc_to_exp[eqc] = mkAnd(d_normal_forms_exp[eqc]); + eqc_to_exp[eqc] = mkAnd(nfe.d_exp); } Trace("strings-process-debug") << "Done verifying normal forms are the same for " << eqc << std::endl; @@ -2521,8 +2535,8 @@ void TheoryStrings::checkNormalFormsEq() it != eqc_to_exp.end(); ++it) { - Trace("strings-nf") << " N[" << it->first << "] (base " - << d_normal_forms_base[it->first] + NormalForm& nf = getNormalForm(it->first); + Trace("strings-nf") << " N[" << it->first << "] (base " << nf.d_base << ") = " << eqc_to_nf[it->first] << std::endl; Trace("strings-nf") << " exp: " << it->second << std::endl; } @@ -2545,9 +2559,10 @@ void TheoryStrings::checkCodes() std::vector const_codes; for (const Node& eqc : d_strings_eqc) { - if (d_normal_forms[eqc].size() == 1 && d_normal_forms[eqc][0].isConst()) + NormalForm& nfe = getNormalForm(eqc); + if (nfe.d_nf.size() == 1 && nfe.d_nf[0].isConst()) { - Node c = d_normal_forms[eqc][0]; + Node c = nfe.d_nf[0]; Trace("strings-code-debug") << "Get proxy variable for " << c << std::endl; Node cc = nm->mkNode(kind::STRING_CODE, c); @@ -2616,83 +2631,65 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc ) { #endif //do nothing Trace("strings-process-debug") << "Return process equivalence class " << eqc << " : empty." << std::endl; - d_normal_forms_base[eqc] = d_emptyString; - d_normal_forms[eqc].clear(); - d_normal_forms_exp[eqc].clear(); + d_normal_form[eqc].init(d_emptyString); } else { - Assert( d_normal_forms.find(eqc)==d_normal_forms.end() ); - //phi => t = s1 * ... * sn - // normal form for each non-variable term in this eqc (s1...sn) - std::vector< std::vector< Node > > normal_forms; - // explanation for each normal form (phi) - std::vector< std::vector< Node > > normal_forms_exp; - // dependency information - std::vector< std::map< Node, std::map< bool, int > > > normal_forms_exp_depend; - // record terms for each normal form (t) - std::vector< Node > normal_form_src; - // get normal forms - getNormalForms(eqc, normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend); + // should not have computed the normal form of this equivalence class yet + Assert(d_normal_form.find(eqc) == d_normal_form.end()); + // Normal forms for the relevant terms in the equivalence class of eqc + std::vector normal_forms; + // map each term to its index in the above vector + std::map term_to_nf_index; + // get the normal forms + getNormalForms(eqc, normal_forms, term_to_nf_index); if( hasProcessed() ){ return; } // process the normal forms - processNEqc( normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend ); + processNEqc(normal_forms); if( hasProcessed() ){ return; } - //debugPrintNormalForms( "strings-solve", eqc, normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend ); - + // debugPrintNormalForms( "strings-solve", eqc, normal_forms ); + //construct the normal form Assert( !normal_forms.empty() ); - - int nf_index = 0; - std::vector< Node >::iterator itn = std::find( normal_form_src.begin(), normal_form_src.end(), eqc ); - if( itn!=normal_form_src.end() ){ - nf_index = itn - normal_form_src.begin(); - Trace("strings-solve-debug2") << "take normal form " << nf_index << std::endl; - Assert( normal_form_src[nf_index]==eqc ); - }else{ - //just take the first normal form - Trace("strings-solve-debug2") << "take the first normal form" << std::endl; - } - d_normal_forms[eqc].insert( d_normal_forms[eqc].end(), normal_forms[nf_index].begin(), normal_forms[nf_index].end() ); - d_normal_forms_exp[eqc].insert( d_normal_forms_exp[eqc].end(), normal_forms_exp[nf_index].begin(), normal_forms_exp[nf_index].end() ); - Trace("strings-solve-debug2") << "take normal form ... done" << std::endl; - d_normal_forms_base[eqc] = normal_form_src[nf_index]; - //track dependencies - for( unsigned i=0; i::iterator it = term_to_nf_index.find(eqc); + // we prefer taking the normal form whose base is the equivalence + // class representative, since this leads to shorter explanations in + // some cases. + if (it != term_to_nf_index.end()) + { + nf_index = it->second; } - Trace("strings-process-debug") << "Return process equivalence class " << eqc << " : returned, size = " << d_normal_forms[eqc].size() << std::endl; + d_normal_form[eqc] = normal_forms[nf_index]; + Trace("strings-process-debug") + << "Return process equivalence class " << eqc + << " : returned, size = " << d_normal_form[eqc].d_nf.size() + << std::endl; } } -void trackNfExpDependency( std::vector< Node >& nf_exp_n, std::map< Node, std::map< bool, int > >& nf_exp_depend_n, Node exp, int new_val, int new_rev_val ){ - if( std::find( nf_exp_n.begin(), nf_exp_n.end(), exp )==nf_exp_n.end() ){ - nf_exp_n.push_back( exp ); - } - for( unsigned k=0; k<2; k++ ){ - int val = k==0 ? new_val : new_rev_val; - std::map< bool, int >::iterator itned = nf_exp_depend_n[exp].find( k==1 ); - if( itned==nf_exp_depend_n[exp].end() ){ - Trace("strings-process-debug") << "Deps : set dependency on " << exp << " to " << val << " isRev=" << (k==0) << std::endl; - nf_exp_depend_n[exp][k==1] = val; - }else{ - Trace("strings-process-debug") << "Deps : Multiple dependencies on " << exp << " : " << itned->second << " " << val << " isRev=" << (k==0) << std::endl; - //if we already have a dependency (in the case of non-linear string equalities), it is min/max - bool cmp = val > itned->second; - if( cmp==(k==1) ){ - nf_exp_depend_n[exp][k==1] = val; - } - } +NormalForm& TheoryStrings::getNormalForm(Node n) +{ + std::map::iterator itn = d_normal_form.find(n); + if (itn == d_normal_form.end()) + { + Trace("strings-warn") << "WARNING: returning empty normal form for " << n + << std::endl; + // Shouln't ask for normal forms of strings that weren't computed. This + // likely means that n is not a representative or not a term in the current + // context. We simply return a default normal form here in this case. + Assert(false); + return d_normal_form[n]; } + return itn->second; } -void 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 ) { +void TheoryStrings::getNormalForms(Node eqc, + std::vector& normal_forms, + std::map& term_to_nf_index) +{ //constant for equivalence class Node eqc_non_c = eqc; Trace("strings-process-debug") << "Get normal forms " << eqc << std::endl; @@ -2700,79 +2697,115 @@ void TheoryStrings::getNormalForms( Node &eqc, std::vector< std::vector< Node > while( !eqc_i.isFinished() ){ Node n = (*eqc_i); if( d_congruent.find( n )==d_congruent.end() ){ - if( n.getKind() == kind::CONST_STRING || n.getKind() == kind::STRING_CONCAT ){ + if (n.getKind() == CONST_STRING || n.getKind() == STRING_CONCAT) + { Trace("strings-process-debug") << "Get Normal Form : Process term " << n << " in eqc " << eqc << std::endl; - std::vector< Node > nf_n; - std::vector< Node > nf_exp_n; - std::map< Node, std::map< bool, int > > nf_exp_depend_n; - if( n.getKind()==kind::CONST_STRING ){ - if( n!=d_emptyString ) { - nf_n.push_back( n ); - } - }else if( n.getKind()==kind::STRING_CONCAT ){ + NormalForm nf_curr; + if (n.getKind() == CONST_STRING) + { + nf_curr.init(n); + } + else if (n.getKind() == STRING_CONCAT) + { + // set the base to n, we construct the other portions of nf_curr in + // the following. + nf_curr.d_base = n; for( unsigned i=0; i& nfrv = nfr.d_nf; Trace("strings-process-debug") << "Normalizing subterm " << n[i] << " = " << nr << std::endl; - Assert( d_normal_forms.find( nr )!=d_normal_forms.end() ); - unsigned orig_size = nf_n.size(); - unsigned add_size = d_normal_forms[nr].size(); + unsigned orig_size = nf_curr.d_nf.size(); + unsigned add_size = nfrv.size(); //if not the empty string, add to current normal form - if( !d_normal_forms[nr].empty() ){ - for( unsigned r=0; r >::iterator it = nf_exp_depend_n.begin(); it != nf_exp_depend_n.end(); ++it ){ - it->second[true] = total_size - it->second[true]; - Assert( it->second[true]>=0 ); + // Now that we are finished with the loop, we convert forward indices + // to reverse indices in the explanation dependency information + int total_size = nf_curr.d_nf.size(); + for (std::pair >& ed : + nf_curr.d_expDep) + { + ed.second[true] = total_size - ed.second[true]; + Assert(ed.second[true] >= 0); } } //if not equal to self - if( nf_n.size()>1 || ( nf_n.size()==1 && nf_n[0].getKind()==kind::CONST_STRING ) ){ - if( nf_n.size()>1 ) { - for( unsigned i=0; i& currv = nf_curr.d_nf; + if (currv.size() > 1 + || (currv.size() == 1 && currv[0].getKind() == CONST_STRING)) + { + // if in a build with assertions, check that normal form is acyclic + if (Configuration::isAssertionBuild()) + { + if (currv.size() > 1) + { + for (unsigned i = 0; i < currv.size(); i++) + { + if (Trace.isOn("strings-error")) + { + Trace("strings-error") << "Cycle for normal form "; + printConcat(currv, "strings-error"); + Trace("strings-error") << "..." << currv[i] << std::endl; + } + Assert(!areEqual(currv[i], n)); } - Assert( !areEqual( nf_n[i], n ) ); } } - normal_forms.push_back(nf_n); - normal_form_src.push_back(n); - normal_forms_exp.push_back(nf_exp_n); - normal_forms_exp_depend.push_back(nf_exp_depend_n); + term_to_nf_index[n] = normal_forms.size(); + normal_forms.push_back(nf_curr); }else{ //this was redundant: combination of self + empty string(s) - Node nn = nf_n.size()==0 ? d_emptyString : nf_n[0]; + Node nn = currv.size() == 0 ? d_emptyString : currv[0]; Assert( areEqual( nn, eqc ) ); } }else{ @@ -2784,41 +2817,56 @@ void TheoryStrings::getNormalForms( Node &eqc, std::vector< std::vector< Node > if( normal_forms.empty() ) { Trace("strings-solve-debug2") << "construct the normal form" << std::endl; - //do not choose a concat here use "eqc_non_c" (in this case they have non-trivial explanation why they normalize to self) - std::vector< Node > eqc_non_c_nf; - getConcatVec( eqc_non_c, eqc_non_c_nf ); - normal_forms.push_back( eqc_non_c_nf ); - normal_form_src.push_back( eqc_non_c ); - normal_forms_exp.push_back( std::vector< Node >() ); - normal_forms_exp_depend.push_back( std::map< Node, std::map< bool, int > >() ); + // This case happens when there are no non-trivial normal forms for this + // equivalence class. For example, given assertions: + // { x = y ++ z, x = y, z = "" } + // The equivalence class of { x, y, y ++ z } is such that the normal form + // of all terms is a variable (either x or y) in the equivalence class + // itself. Thus, the normal form of this equivalence class can be assigned + // to one of these variables. + // We use a non-concatenation term among the terms in this equivalence + // class, which is stored in eqc_non_c. The reason is this does not require + // an explanation, whereas e.g. y ++ z would require the explanation z = "" + // to justify its normal form is y. + Assert(eqc_non_c.getKind() != STRING_CONCAT); + NormalForm nf_triv; + nf_triv.init(eqc_non_c); + normal_forms.push_back(nf_triv); }else{ if(Trace.isOn("strings-solve")) { Trace("strings-solve") << "--- Normal forms for equivalance class " << eqc << " : " << std::endl; - for( unsigned i=0; i0) { Trace("strings-solve") << ", "; } - Trace("strings-solve") << normal_forms[i][j]; + Trace("strings-solve") << nf.d_nf[j]; } Trace("strings-solve") << std::endl; Trace("strings-solve") << " Explanation is : "; - if(normal_forms_exp[i].size() == 0) { + if (nf.d_exp.size() == 0) + { Trace("strings-solve") << "NONE"; } else { - for( unsigned j=0; j0) { Trace("strings-solve") << " AND "; } - Trace("strings-solve") << normal_forms_exp[i][j]; + Trace("strings-solve") << nf.d_exp[j]; } Trace("strings-solve") << std::endl; Trace("strings-solve") << "WITH DEPENDENCIES : " << std::endl; - for( unsigned j=0; j "; - Trace("strings-solve") << normal_forms_exp_depend[i][normal_forms_exp[i][j]][false] << ","; - Trace("strings-solve") << normal_forms_exp_depend[i][normal_forms_exp[i][j]][true] << std::endl; + for (unsigned j = 0, sizej = nf.d_exp.size(); j < sizej; j++) + { + Node exp = nf.d_exp[j]; + Trace("strings-solve") << " " << exp << " -> "; + Trace("strings-solve") << nf.d_expDep[exp][false] << ","; + Trace("strings-solve") << nf.d_expDep[exp][true] << std::endl; } } Trace("strings-solve") << std::endl; @@ -2832,10 +2880,14 @@ void TheoryStrings::getNormalForms( Node &eqc, std::vector< std::vector< Node > Node c = getConstantEqc( eqc ); if( !c.isNull() ){ Trace("strings-solve") << "Eqc is constant " << c << std::endl; - for( unsigned i=0; i 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() ); + exp.insert(exp.end(), nf.d_exp.begin(), nf.d_exp.end()); Node conc = d_false; sendInference( exp, conc, "N_NCTN" ); } @@ -2856,52 +2908,29 @@ void TheoryStrings::getNormalForms( Node &eqc, std::vector< std::vector< Node > } } -void TheoryStrings::getExplanationVectorForPrefix( std::vector< std::vector< Node > > &normal_forms_exp, std::vector< std::map< Node, std::map< bool, int > > >& normal_forms_exp_depend, - unsigned i, int index, bool isRev, std::vector< Node >& curr_exp ) { - if( index==-1 || !options::stringMinPrefixExplain() ){ - curr_exp.insert(curr_exp.end(), normal_forms_exp[i].begin(), normal_forms_exp[i].end() ); - }else{ - for( unsigned k=0; k > &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, - unsigned i, unsigned j, int index_i, int index_j, bool isRev, std::vector< Node >& curr_exp ) { - Trace("strings-explain-prefix") << "Get explanation for prefix " << index_i << ", " << index_j << " of normal forms " << i << " and " << j << ", reverse = " << isRev << std::endl; - for( unsigned r=0; r<2; r++ ){ - getExplanationVectorForPrefix( normal_forms_exp, normal_forms_exp_depend, r==0 ? i : j, r==0 ? index_i : index_j, isRev, curr_exp ); - } - Trace("strings-explain-prefix") << "Included " << curr_exp.size() << " / " << ( normal_forms_exp[i].size() + normal_forms_exp[j].size() ) << std::endl; - addToExplanation( normal_form_src[i], normal_form_src[j], curr_exp ); -} - - -void TheoryStrings::processNEqc( 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 ){ +void TheoryStrings::processNEqc(std::vector& normal_forms) +{ //the possible inferences std::vector< InferInfo > pinfer; // loop over all pairs for(unsigned i=0; i > &normal_form //rindex = 0; unsigned index = 0; - processSimpleNEq( normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend, i, j, index, false, rindex, pinfer ); + processSimpleNEq(nfi, nfj, index, false, rindex, pinfer); if( hasProcessed() ){ return; }else if( !pinfer.empty() && pinfer.back().d_id==1 ){ @@ -2977,86 +3006,92 @@ bool TheoryStrings::InferInfo::sendAsLemma() { return true; } -void TheoryStrings::processReverseNEq( 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, - unsigned i, unsigned j, unsigned& index, unsigned rproc, std::vector< InferInfo >& pinfer ) { - //reverse normal form of i, j - std::reverse( normal_forms[i].begin(), normal_forms[i].end() ); - std::reverse( normal_forms[j].begin(), normal_forms[j].end() ); - - processSimpleNEq( normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend, i, j, index, true, rproc, pinfer ); - - //reverse normal form of i, j - std::reverse( normal_forms[i].begin(), normal_forms[i].end() ); - std::reverse( normal_forms[j].begin(), normal_forms[j].end() ); -} - -//rproc is the # is the size of suffix that is identical -void TheoryStrings::processSimpleNEq( 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, - unsigned i, unsigned j, unsigned& index, bool isRev, unsigned rproc, std::vector< InferInfo >& pinfer ) { - Assert( rproc<=normal_forms[i].size() && rproc<=normal_forms[j].size() ); +void TheoryStrings::processSimpleNEq(NormalForm& nfi, + NormalForm& nfj, + unsigned& index, + bool isRev, + unsigned rproc, + std::vector& pinfer) +{ + std::vector& nfiv = nfi.d_nf; + std::vector& nfjv = nfj.d_nf; + NodeManager* nm = NodeManager::currentNM(); + Assert(rproc <= nfiv.size() && rproc <= nfjv.size()); bool success; do { success = false; //if we are at the end - if( index==(normal_forms[i].size()-rproc) || index==(normal_forms[j].size()-rproc) ){ - if( index==(normal_forms[i].size()-rproc) && index==(normal_forms[j].size()-rproc) ){ + if (index == (nfiv.size() - rproc) || index == (nfjv.size() - rproc)) + { + if (index == (nfiv.size() - rproc) && index == (nfjv.size() - rproc)) + { //we're done }else{ //the remainder must be empty - unsigned k = index==(normal_forms[i].size()-rproc) ? j : i; + NormalForm& nfk = index == (nfiv.size() - rproc) ? nfj : nfi; + std::vector& nfkv = nfk.d_nf; unsigned index_k = index; //Node eq_exp = mkAnd( curr_exp ); std::vector< Node > curr_exp; - getExplanationVectorForPrefixEq( normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend, i, j, -1, -1, isRev, curr_exp ); - while( !d_conflict && index_k<(normal_forms[k].size()-rproc) ){ + NormalForm::getExplanationForPrefixEq(nfi, nfj, -1, -1, curr_exp); + while (!d_conflict && index_k < (nfkv.size() - rproc)) + { //can infer that this string must be empty - Node eq = normal_forms[k][index_k].eqNode( d_emptyString ); + Node eq = nfkv[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] ) ); + Assert(!areEqual(d_emptyString, nfkv[index_k])); sendInference( curr_exp, eq, "N_EndpointEmp" ); index_k++; } } }else{ - Trace("strings-solve-debug") << "Process " << normal_forms[i][index] << " ... " << normal_forms[j][index] << std::endl; - if( normal_forms[i][index]==normal_forms[j][index] ){ + Trace("strings-solve-debug") + << "Process " << nfiv[index] << " ... " << nfjv[index] << std::endl; + if (nfiv[index] == nfjv[index]) + { Trace("strings-solve-debug") << "Simple Case 1 : strings are equal" << std::endl; index++; success = true; }else{ - Assert( !areEqual(normal_forms[i][index], normal_forms[j][index]) ); + Assert(!areEqual(nfiv[index], nfjv[index])); std::vector< Node > temp_exp; - Node length_term_i = getLength( normal_forms[i][index], temp_exp ); - Node length_term_j = getLength( normal_forms[j][index], temp_exp ); - //check length(normal_forms[i][index]) == length(normal_forms[j][index]) + Node length_term_i = getLength(nfiv[index], temp_exp); + Node length_term_j = getLength(nfjv[index], temp_exp); + // check length(nfiv[index]) == length(nfjv[index]) if( areEqual( length_term_i, length_term_j ) ){ Trace("strings-solve-debug") << "Simple Case 2 : string lengths are equal" << std::endl; - Node eq = normal_forms[i][index].eqNode( normal_forms[j][index] ); + Node eq = nfiv[index].eqNode(nfjv[index]); //eq = Rewriter::rewrite( eq ); Node length_eq = length_term_i.eqNode( length_term_j ); //temp_exp.insert(temp_exp.end(), curr_exp.begin(), curr_exp.end() ); - getExplanationVectorForPrefixEq( normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend, i, j, index, index, isRev, temp_exp ); + NormalForm::getExplanationForPrefixEq( + nfi, nfj, index, index, temp_exp); temp_exp.push_back(length_eq); sendInference( temp_exp, eq, "N_Unify" ); return; - }else if( ( normal_forms[i][index].getKind()!=kind::CONST_STRING && index==normal_forms[i].size()-rproc-1 ) || - ( normal_forms[j][index].getKind()!=kind::CONST_STRING && index==normal_forms[j].size()-rproc-1 ) ){ + } + else if ((nfiv[index].getKind() != CONST_STRING + && index == nfiv.size() - rproc - 1) + || (nfjv[index].getKind() != CONST_STRING + && index == nfjv.size() - rproc - 1)) + { Trace("strings-solve-debug") << "Simple Case 3 : at endpoint" << std::endl; std::vector< Node > antec; //antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() ); - getExplanationVectorForPrefixEq( normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend, i, j, -1, -1, isRev, antec ); + NormalForm::getExplanationForPrefixEq(nfi, nfj, -1, -1, antec); std::vector< Node > eqn; for( unsigned r=0; r<2; r++ ) { - int index_k = index; - int k = r==0 ? i : j; + NormalForm& nfk = r == 0 ? nfi : nfj; + std::vector& nfkv = nfk.d_nf; std::vector< Node > eqnc; - for( unsigned index_l=index_k; index_l<(normal_forms[k].size()-rproc); index_l++ ) { + for (unsigned index_l = index, size = (nfkv.size() - rproc); + index_l < size; + index_l++) + { if(isRev) { - eqnc.insert(eqnc.begin(), normal_forms[k][index_l] ); + eqnc.insert(eqnc.begin(), nfkv[index_l]); } else { - eqnc.push_back( normal_forms[k][index_l] ); + eqnc.push_back(nfkv[index_l]); } } eqn.push_back( mkConcat( eqnc ) ); @@ -3065,49 +3100,46 @@ void TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal sendInference( antec, eqn[0].eqNode( eqn[1] ), "N_EndpointEq", true ); return; }else{ - Assert( normal_forms[i].size()==normal_forms[j].size() ); - index = normal_forms[i].size()-rproc; + Assert(nfiv.size() == nfjv.size()); + index = nfiv.size() - rproc; } - }else if( normal_forms[i][index].isConst() && normal_forms[j][index].isConst() ){ - Node const_str = normal_forms[i][index]; - Node other_str = normal_forms[j][index]; + } + else if (nfiv[index].isConst() && nfjv[index].isConst()) + { + Node const_str = nfiv[index]; + Node other_str = nfjv[index]; Trace("strings-solve-debug") << "Simple Case 3 : Const Split : " << const_str << " vs " << other_str << " at index " << index << ", isRev = " << isRev << std::endl; unsigned len_short = const_str.getConst().size() <= other_str.getConst().size() ? const_str.getConst().size() : other_str.getConst().size(); bool isSameFix = isRev ? const_str.getConst().rstrncmp(other_str.getConst(), len_short): const_str.getConst().strncmp(other_str.getConst(), len_short); if( isSameFix ) { //same prefix/suffix + bool constCmp = const_str.getConst().size() + < other_str.getConst().size(); //k is the index of the string that is shorter - int k = const_str.getConst().size()().size() ? i : j; - int l = const_str.getConst().size()().size() ? j : i; - //update the nf exp dependencies - //notice this is not critical for soundness: not doing the below incrementing will only lead to overapproximating when antecedants are required in explanations - for( std::map< Node, std::map< bool, int > >::iterator itnd = normal_forms_exp_depend[l].begin(); itnd != normal_forms_exp_depend[l].end(); ++itnd ){ - for( std::map< bool, int >::iterator itnd2 = itnd->second.begin(); itnd2 != itnd->second.end(); ++itnd2 ){ - //see if this can be incremented: it can if it is not relevant to the current index - Assert( itnd2->second>=0 && itnd2->second<=(int)normal_forms[l].size() ); - bool increment = (itnd2->first==isRev) ? itnd2->second>(int)index : ( (int)normal_forms[l].size()-1-itnd2->second )<(int)index; - if( increment ){ - normal_forms_exp_depend[l][itnd->first][itnd2->first] = itnd2->second + 1; - } - } - } + NormalForm& nfk = constCmp ? nfi : nfj; + std::vector& nfkv = nfk.d_nf; + NormalForm& nfl = constCmp ? nfj : nfi; + std::vector& nflv = nfl.d_nf; + Node remainderStr; if( isRev ){ - int new_len = normal_forms[l][index].getConst().size() - len_short; - Node remainderStr = NodeManager::currentNM()->mkConst( normal_forms[l][index].getConst().substr(0, new_len) ); - Trace("strings-solve-debug-test") << "Break normal form of " << normal_forms[l][index] << " into " << normal_forms[k][index] << ", " << remainderStr << std::endl; - normal_forms[l].insert( normal_forms[l].begin()+index + 1, remainderStr ); + int new_len = nflv[index].getConst().size() - len_short; + remainderStr = nm->mkConst( + nflv[index].getConst().substr(0, new_len)); }else{ - Node remainderStr = NodeManager::currentNM()->mkConst(normal_forms[l][index].getConst().substr(len_short)); - Trace("strings-solve-debug-test") << "Break normal form of " << normal_forms[l][index] << " into " << normal_forms[k][index] << ", " << remainderStr << std::endl; - normal_forms[l].insert( normal_forms[l].begin()+index + 1, remainderStr ); + remainderStr = + nm->mkConst(nflv[index].getConst().substr(len_short)); } - normal_forms[l][index] = normal_forms[k][index]; + Trace("strings-solve-debug-test") + << "Break normal form of " << nflv[index] << " into " + << nfkv[index] << ", " << remainderStr << std::endl; + nfl.splitConstant(index, nfkv[index], remainderStr); index++; success = true; }else{ //conflict std::vector< Node > antec; - getExplanationVectorForPrefixEq( normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend, i, j, index, index, isRev, antec ); + NormalForm::getExplanationForPrefixEq( + nfi, nfj, index, index, antec); sendInference( antec, d_false, "N_Const", true ); return; } @@ -3116,17 +3148,19 @@ void TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal InferInfo info; info.d_index = index; //for debugging - info.d_i = i; - info.d_j = j; + info.d_i = nfi.d_base; + info.d_j = nfj.d_base; info.d_rev = isRev; bool info_valid = false; - Assert( index lexp; - Node length_term_i = getLength( normal_forms[i][index], lexp ); - Node length_term_j = getLength( normal_forms[j][index], lexp ); + Node length_term_i = getLength(nfiv[index], lexp); + Node length_term_j = getLength(nfjv[index], lexp); //split on equality between string lengths (note that splitting on equality between strings is worse since it is harder to process) - 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 ){ //AJR: remove the latter 2 conditions? + if (!areDisequal(length_term_i, length_term_j) + && !areEqual(length_term_i, length_term_j) + && !nfiv[index].isConst() && !nfjv[index].isConst()) + { // AJR: remove the latter 2 conditions? Trace("strings-solve-debug") << "Non-simple Case 1 : string lengths neither equal nor disequal" << std::endl; //try to make the lengths equal via splitting on demand Node length_eq = NodeManager::currentNM()->mkNode( kind::EQUAL, length_term_i, length_term_j ); @@ -3141,33 +3175,34 @@ void TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal int loop_in_i = -1; int loop_in_j = -1; ProcessLoopResult plr = ProcessLoopResult::SKIPPED; - if( detectLoop( normal_forms, i, j, index, loop_in_i, loop_in_j, rproc ) ){ + if (detectLoop(nfi, nfj, index, loop_in_i, loop_in_j, rproc)) + { if( !isRev ){ //FIXME - getExplanationVectorForPrefixEq( normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend, i, j, -1, -1, isRev, info.d_ant ); - //set info - plr = processLoop(normal_forms, - normal_form_src, - i, - j, - loop_in_i != -1 ? i : j, - loop_in_i != -1 ? j : i, - loop_in_i != -1 ? loop_in_i : loop_in_j, - index, - info); - if (plr == ProcessLoopResult::INFERENCE) - { - info_valid = true; - } + NormalForm::getExplanationForPrefixEq( + nfi, nfj, -1, -1, info.d_ant); + // set info + plr = processLoop(loop_in_i != -1 ? nfi : nfj, + loop_in_i != -1 ? nfj : nfi, + loop_in_i != -1 ? loop_in_i : loop_in_j, + index, + info); + if (plr == ProcessLoopResult::INFERENCE) + { + info_valid = true; + } } } if (plr == ProcessLoopResult::SKIPPED) { //AJR: length entailment here? - if( normal_forms[i][index].getKind() == kind::CONST_STRING || normal_forms[j][index].getKind() == kind::CONST_STRING ){ - unsigned const_k = normal_forms[i][index].getKind() == kind::CONST_STRING ? i : j; - unsigned nconst_k = normal_forms[i][index].getKind() == kind::CONST_STRING ? j : i; - Node other_str = normal_forms[nconst_k][index]; + if (nfiv[index].isConst() || nfjv[index].isConst()) + { + NormalForm& nfc = nfiv[index].isConst() ? nfi : nfj; + std::vector& nfcv = nfc.d_nf; + NormalForm& nfnc = nfiv[index].isConst() ? nfj : nfi; + std::vector& nfncv = nfnc.d_nf; + Node other_str = nfncv[index]; Assert( other_str.getKind()!=kind::CONST_STRING, "Other string is not constant." ); Assert( other_str.getKind()!=kind::STRING_CONCAT, "Other string is not CONCAT." ); if( !d_equalityEngine.areDisequal( other_str, d_emptyString, true ) ){ @@ -3180,12 +3215,15 @@ void TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal if( !isRev ){ //FIXME Node xnz = other_str.eqNode( d_emptyString ).negate(); unsigned index_nc_k = index+1; - //Node next_const_str = TheoryStringsRewriter::collectConstantStringAt( normal_forms[nconst_k], index_nc_k, false ); unsigned start_index_nc_k = index+1; - Node next_const_str = TheoryStringsRewriter::getNextConstantAt( normal_forms[nconst_k], start_index_nc_k, index_nc_k, false ); + Node next_const_str = + TheoryStringsRewriter::getNextConstantAt( + nfncv, start_index_nc_k, index_nc_k, false); if( !next_const_str.isNull() ) { unsigned index_c_k = index; - Node const_str = TheoryStringsRewriter::collectConstantStringAt( normal_forms[const_k], index_c_k, false ); + Node const_str = + TheoryStringsRewriter::collectConstantStringAt( + nfcv, index_c_k, false); Assert( !const_str.isNull() ); CVC4::String stra = const_str.getConst(); CVC4::String strb = next_const_str.getConst(); @@ -3208,9 +3246,9 @@ void TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal } if( p>1 ){ if( start_index_nc_k==index+1 ){ - info.d_ant.push_back( xnz ); - getExplanationVectorForPrefixEq( normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend, - const_k, nconst_k, index_c_k, index_nc_k, isRev, info.d_ant ); + info.d_ant.push_back(xnz); + NormalForm::getExplanationForPrefixEq( + nfc, nfnc, index_c_k, index_nc_k, info.d_ant); Node prea = p==stra.size() ? const_str : NodeManager::currentNM()->mkConst( isRev ? stra.suffix( p ) : stra.prefix( p ) ); Node sk = d_sk_cache.mkSkolemCached( other_str, @@ -3225,24 +3263,13 @@ void TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal info.d_id = INFER_SSPLIT_CST_PROP; info_valid = true; } - /* FIXME for isRev, speculative - else if( options::stringLenPropCsp() ){ - //propagate length constraint - std::vector< Node > cc; - for( unsigned i=index; imkNode( kind::STRING_LENGTH, mkConcat( cc ) ); - conc = NodeManager::currentNM()->mkNode( kind::GEQ, lt, NodeManager::currentNM()->mkConst( Rational(p) ) ); - sendInference( ant, conc, "S-Split(CSP-P)-lprop", true ); - } - */ } } if( !info_valid ){ info.d_ant.push_back( xnz ); - Node const_str = normal_forms[const_k][index]; - getExplanationVectorForPrefixEq( normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend, i, j, index, index, isRev, info.d_ant ); + Node const_str = nfcv[index]; + NormalForm::getExplanationForPrefixEq( + nfi, nfj, index, index, info.d_ant); CVC4::String stra = const_str.getConst(); if( options::stringBinaryCsp() && stra.size()>3 ){ //split string in half @@ -3285,7 +3312,7 @@ void TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal if( options::stringCheckEntailLen() ){ //check entailment for( unsigned e=0; e<2; e++ ){ - Node t = e==0 ? normal_forms[i][index] : normal_forms[j][index]; + Node t = e == 0 ? nfiv[index] : nfjv[index]; //do not infer constants are larger than variables if( t.getKind()!=kind::CONST_STRING ){ Node lt1 = e==0 ? length_term_i : length_term_j; @@ -3302,11 +3329,12 @@ void TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal } } } - - getExplanationVectorForPrefixEq( normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend, i, j, index, index, isRev, info.d_ant ); + + NormalForm::getExplanationForPrefixEq( + nfi, nfj, index, index, info.d_ant); //x!=e /\ y!=e for(unsigned xory=0; xory<2; xory++) { - Node x = xory==0 ? normal_forms[i][index] : normal_forms[j][index]; + Node x = xory == 0 ? nfiv[index] : nfjv[index]; Node xgtz = x.eqNode( d_emptyString ).negate(); if( d_equalityEngine.areDisequal( x, d_emptyString, true ) ) { info.d_ant.push_back( xgtz ); @@ -3315,15 +3343,19 @@ void TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal } } Node sk = d_sk_cache.mkSkolemCached( - normal_forms[i][index], - normal_forms[j][index], + nfiv[index], + nfjv[index], isRev ? SkolemCache::SK_ID_V_SPT_REV : SkolemCache::SK_ID_V_SPT, "v_spt"); // must add length requirement info.d_new_skolem[LENGTH_GEQ_ONE].push_back(sk); - Node eq1 = normal_forms[i][index].eqNode( isRev ? mkConcat(sk, normal_forms[j][index]) : mkConcat(normal_forms[j][index], sk) ); - Node eq2 = normal_forms[j][index].eqNode( isRev ? mkConcat(sk, normal_forms[i][index]) : mkConcat(normal_forms[i][index], sk) ); + Node eq1 = + nfiv[index].eqNode(isRev ? mkConcat(sk, nfjv[index]) + : mkConcat(nfjv[index], sk)); + Node eq2 = + nfjv[index].eqNode(isRev ? mkConcat(sk, nfiv[index]) + : mkConcat(nfiv[index], sk)); if( lentTestSuccess!=-1 ){ info.d_antn.push_back( lentTestExp ); @@ -3355,15 +3387,26 @@ void TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal }while( success ); } -bool TheoryStrings::detectLoop( std::vector< std::vector< Node > > &normal_forms, int i, int j, int index, int &loop_in_i, int &loop_in_j, unsigned rproc ){ +bool TheoryStrings::detectLoop(NormalForm& nfi, + NormalForm& nfj, + int index, + int& loop_in_i, + int& loop_in_j, + unsigned rproc) +{ int has_loop[2] = { -1, -1 }; if( options::stringLB() != 2 ) { for( unsigned r=0; r<2; r++ ) { - int n_index = (r==0 ? i : j); - int other_n_index = (r==0 ? j : i); - if( normal_forms[other_n_index][index].getKind() != kind::CONST_STRING ) { - for( unsigned lp = index+1; lp& nfv = nf.d_nf; + std::vector& nfov = nfo.d_nf; + if (!nfov[index].isConst()) + { + for (unsigned lp = index + 1; lp < nfv.size() - rproc; lp++) + { + if (nfv[lp] == nfov[index]) + { has_loop[r] = lp; break; } @@ -3382,16 +3425,11 @@ bool TheoryStrings::detectLoop( std::vector< std::vector< Node > > &normal_forms } //xs(zy)=t(yz)xr -TheoryStrings::ProcessLoopResult TheoryStrings::processLoop( - const std::vector >& normal_forms, - const std::vector& normal_form_src, - int i, - int j, - int loop_n_index, - int other_n_index, - int loop_index, - int index, - InferInfo& info) +TheoryStrings::ProcessLoopResult TheoryStrings::processLoop(NormalForm& nfi, + NormalForm& nfj, + int loop_index, + int index, + InferInfo& info) { if (options::stringProcessLoopMode() == ProcessLoopMode::ABORT) { @@ -3405,18 +3443,17 @@ TheoryStrings::ProcessLoopResult TheoryStrings::processLoop( NodeManager* nm = NodeManager::currentNM(); Node conc; - Trace("strings-loop") << "Detected possible loop for " - << normal_forms[loop_n_index][loop_index] << std::endl; - Trace("strings-loop") << " ... (X)= " << normal_forms[other_n_index][index] - << std::endl; + const std::vector& veci = nfi.d_nf; + const std::vector& vecoi = nfj.d_nf; + Trace("strings-loop") << "Detected possible loop for " << veci[loop_index] + << std::endl; + Trace("strings-loop") << " ... (X)= " << vecoi[index] << std::endl; Trace("strings-loop") << " ... T(Y.Z)= "; - const std::vector& veci = normal_forms[loop_n_index]; std::vector vec_t(veci.begin() + index, veci.begin() + loop_index); Node t_yz = mkConcat(vec_t); Trace("strings-loop") << " (" << t_yz << ")" << std::endl; Trace("strings-loop") << " ... S(Z.Y)= "; - const std::vector& vecoi = normal_forms[other_n_index]; std::vector vec_s(vecoi.begin() + index + 1, vecoi.end()); Node s_zy = mkConcat(vec_s); Trace("strings-loop") << s_zy << std::endl; @@ -3453,7 +3490,7 @@ TheoryStrings::ProcessLoopResult TheoryStrings::processLoop( Node split_eq; for (unsigned r = 0; r < 2; r++) { - Node t = r == 0 ? normal_forms[loop_n_index][loop_index] : t_yz; + Node t = r == 0 ? veci[loop_index] : t_yz; split_eq = t.eqNode(d_emptyString); Node split_eqr = Rewriter::rewrite(split_eq); // the equality could rewrite to false @@ -3486,16 +3523,14 @@ TheoryStrings::ProcessLoopResult TheoryStrings::processLoop( && s_zy.getConst().isRepeated()) { Node rep_c = nm->mkConst(s_zy.getConst().substr(0, 1)); - Trace("strings-loop") << "Special case (X)=" - << normal_forms[other_n_index][index] << " " + Trace("strings-loop") << "Special case (X)=" << vecoi[index] << " " << std::endl; Trace("strings-loop") << "... (C)=" << rep_c << " " << std::endl; // special case - str_in_re = - nm->mkNode(kind::STRING_IN_REGEXP, - normal_forms[other_n_index][index], - nm->mkNode(kind::REGEXP_STAR, - nm->mkNode(kind::STRING_TO_REGEXP, rep_c))); + str_in_re = nm->mkNode( + STRING_IN_REGEXP, + vecoi[index], + nm->mkNode(REGEXP_STAR, nm->mkNode(STRING_TO_REGEXP, rep_c))); conc = str_in_re; } else if (t_yz.isConst()) @@ -3528,12 +3563,12 @@ TheoryStrings::ProcessLoopResult TheoryStrings::processLoop( continue; } Node conc2 = nm->mkNode( - kind::STRING_IN_REGEXP, - normal_forms[other_n_index][index], - nm->mkNode(kind::REGEXP_CONCAT, - nm->mkNode(kind::STRING_TO_REGEXP, y), - nm->mkNode(kind::REGEXP_STAR, - nm->mkNode(kind::STRING_TO_REGEXP, restr)))); + STRING_IN_REGEXP, + vecoi[index], + nm->mkNode( + REGEXP_CONCAT, + nm->mkNode(STRING_TO_REGEXP, y), + nm->mkNode(REGEXP_STAR, nm->mkNode(STRING_TO_REGEXP, restr)))); cc = cc == d_true ? conc2 : nm->mkNode(kind::AND, cc, conc2); vconc.push_back(cc); } @@ -3566,8 +3601,7 @@ TheoryStrings::ProcessLoopResult TheoryStrings::processLoop( vec_r.insert(vec_r.begin(), sk_y); vec_r.insert(vec_r.begin(), sk_z); Node conc2 = s_zy.eqNode(mkConcat(vec_r)); - Node conc3 = - normal_forms[other_n_index][index].eqNode(mkConcat(sk_y, sk_w)); + Node conc3 = vecoi[index].eqNode(mkConcat(sk_y, sk_w)); Node restr = r == d_emptyString ? s_zy : mkConcat(sk_z, sk_y); str_in_re = nm->mkNode(kind::STRING_IN_REGEXP, @@ -3587,19 +3621,22 @@ TheoryStrings::ProcessLoopResult TheoryStrings::processLoop( // we will be done info.d_conc = conc; info.d_id = INFER_FLOOP; - info.d_nf_pair[0] = normal_form_src[i]; - info.d_nf_pair[1] = normal_form_src[j]; + info.d_nf_pair[0] = nfi.d_base; + info.d_nf_pair[1] = nfj.d_base; return ProcessLoopResult::INFERENCE; } //return true for lemma, false if we succeed void TheoryStrings::processDeq( Node ni, Node nj ) { //Assert( areDisequal( ni, nj ) ); - if( d_normal_forms[ni].size()>1 || d_normal_forms[nj].size()>1 ){ + NormalForm& nfni = getNormalForm(ni); + NormalForm& nfnj = getNormalForm(nj); + if (nfni.d_nf.size() > 1 || nfnj.d_nf.size() > 1) + { std::vector< Node > nfi; - nfi.insert( nfi.end(), d_normal_forms[ni].begin(), d_normal_forms[ni].end() ); + nfi.insert(nfi.end(), nfni.d_nf.begin(), nfni.d_nf.end()); std::vector< Node > nfj; - nfj.insert( nfj.end(), d_normal_forms[nj].begin(), d_normal_forms[nj].end() ); + nfj.insert(nfj.end(), nfnj.d_nf.begin(), nfnj.d_nf.end()); int revRet = processReverseDeq( nfi, nfj, ni, nj ); if( revRet!=0 ){ @@ -3607,9 +3644,9 @@ void TheoryStrings::processDeq( Node ni, Node nj ) { } nfi.clear(); - nfi.insert( nfi.end(), d_normal_forms[ni].begin(), d_normal_forms[ni].end() ); + nfi.insert(nfi.end(), nfni.d_nf.begin(), nfni.d_nf.end()); nfj.clear(); - nfj.insert( nfj.end(), d_normal_forms[nj].begin(), d_normal_forms[nj].end() ); + nfj.insert(nfj.end(), nfnj.d_nf.begin(), nfnj.d_nf.end()); unsigned index = 0; while( indexmkNode( kind::STRING_CONCAT, firstChar, skr ) ); std::vector< Node > antec; - antec.insert( antec.end(), d_normal_forms_exp[ni].begin(), d_normal_forms_exp[ni].end() ); - antec.insert( antec.end(), d_normal_forms_exp[nj].begin(), d_normal_forms_exp[nj].end() ); + antec.insert( + antec.end(), nfni.d_exp.begin(), nfni.d_exp.end()); + antec.insert( + antec.end(), nfnj.d_exp.begin(), nfnj.d_exp.end()); antec.push_back( nconst_k.eqNode( d_emptyString ).negate() ); sendInference( antec, NodeManager::currentNM()->mkNode( kind::OR, NodeManager::currentNM()->mkNode( kind::AND, eq1, sk.eqNode( firstChar ).negate() ), eq2 ), "D-DISL-CSplit" ); @@ -3679,8 +3718,8 @@ void TheoryStrings::processDeq( Node ni, Node nj ) { //must add lemma std::vector< Node > antec; std::vector< Node > antec_new_lits; - antec.insert( antec.end(), d_normal_forms_exp[ni].begin(), d_normal_forms_exp[ni].end() ); - antec.insert( antec.end(), d_normal_forms_exp[nj].begin(), d_normal_forms_exp[nj].end() ); + antec.insert(antec.end(), nfni.d_exp.begin(), nfni.d_exp.end()); + antec.insert(antec.end(), nfnj.d_exp.begin(), nfnj.d_exp.end()); //check disequal if( areDisequal( ni, nj ) ){ antec.push_back( ni.eqNode( nj ).negate() ); @@ -3767,16 +3806,18 @@ int TheoryStrings::processSimpleDeq( std::vector< Node >& nfi, std::vector< Node } } } + NormalForm& nfni = getNormalForm(ni); + NormalForm& nfnj = getNormalForm(nj); while( index=nfi.size() || index>=nfj.size() ){ Trace("strings-solve-debug") << "Disequality normalize empty" << std::endl; std::vector< Node > ant; //we have a conflict : because the lengths are equal, the remainder needs to be empty, which will lead to a conflict - Node lni = getLengthExp( ni, ant, d_normal_forms_base[ni] ); - Node lnj = getLengthExp( nj, ant, d_normal_forms_base[nj] ); + Node lni = getLengthExp(ni, ant, nfni.d_base); + Node lnj = getLengthExp(nj, ant, nfnj.d_base); ant.push_back( lni.eqNode( lnj ) ); - ant.insert( ant.end(), d_normal_forms_exp[ni].begin(), d_normal_forms_exp[ni].end() ); - ant.insert( ant.end(), d_normal_forms_exp[nj].begin(), d_normal_forms_exp[nj].end() ); + ant.insert(ant.end(), nfni.d_exp.begin(), nfni.d_exp.end()); + ant.insert(ant.end(), nfnj.d_exp.begin(), nfnj.d_exp.end()); std::vector< Node > cc; std::vector< Node >& nfk = index>=nfi.size() ? nfj : nfi; for( unsigned index_k=index; index_k& a ) { } } -void TheoryStrings::getConcatVec( Node n, std::vector< Node >& c ) { - if( n.getKind()==kind::STRING_CONCAT ) { - for( unsigned i=0; i > cols; @@ -4422,20 +4451,28 @@ void TheoryStrings::checkNormalFormsDeq() 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] << ", normal form : "; - printConcat( d_normal_forms[cols[i][0]], "strings-solve" ); - Trace("strings-solve") << "... #eql = " << cols[i].size() << std::endl; + if (Trace.isOn("strings-solve")) + { + Trace("strings-solve") << "- Verify disequalities are processed for " + << cols[i][0] << ", normal form : "; + printConcat(getNormalForm(cols[i][0]).d_nf, "strings-solve"); + Trace("strings-solve") + << "... #eql = " << cols[i].size() << std::endl; + } //must ensure that normal forms are disequal for( unsigned j=0; j1 ) { + NormalForm& nfi = getNormalForm(d_strings_eqc[i]); Trace("strings-process-debug") << "Process length constraints for " << d_strings_eqc[i] << std::endl; //check if there is a length term for this equivalence class EqcInfo* ei = getOrMakeEqcInfo( d_strings_eqc[i], false ); @@ -4460,19 +4497,22 @@ 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]] ); + Node nf = mkConcat(nfi.d_nf); 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 is " << nf << " from base " << nfi.d_base + << std::endl; Trace("strings-process-debug") << " normal form exp is: " << std::endl; - for( unsigned j=0; j 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 ) ); + ant.insert(ant.end(), nfi.d_exp.begin(), nfi.d_exp.end()); + ant.push_back(nfi.d_base.eqNode(lt)); Node lc = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, nf ); Node lcr = Rewriter::rewrite( lc ); Trace("strings-process-debug") << "Rewrote length " << lc << " to " << lcr << std::endl; @@ -4485,7 +4525,7 @@ void TheoryStrings::checkLengthsEqc() { }else{ Trace("strings-process-debug") << "No length term for eqc " << d_strings_eqc[i] << " " << d_eqc_to_len_term[d_strings_eqc[i]] << std::endl; if( !options::stringEagerLen() ){ - Node c = mkConcat( d_normal_forms[d_strings_eqc[i]] ); + Node c = mkConcat(nfi.d_nf); registerTerm( c, 3 ); /* if( !c.isConst() ){ diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index b3cb323ae..e9d82a7b2 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -24,6 +24,7 @@ #include "expr/attribute.h" #include "expr/node_trie.h" #include "theory/decision_manager.h" +#include "theory/strings/normal_form.h" #include "theory/strings/regexp_elim.h" #include "theory/strings/regexp_operation.h" #include "theory/strings/regexp_solver.h" @@ -307,11 +308,10 @@ class TheoryStrings : public Theory { /** inferences: maintained to ensure ref count for internally introduced nodes */ NodeList d_infer; NodeList d_infer_exp; - /** normal forms */ - std::map< Node, Node > d_normal_forms_base; - std::map< Node, std::vector< Node > > d_normal_forms; - std::map< Node, std::vector< Node > > d_normal_forms_exp; - std::map< Node, std::map< Node, std::map< bool, int > > > d_normal_forms_exp_depend; + /** map from terms to their normal forms */ + std::map d_normal_form; + /** get normal form */ + NormalForm& getNormalForm(Node n); //map of pairs of terms that have the same normal form NodeIntMap d_nf_pairs; std::map< Node, std::vector< Node > > d_nf_pairs_data; @@ -468,8 +468,14 @@ private: class InferInfo { public: - unsigned d_i; - unsigned d_j; + /** for debugging + * + * The base pair of strings d_i/d_j that led to the inference, and whether + * (d_rev) we were processing the normal forms of these strings in reverse + * direction. + */ + Node d_i; + Node d_j; bool d_rev; std::vector d_ant; std::vector d_antn; @@ -554,10 +560,77 @@ private: //--------------------------end for checkCycles //--------------------------for checkNormalFormsEq + /** normalize equivalence class + * + * This method attempts to build a "normal form" for the equivalence class + * of string term n (for more details on normal forms, see normal_form.h + * or see Liang et al CAV 2014). In particular, this method checks whether the + * current normal form for each term in this equivalence class is identical. + * If it is not, then we add an inference via sendInference and abort the + * call. + */ void normalizeEquivalenceClass( Node n ); - void 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 ); - bool detectLoop( std::vector< std::vector< Node > > &normal_forms, int i, int j, int index, int &loop_in_i, int &loop_in_j, unsigned rproc ); + /** + * For each term in the equivalence class of eqc, this adds data regarding its + * normal form to normal_forms. The map term_to_nf_index maps terms to the + * index in normal_forms where their normal form data is located. + */ + void getNormalForms(Node eqc, + std::vector& normal_forms, + std::map& term_to_nf_index); + /** process normalize equivalence class + * + * This is called when an equivalence class contains a set of terms that + * have normal forms given by the argument normal_forms. It either + * verifies that all normal forms in this vector are identical, or otherwise + * adds a conflict, lemma, or inference via the sendInference method. + * + * To prioritize one inference versus another, it builds a set of possible + * inferences, at most two for each pair of distinct normal forms, + * corresponding to processing the normal form pair in the (forward, reverse) + * directions. Once all possible inferences are recorded, it executes the + * one with highest priority based on the enumeration type Inference. + */ + void processNEqc(std::vector& normal_forms); + /** process simple normal equality + * + * This method is called when two equal terms have normal forms nfi and nfj. + * It adds (typically at most one) possible inference to the vector pinfer. + * This inference is in the form of an InferInfo object, which stores the + * necessary information regarding how to process the inference. + * + * index: The index in the normal form vectors (nfi.d_nf and nfj.d_nf) that + * we are currently checking. This method will increment this index until + * it finds an index where these vectors differ, or until it reaches the + * end of these vectors. + * isRev: Whether we are processing the normal forms in reverse direction. + * Notice in this case the normal form vectors have been reversed, hence, + * many operations are identical to the forward case, e.g. index is + * incremented not decremented, while others require special care, e.g. + * constant strings "ABC" in the normal form vectors are not reversed to + * "CBA" and hence all operations should assume a flipped semantics for + * constants when isRev is true, + * rproc: the number of string components on the suffix of the normal form of + * nfi and nfj that were already processed. This is used when using + * fowards/backwards traversals of normal forms to ensure that duplicate + * inferences are not processed. + * pinfer: the set of possible inferences we add to. + */ + void processSimpleNEq(NormalForm& nfi, + NormalForm& nfj, + unsigned& index, + bool isRev, + unsigned rproc, + std::vector& pinfer); + //--------------------------end for checkNormalFormsEq + + //--------------------------for checkNormalFormsEq with loops + bool detectLoop(NormalForm& nfi, + NormalForm& nfj, + int index, + int& loop_in_i, + int& loop_in_j, + unsigned rproc); /** * Result of processLoop() below. @@ -572,36 +645,17 @@ private: SKIPPED, }; - ProcessLoopResult processLoop( - const std::vector >& normal_forms, - const std::vector& normal_form_src, - int i, - int j, - int loop_n_index, - int other_n_index, - int loop_index, - int index, - InferInfo& info); - - void processNEqc( 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 ); - void processReverseNEq( 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, - unsigned i, unsigned j, unsigned& index, unsigned rproc, std::vector< InferInfo >& pinfer ); - void processSimpleNEq( 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, - unsigned i, unsigned j, unsigned& index, bool isRev, unsigned rproc, std::vector< InferInfo >& pinfer ); - //--------------------------end for checkNormalFormsEq + ProcessLoopResult processLoop(NormalForm& nfi, + NormalForm& nfj, + int loop_index, + int index, + InferInfo& info); + //--------------------------end for checkNormalFormsEq with loops //--------------------------for checkNormalFormsDeq void processDeq( Node n1, Node n2 ); int processReverseDeq( std::vector< Node >& nfi, std::vector< Node >& nfj, Node ni, Node nj ); int processSimpleDeq( std::vector< Node >& nfi, std::vector< Node >& nfj, Node ni, Node nj, unsigned& index, bool isRev ); - void getExplanationVectorForPrefix( std::vector< std::vector< Node > > &normal_forms_exp, std::vector< std::map< Node, std::map< bool, int > > >& normal_forms_exp_depend, - unsigned i, int index, bool isRev, std::vector< Node >& curr_exp ); - void getExplanationVectorForPrefixEq( 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, - unsigned i, unsigned j, int index_i, int index_j, bool isRev, std::vector< Node >& curr_exp ); //--------------------------end for checkNormalFormsDeq //--------------------------------for checkMemberships @@ -787,8 +841,6 @@ private: protected: /** mkAnd **/ Node mkAnd(std::vector& a); - /** get concat vector */ - void getConcatVec(Node n, std::vector& c); /** get equivalence classes *