diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-01-29 20:08:27 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-01-29 20:08:27 -0600 |
commit | 970e64b0cef4402b5b30bae32c4d4f647f187201 (patch) | |
tree | 2ded393febd12e43d7548c0872fb99ffa52989ee | |
parent | c74246374ea672242c5e16bd8db0f25e1222cab4 (diff) | |
parent | 33cabd5c723d33a5aa4c85856af83b141cbbbd87 (diff) |
Merge branch 'master' into oldVarHeuristicPRoldVarHeuristicPR
-rw-r--r-- | src/theory/strings/inference_manager.cpp | 12 | ||||
-rw-r--r-- | src/theory/strings/inference_manager.h | 16 | ||||
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 163 | ||||
-rw-r--r-- | src/theory/strings/theory_strings.h | 21 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_utils.cpp | 19 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_utils.h | 5 |
6 files changed, 157 insertions, 79 deletions
diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp index c9a2bcd70..2b5338a6a 100644 --- a/src/theory/strings/inference_manager.cpp +++ b/src/theory/strings/inference_manager.cpp @@ -16,6 +16,7 @@ #include "expr/kind.h" #include "options/strings_options.h" +#include "theory/ext_theory.h" #include "theory/rewriter.h" #include "theory/strings/theory_strings.h" #include "theory/strings/theory_strings_rewriter.h" @@ -625,6 +626,17 @@ void InferenceManager::explain(TNode literal, } } } +void InferenceManager::setIncomplete() { d_out.setIncomplete(); } + +void InferenceManager::markCongruent(Node a, Node b) +{ + Assert(a.getKind() == b.getKind()); + ExtTheory* eth = d_parent.getExtTheory(); + if (eth->hasFunctionKind(a.getKind())) + { + eth->markCongruent(a, b); + } +} } // namespace strings } // namespace theory diff --git a/src/theory/strings/inference_manager.h b/src/theory/strings/inference_manager.h index e052889f6..819e4b98f 100644 --- a/src/theory/strings/inference_manager.h +++ b/src/theory/strings/inference_manager.h @@ -61,7 +61,8 @@ class TheoryStrings; * to doPendingLemmas. * * It also manages other kinds of interaction with the output channel of the - * theory of strings, e.g. sendPhaseRequirement. + * theory of strings, e.g. sendPhaseRequirement, setIncomplete, and + * with the extended theory object e.g. markCongruent. */ class InferenceManager { @@ -249,6 +250,19 @@ class InferenceManager * the node corresponding to their conjunction. */ void explain(TNode literal, std::vector<TNode>& assumptions) const; + /** + * Set that we are incomplete for the current set of assertions (in other + * words, we must answer "unknown" instead of "sat"); this calls the output + * channel's setIncomplete method. + */ + void setIncomplete(); + /** + * Mark that terms a and b are congruent in the current context. + * This makes a call to markCongruent in the extended theory object of + * the parent theory if the kind of a (and b) is owned by the extended + * theory. + */ + void markCongruent(Node a, Node b); private: /** diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 6000489cf..755e6b4df 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -2486,26 +2486,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; i<d_strings_eqc.size(); i++ ) { - Node eqc = d_strings_eqc[i]; - eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); - while( !eqc_i.isFinished() ) { - Node n = (*eqc_i); - if( d_congruent.find( n )==d_congruent.end() ){ - registerTerm( n, 2 ); - } - ++eqc_i; + for (const Node& eqc : d_strings_eqc) + { + eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, &d_equalityEngine); + while (!eqc_i.isFinished()) + { + Node n = (*eqc_i); + if (d_congruent.find(n) == d_congruent.end()) + { + registerTerm(n, 2); } + ++eqc_i; } } +} - if (d_im.hasProcessed()) - { - return; - } +void TheoryStrings::checkNormalFormsEq() +{ // calculate normal forms for each equivalence class, possibly adding // splitting lemmas d_normal_form.clear(); @@ -2819,7 +2818,7 @@ void TheoryStrings::getNormalForms(Node eqc, if (Trace.isOn("strings-error")) { Trace("strings-error") << "Cycle for normal form "; - printConcat(currv, "strings-error"); + utils::printConcatTrace(currv, "strings-error"); Trace("strings-error") << "..." << currv[i] << std::endl; } Assert(!d_state.areEqual(currv[i], n)); @@ -4176,7 +4175,8 @@ void TheoryStrings::checkNormalFormsDeq() { Trace("strings-solve") << "- Verify disequalities are processed for " << cols[i][0] << ", normal form : "; - printConcat(getNormalForm(cols[i][0]).d_nf, "strings-solve"); + utils::printConcatTrace(getNormalForm(cols[i][0]).d_nf, + "strings-solve"); Trace("strings-solve") << "... #eql = " << cols[i].size() << std::endl; } @@ -4197,9 +4197,11 @@ void TheoryStrings::checkNormalFormsDeq() if (Trace.isOn("strings-solve")) { Trace("strings-solve") << "- Compare " << cols[i][j] << " "; - printConcat(getNormalForm(cols[i][j]).d_nf, "strings-solve"); + utils::printConcatTrace(getNormalForm(cols[i][j]).d_nf, + "strings-solve"); Trace("strings-solve") << " against " << cols[i][k] << " "; - printConcat(getNormalForm(cols[i][k]).d_nf, "strings-solve"); + utils::printConcatTrace(getNormalForm(cols[i][k]).d_nf, + "strings-solve"); Trace("strings-solve") << "..." << std::endl; } processDeq(cols[i][j], cols[i][k]); @@ -4217,54 +4219,67 @@ void TheoryStrings::checkNormalFormsDeq() } void TheoryStrings::checkLengthsEqc() { - if( options::stringLenNorm() ){ - 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() ) { - 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<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); + } + } + } +} +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); } } } @@ -4372,13 +4387,6 @@ void TheoryStrings::checkCardinality() { Trace("strings-card") << "...end check cardinality" << std::endl; } -void TheoryStrings::printConcat( std::vector< Node >& n, const char * c ) { - for( unsigned i=0; i<n.size(); i++ ){ - if( i>0 ) Trace(c) << " ++ "; - Trace(c) << n[i]; - } -} - //// Finite Model Finding @@ -4494,10 +4502,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; @@ -4561,15 +4571,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 8e2af8434..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 @@ -615,10 +619,6 @@ private: */ void registerTerm(Node n, int effort); - protected: - - void printConcat(std::vector<Node>& n, const char* c); - // Symbolic Regular Expression private: /** regular expression solver module */ @@ -768,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 @@ -845,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 diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp index 03c2419c4..a564c82e1 100644 --- a/src/theory/strings/theory_strings_utils.cpp +++ b/src/theory/strings/theory_strings_utils.cpp @@ -225,6 +225,25 @@ void getRegexpComponents(Node r, std::vector<Node>& result) } } +void printConcat(std::ostream& out, std::vector<Node>& n) +{ + for (unsigned i = 0, nsize = n.size(); i < nsize; i++) + { + if (i > 0) + { + out << " ++ "; + } + out << n[i]; + } +} + +void printConcatTrace(std::vector<Node>& n, const char* c) +{ + std::stringstream ss; + printConcat(ss, n); + Trace(c) << ss.str(); +} + } // namespace utils } // namespace strings } // namespace theory diff --git a/src/theory/strings/theory_strings_utils.h b/src/theory/strings/theory_strings_utils.h index 2c84bd516..ccdac8edf 100644 --- a/src/theory/strings/theory_strings_utils.h +++ b/src/theory/strings/theory_strings_utils.h @@ -131,6 +131,11 @@ bool isSimpleRegExp(Node r); */ void getRegexpComponents(Node r, std::vector<Node>& result); +/** Print the vector n as a concatentation term on output stream out */ +void printConcat(std::ostream& out, std::vector<Node>& n); +/** Print the vector n as a concatentation term on trace given by c */ +void printConcatTrace(std::vector<Node>& n, const char* c); + } // namespace utils } // namespace strings } // namespace theory |