From 33cabd5c723d33a5aa4c85856af83b141cbbbd87 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 29 Jan 2020 20:08:09 -0600 Subject: [PATCH] Modularize more steps in the strings strategy (#3676) --- src/theory/strings/theory_strings.cpp | 145 +++++++++++++++----------- src/theory/strings/theory_strings.h | 17 +++ 2 files changed, 99 insertions(+), 63 deletions(-) diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 01f9fc99a..7b1b34917 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -2473,26 +2473,25 @@ Node TheoryStrings::checkCycles( Node eqc, std::vector< Node >& curr, std::vecto return Node::null(); } -void TheoryStrings::checkNormalFormsEq() +void TheoryStrings::checkRegisterTermsPreNormalForm() { - if( !options::stringEagerLen() ){ - for( unsigned i=0; id_lengthTerm : Node::null(); - if( !lt.isNull() ) { - Node llt = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, lt ); - //now, check if length normalization has occurred - if (ei->d_normalizedLength.get().isNull()) + for (unsigned i = 0; i < d_strings_eqc.size(); i++) + { + 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 = d_state.getOrMakeEqcInfo(d_strings_eqc[i], false); + Node lt = ei ? ei->d_lengthTerm : Node::null(); + if (lt.isNull()) + { + Trace("strings-process-debug") + << "No length term for eqc " << d_strings_eqc[i] << " " + << d_eqc_to_len_term[d_strings_eqc[i]] << std::endl; + continue; + } + Node llt = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, lt); + // now, check if length normalization has occurred + if (ei->d_normalizedLength.get().isNull()) + { + Node nf = utils::mkNConcat(nfi.d_nf); + if (Trace.isOn("strings-process-debug")) + { + 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 (const Node& exp : nfi.d_exp) { - Node nf = utils::mkNConcat(nfi.d_nf); - if( Trace.isOn("strings-process-debug") ){ - 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 (const Node& exp : nfi.d_exp) - { - Trace("strings-process-debug") << " " << exp << std::endl; - } - } - - //if not, add the lemma - std::vector< Node > ant; - 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; - if (!d_state.areEqual(llt, lcr)) - { - Node eq = llt.eqNode(lcr); - ei->d_normalizedLength.set(eq); - d_im.sendInference(ant, eq, "LEN-NORM", true); - } - } - }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 = utils::mkNConcat(nfi.d_nf); - registerTerm( c, 3 ); + Trace("strings-process-debug") << " " << exp << std::endl; } } - //} else { - // Trace("strings-process-debug") << "Do not process length constraints for " << nodes[i] << " " << d_normal_forms[nodes[i]].size() << std::endl; - //} + + // if not, add the lemma + std::vector ant; + 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; + if (!d_state.areEqual(llt, lcr)) + { + Node eq = llt.eqNode(lcr); + ei->d_normalizedLength.set(eq); + d_im.sendInference(ant, eq, "LEN-NORM", true); + } + } + } +} +void TheoryStrings::checkRegisterTermsNormalForms() +{ + for (const Node& eqc : d_strings_eqc) + { + NormalForm& nfi = getNormalForm(eqc); + // check if there is a length term for this equivalence class + EqcInfo* ei = d_state.getOrMakeEqcInfo(eqc, false); + Node lt = ei ? ei->d_lengthTerm : Node::null(); + if (lt.isNull()) + { + Node c = utils::mkNConcat(nfi.d_nf); + registerTerm(c, 3); } } } @@ -4477,10 +4489,12 @@ void TheoryStrings::runInferStep(InferStep s, int effort) case CHECK_EXTF_EVAL: checkExtfEval(effort); break; case CHECK_CYCLES: checkCycles(); break; case CHECK_FLAT_FORMS: checkFlatForms(); break; + case CHECK_REGISTER_TERMS_PRE_NF: checkRegisterTermsPreNormalForm(); break; case CHECK_NORMAL_FORMS_EQ: checkNormalFormsEq(); break; case CHECK_NORMAL_FORMS_DEQ: checkNormalFormsDeq(); break; case CHECK_CODES: checkCodes(); break; case CHECK_LENGTH_EQC: checkLengthsEqc(); break; + case CHECK_REGISTER_TERMS_NF: checkRegisterTermsNormalForms(); break; case CHECK_EXTF_REDUCTION: checkExtfReductions(effort); break; case CHECK_MEMBERSHIP: checkMemberships(); break; case CHECK_CARDINALITY: checkCardinality(); break; @@ -4544,15 +4558,20 @@ void TheoryStrings::initializeStrategy() // do only the above inferences at standard effort, if applicable step_end[EFFORT_STANDARD] = d_infer_steps.size() - 1; } + if (!options::stringEagerLen()) + { + addStrategyStep(CHECK_REGISTER_TERMS_PRE_NF); + } addStrategyStep(CHECK_NORMAL_FORMS_EQ); addStrategyStep(CHECK_EXTF_EVAL, 1); - if (!options::stringEagerLen()) + if (!options::stringEagerLen() && options::stringLenNorm()) { - addStrategyStep(CHECK_LENGTH_EQC); + addStrategyStep(CHECK_LENGTH_EQC, 0, false); + addStrategyStep(CHECK_REGISTER_TERMS_NF); } addStrategyStep(CHECK_NORMAL_FORMS_DEQ); addStrategyStep(CHECK_CODES); - if (options::stringEagerLen()) + if (options::stringEagerLen() && options::stringLenNorm()) { addStrategyStep(CHECK_LENGTH_EQC); } diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index b9e994fb5..990461027 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -68,6 +68,8 @@ enum InferStep CHECK_CYCLES, // check flat forms CHECK_FLAT_FORMS, + // check register terms pre-normal forms + CHECK_REGISTER_TERMS_PRE_NF, // check normal forms equalities CHECK_NORMAL_FORMS_EQ, // check normal forms disequalities @@ -76,6 +78,8 @@ enum InferStep CHECK_CODES, // check lengths for equivalence classes CHECK_LENGTH_EQC, + // check register terms for normal forms + CHECK_REGISTER_TERMS_NF, // check extended function reductions CHECK_EXTF_REDUCTION, // check regular expression memberships @@ -764,6 +768,12 @@ private: * Must call checkCycles before this function in a strategy. */ void checkFlatForms(); + /** check register terms pre-normal forms + * + * This calls registerTerm(n,2) on all non-congruent strings in the + * equality engine of this class. + */ + void checkRegisterTermsPreNormalForm(); /** check normal forms equalities * * This applies an inference schema based on "normal forms". The normal form @@ -841,6 +851,13 @@ private: * shown to be helpful. */ void checkLengthsEqc(); + /** check register terms for normal forms + * + * This calls registerTerm(str.++(t1, ..., tn ), 3) on the normal forms + * (t1, ..., tn) of all string equivalence classes { s1, ..., sm } such that + * there does not exist a term of the form str.len(si) in the current context. + */ + void checkRegisterTermsNormalForms(); /** check extended function reductions * * This adds "reduction" lemmas for each active extended function in this SAT -- 2.30.2