From 8e15d120579b791af0999d07d847620037366978 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 29 Jan 2020 19:42:50 -0600 Subject: [PATCH] Minor updates to string utilities (#3675) --- src/theory/strings/inference_manager.cpp | 12 ++++++++++++ src/theory/strings/inference_manager.h | 16 +++++++++++++++- src/theory/strings/theory_strings.cpp | 18 +++++++----------- src/theory/strings/theory_strings.h | 4 ---- src/theory/strings/theory_strings_utils.cpp | 19 +++++++++++++++++++ src/theory/strings/theory_strings_utils.h | 5 +++++ 6 files changed, 58 insertions(+), 16 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& 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 1bc104096..01f9fc99a 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -2806,7 +2806,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)); @@ -4163,7 +4163,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; } @@ -4184,9 +4185,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]); @@ -4359,13 +4362,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; i0 ) Trace(c) << " ++ "; - Trace(c) << n[i]; - } -} - //// Finite Model Finding diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 8e2af8434..b9e994fb5 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -615,10 +615,6 @@ private: */ void registerTerm(Node n, int effort); - protected: - - void printConcat(std::vector& n, const char* c); - // Symbolic Regular Expression private: /** regular expression solver module */ 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& result) } } +void printConcat(std::ostream& out, std::vector& n) +{ + for (unsigned i = 0, nsize = n.size(); i < nsize; i++) + { + if (i > 0) + { + out << " ++ "; + } + out << n[i]; + } +} + +void printConcatTrace(std::vector& 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& result); +/** Print the vector n as a concatentation term on output stream out */ +void printConcat(std::ostream& out, std::vector& n); +/** Print the vector n as a concatentation term on trace given by c */ +void printConcatTrace(std::vector& n, const char* c); + } // namespace utils } // namespace strings } // namespace theory -- 2.30.2