diff options
| -rw-r--r-- | src/theory/strings/extf_solver.cpp | 31 | ||||
| -rw-r--r-- | src/theory/strings/extf_solver.h | 6 | ||||
| -rw-r--r-- | src/theory/strings/regexp_solver.cpp | 16 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 13 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/strings/issue6203-2-re-ccache.smt2 | 8 |
6 files changed, 52 insertions, 23 deletions
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<Node> 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<Node> 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<Node, std::vector<Node> >& mems) bool addedLemma = false; bool changed = false; std::vector<Node> processed; - std::vector<Node> cprocessed; Trace("regexp-process") << "Checking Memberships ... " << std::endl; for (const std::pair<const Node, std::vector<Node> >& mr : mems) @@ -287,14 +286,7 @@ void RegExpSolver::check(const std::map<Node, std::vector<Node> >& 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<Node, std::vector<Node> >& 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<Node>& 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<TypeNode, std::unordered_set<Node, NodeHashFunction> > 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) |