From ef2f19f8ba2a72d43586d1f4f364822dbe389aec Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 1 Apr 2021 17:02:33 -0500 Subject: [PATCH] Simplify caching of regular expression unfolding (#6262) This ensures that we always cache regular expressions in a user-dependent manner. Previously, we were erroneously caching in a SAT-dependent way for very rare cases when non-constant regular expressions were used. Since we never dependent on current assertions for the unfolding, there is no need to cache in the SAT context. This fixes the second benchmark from #6203. This PR also improves our traces for checking models in strings. --- src/theory/strings/extf_solver.cpp | 31 +++++++++++++++++-- src/theory/strings/extf_solver.h | 6 ++++ src/theory/strings/regexp_solver.cpp | 16 +--------- src/theory/strings/theory_strings.cpp | 13 +++++--- test/regress/CMakeLists.txt | 1 + .../strings/issue6203-2-re-ccache.smt2 | 8 +++++ 6 files changed, 52 insertions(+), 23 deletions(-) create mode 100644 test/regress/regress1/strings/issue6203-2-re-ccache.smt2 diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp index 39bcb8f53..fd50e78ee 100644 --- a/src/theory/strings/extf_solver.cpp +++ b/src/theory/strings/extf_solver.cpp @@ -85,7 +85,7 @@ bool ExtfSolver::doReduction(int effort, Node n) if (d_reduced.find(n)!=d_reduced.end()) { // already sent a reduction lemma - Trace("strings-extf-debug") << "...skip due to reduced" << std::endl; + Trace("strings-extf-debug") << "...skip due to reduced" << std::endl; return false; } // determine the effort level to process the extf at @@ -157,8 +157,7 @@ bool ExtfSolver::doReduction(int effort, Node n) } if (effort != r_effort) { - - Trace("strings-extf-debug") << "...skip due to effort" << std::endl; + Trace("strings-extf-debug") << "...skip due to effort" << std::endl; // not the right effort level to reduce return false; } @@ -722,6 +721,32 @@ bool StringsExtfCallback::getCurrentSubstitution( return true; } +std::string ExtfSolver::debugPrintModel() +{ + std::stringstream ss; + std::vector extf; + d_extt.getTerms(extf); + // each extended function should have at least one annotation below + for (const Node& n : extf) + { + ss << "- " << n; + if (!d_extt.isActive(n)) + { + ss << " :extt-inactive"; + } + if (!d_extfInfoTmp[n].d_modelActive) + { + ss << " :model-inactive"; + } + if (d_reduced.find(n) != d_reduced.end()) + { + ss << " :reduced"; + } + ss << std::endl; + } + return ss.str(); +} + } // namespace strings } // namespace theory } // namespace cvc5 diff --git a/src/theory/strings/extf_solver.h b/src/theory/strings/extf_solver.h index 3cfe2309c..bbc32e7a2 100644 --- a/src/theory/strings/extf_solver.h +++ b/src/theory/strings/extf_solver.h @@ -153,6 +153,12 @@ class ExtfSolver */ std::vector getActive(Kind k) const; //---------------------------------- end information about ExtTheory + /** + * Print the relevant information regarding why we have a model, return as a + * string. + */ + std::string debugPrintModel(); + private: /** do reduction * diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp index 2d4404c10..7737a90f7 100644 --- a/src/theory/strings/regexp_solver.cpp +++ b/src/theory/strings/regexp_solver.cpp @@ -96,7 +96,6 @@ void RegExpSolver::check(const std::map >& mems) bool addedLemma = false; bool changed = false; std::vector processed; - std::vector cprocessed; Trace("regexp-process") << "Checking Memberships ... " << std::endl; for (const std::pair >& mr : mems) @@ -287,14 +286,7 @@ void RegExpSolver::check(const std::map >& mems) polarity ? InferenceId::STRINGS_RE_UNFOLD_POS : InferenceId::STRINGS_RE_UNFOLD_NEG; d_im.sendInference(iexp, noExplain, conc, inf); addedLemma = true; - if (changed) - { - cprocessed.push_back(assertion); - } - else - { - processed.push_back(assertion); - } + processed.push_back(assertion); if (e == 0) { // Remember that we have unfolded a membership for x @@ -326,12 +318,6 @@ void RegExpSolver::check(const std::map >& mems) << "...add " << processed[i] << " to u-cache." << std::endl; d_regexp_ucached.insert(processed[i]); } - for (unsigned i = 0; i < cprocessed.size(); i++) - { - Trace("strings-regexp") - << "...add " << cprocessed[i] << " to c-cache." << std::endl; - d_regexp_ccached.insert(cprocessed[i]); - } } } } diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 5bd92267e..f2f584da7 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -203,13 +203,16 @@ void TheoryStrings::presolve() { bool TheoryStrings::collectModelValues(TheoryModel* m, const std::set& termSet) { - if (Trace.isOn("strings-model")) + if (Trace.isOn("strings-debug-model")) { - Trace("strings-model") << "TheoryStrings : Collect model values" - << std::endl; - Trace("strings-model") << "Equivalence classes are:" << std::endl; - Trace("strings-model") << debugPrintStringsEqc() << std::endl; + Trace("strings-debug-model") + << "TheoryStrings::collectModelValues" << std::endl; + Trace("strings-debug-model") << "Equivalence classes are:" << std::endl; + Trace("strings-debug-model") << debugPrintStringsEqc() << std::endl; + Trace("strings-debug-model") << "Extended functions are:" << std::endl; + Trace("strings-debug-model") << d_esolver.debugPrintModel() << std::endl; } + Trace("strings-model") << "TheoryStrings::collectModelValues" << std::endl; std::map > repSet; // Generate model // get the relevant string equivalence classes diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 232a7f7ab..64c584f7a 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2040,6 +2040,7 @@ set(regress_1_tests regress1/strings/issue6132-non-unique-skolem.smt2 regress1/strings/issue6142-repl-inv-rew.smt2 regress1/strings/issue6191-replace-all.smt2 + regress1/strings/issue6203-2-re-ccache.smt2 regress1/strings/kaluza-fl.smt2 regress1/strings/loop002.smt2 regress1/strings/loop003.smt2 diff --git a/test/regress/regress1/strings/issue6203-2-re-ccache.smt2 b/test/regress/regress1/strings/issue6203-2-re-ccache.smt2 new file mode 100644 index 000000000..2deffdadd --- /dev/null +++ b/test/regress/regress1/strings/issue6203-2-re-ccache.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --strings-exp +; EXPECT: sat +(set-logic ALL) +(declare-fun a () String) +(assert + (xor (str.in_re a (re.++ (re.* re.allchar) (str.to_re "A") re.allchar (re.* re.allchar))) + (str.in_re a (re.++ (re.* (str.to_re a)) (str.to_re "A") re.allchar)))) +(check-sat) -- 2.30.2