From 02dd48563db0c5effd608eda70d4c262309322a6 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sat, 20 Mar 2021 06:42:51 -0500 Subject: [PATCH] Improved tracing for equivalence classes of EE (#6169) Helps debugging model issues. --- src/theory/model_manager.cpp | 10 +++ src/theory/sep/theory_sep.cpp | 20 +----- src/theory/strings/theory_strings.cpp | 92 ++++++++++++++++----------- src/theory/strings/theory_strings.h | 2 + src/theory/theory_model.cpp | 33 ++++++++-- src/theory/theory_model.h | 6 +- src/theory/uf/equality_engine.cpp | 23 +++++++ src/theory/uf/equality_engine.h | 3 + 8 files changed, 124 insertions(+), 65 deletions(-) diff --git a/src/theory/model_manager.cpp b/src/theory/model_manager.cpp index b9057604e..d77a88d67 100644 --- a/src/theory/model_manager.cpp +++ b/src/theory/model_manager.cpp @@ -99,6 +99,16 @@ bool ModelManager::buildModel() // now, finish building the model d_modelBuiltSuccess = finishBuildModel(); + + if (Trace.isOn("model-builder")) + { + Trace("model-builder") << "Final model:" << std::endl; + Trace("model-builder") << d_model->debugPrintModelEqc() << std::endl; + } + + Trace("model-builder") << "ModelManager: model built success is " + << d_modelBuiltSuccess << std::endl; + return d_modelBuiltSuccess; } diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index 7fe86d86d..47eac5359 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -656,25 +656,7 @@ void TheorySep::postCheck(Effort level) } if (Trace.isOn("sep-eqc")) { - eq::EqClassesIterator eqcs2_i = eq::EqClassesIterator(d_equalityEngine); - Trace("sep-eqc") << "EQC:" << std::endl; - while (!eqcs2_i.isFinished()) - { - Node eqc = (*eqcs2_i); - eq::EqClassIterator eqc2_i = eq::EqClassIterator(eqc, d_equalityEngine); - Trace("sep-eqc") << "Eqc( " << eqc << " ) : { "; - while (!eqc2_i.isFinished()) - { - if ((*eqc2_i) != eqc) - { - Trace("sep-eqc") << (*eqc2_i) << " "; - } - ++eqc2_i; - } - Trace("sep-eqc") << " } " << std::endl; - ++eqcs2_i; - } - Trace("sep-eqc") << std::endl; + Trace("sep-eqc") << d_equalityEngine->debugPrintEqc(); } bool addedLemma = false; diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 2a5d043f5..b92cdaf5b 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -203,8 +203,13 @@ void TheoryStrings::presolve() { bool TheoryStrings::collectModelValues(TheoryModel* m, const std::set& termSet) { - Trace("strings-model") << "TheoryStrings : Collect model values" << std::endl; - + if (Trace.isOn("strings-model")) + { + Trace("strings-model") << "TheoryStrings : Collect model values" + << std::endl; + Trace("strings-model") << "Equivalence classes are:" << std::endl; + Trace("strings-model") << debugPrintStringsEqc() << std::endl; + } std::map > repSet; // Generate model // get the relevant string equivalence classes @@ -629,42 +634,7 @@ void TheoryStrings::postCheck(Effort e) << "Theory of strings " << e << " effort check " << std::endl; if (Trace.isOn("strings-eqc")) { - for (unsigned t = 0; t < 2; t++) - { - eq::EqClassesIterator eqcs2_i = eq::EqClassesIterator(d_equalityEngine); - Trace("strings-eqc") << (t==0 ? "STRINGS:" : "OTHER:") << std::endl; - while( !eqcs2_i.isFinished() ){ - Node eqc = (*eqcs2_i); - bool print = (t == 0 && eqc.getType().isStringLike()) - || (t == 1 && !eqc.getType().isStringLike()); - if (print) { - eq::EqClassIterator eqc2_i = - eq::EqClassIterator(eqc, d_equalityEngine); - Trace("strings-eqc") << "Eqc( " << eqc << " ) : { "; - while( !eqc2_i.isFinished() ) { - if( (*eqc2_i)!=eqc && (*eqc2_i).getKind()!=kind::EQUAL ){ - Trace("strings-eqc") << (*eqc2_i) << " "; - } - ++eqc2_i; - } - Trace("strings-eqc") << " } " << std::endl; - EqcInfo* ei = d_state.getOrMakeEqcInfo(eqc, false); - if( ei ){ - Trace("strings-eqc-debug") - << "* Length term : " << ei->d_lengthTerm.get() << std::endl; - Trace("strings-eqc-debug") - << "* Cardinality lemma k : " << ei->d_cardinalityLemK.get() - << std::endl; - Trace("strings-eqc-debug") - << "* Normalization length lemma : " - << ei->d_normalizedLength.get() << std::endl; - } - } - ++eqcs2_i; - } - Trace("strings-eqc") << std::endl; - } - Trace("strings-eqc") << std::endl; + Trace("strings-eqc") << debugPrintStringsEqc() << std::endl; } ++(d_statistics.d_checkRuns); bool sentLemma = false; @@ -1074,6 +1044,52 @@ void TheoryStrings::runStrategy(Theory::Effort e) Trace("strings-process") << "----finished round---" << std::endl; } +std::string TheoryStrings::debugPrintStringsEqc() +{ + std::stringstream ss; + for (unsigned t = 0; t < 2; t++) + { + eq::EqClassesIterator eqcs2_i = eq::EqClassesIterator(d_equalityEngine); + ss << (t == 0 ? "STRINGS:" : "OTHER:") << std::endl; + while (!eqcs2_i.isFinished()) + { + Node eqc = (*eqcs2_i); + bool print = (t == 0 && eqc.getType().isStringLike()) + || (t == 1 && !eqc.getType().isStringLike()); + if (print) + { + eq::EqClassIterator eqc2_i = eq::EqClassIterator(eqc, d_equalityEngine); + ss << "Eqc( " << eqc << " ) : { "; + while (!eqc2_i.isFinished()) + { + if ((*eqc2_i) != eqc && (*eqc2_i).getKind() != kind::EQUAL) + { + ss << (*eqc2_i) << " "; + } + ++eqc2_i; + } + ss << " } " << std::endl; + EqcInfo* ei = d_state.getOrMakeEqcInfo(eqc, false); + if (ei) + { + Trace("strings-eqc-debug") + << "* Length term : " << ei->d_lengthTerm.get() << std::endl; + Trace("strings-eqc-debug") + << "* Cardinality lemma k : " << ei->d_cardinalityLemK.get() + << std::endl; + Trace("strings-eqc-debug") + << "* Normalization length lemma : " + << ei->d_normalizedLength.get() << std::endl; + } + } + ++eqcs2_i; + } + ss << std::endl; + } + ss << std::endl; + return ss.str(); +} + }/* CVC4::theory::strings namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 12f644fb4..f35c67da6 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -241,6 +241,8 @@ class TheoryStrings : public Theory { void runInferStep(InferStep s, int effort); /** run strategy for effort e */ void runStrategy(Theory::Effort e); + /** print strings equivalence classes for debugging */ + std::string debugPrintStringsEqc(); /** Commonly used constants */ Node d_true; Node d_false; diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 0c1ea7a7a..a5f8afec4 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -451,25 +451,30 @@ bool TheoryModel::assertEqualityEngine(const eq::EqualityEngine* ee, bool first = true; Node rep; for (; !eqc_i.isFinished(); ++eqc_i) { - if (termSet != NULL && termSet->find(*eqc_i) == termSet->end()) { - Trace("model-builder-debug") << "...skip node " << (*eqc_i) << " in eqc " << eqc << std::endl; + Node n = *eqc_i; + // notice that constants are always relevant + if (termSet != nullptr && termSet->find(n) == termSet->end() + && !n.isConst()) + { + Trace("model-builder-debug") + << "...skip node " << n << " in eqc " << eqc << std::endl; continue; } if (predicate) { if (predTrue || predFalse) { - if (!assertPredicate(*eqc_i, predTrue)) + if (!assertPredicate(n, predTrue)) { return false; } } else { if (first) { - rep = (*eqc_i); + rep = n; first = false; } else { - Node eq = (*eqc_i).eqNode(rep); + Node eq = (n).eqNode(rep); Trace("model-builder-assertions") << "(assert " << eq << ");" << std::endl; d_equalityEngine->assertEquality(eq, true, Node::null()); @@ -481,7 +486,7 @@ bool TheoryModel::assertEqualityEngine(const eq::EqualityEngine* ee, } } else { if (first) { - rep = (*eqc_i); + rep = n; //add the term (this is specifically for the case of singleton equivalence classes) if (rep.getType().isFirstClass()) { @@ -491,7 +496,7 @@ bool TheoryModel::assertEqualityEngine(const eq::EqualityEngine* ee, first = false; } else { - if (!assertEquality(*eqc_i, rep, true)) + if (!assertEquality(n, rep, true)) { return false; } @@ -745,5 +750,19 @@ std::vector< Node > TheoryModel::getFunctionsToAssign() { const std::string& TheoryModel::getName() const { return d_name; } +std::string TheoryModel::debugPrintModelEqc() const +{ + std::stringstream ss; + ss << "--- Equivalence classes:" << std::endl; + ss << d_equalityEngine->debugPrintEqc() << std::endl; + ss << "--- Representative map: " << std::endl; + for (const std::pair& r : d_reps) + { + ss << r.first << " -> " << r.second << std::endl; + } + ss << "---" << std::endl; + return ss.str(); +} + } /* namespace CVC4::theory */ } /* namespace CVC4 */ diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index 2f895ab83..0c7f092bc 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -347,6 +347,11 @@ public: //---------------------------- end function values /** Get the name of this model */ const std::string& getName() const; + /** + * For debugging, print the equivalence classes of the underlying equality + * engine. + */ + std::string debugPrintModelEqc() const; protected: /** Unique name of this model */ @@ -405,7 +410,6 @@ public: * a model builder constructs this model. */ virtual void addTermInternal(TNode n); - private: /** cache for getModelValue */ mutable std::unordered_map d_modelCache; diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 8b44cc4d9..2d34bd547 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -2075,6 +2075,29 @@ void EqualityEngine::debugPrintGraph() const { Debug("equality::graph") << std::endl; } +std::string EqualityEngine::debugPrintEqc() const +{ + std::stringstream ss; + eq::EqClassesIterator eqcs2_i = eq::EqClassesIterator(this); + while (!eqcs2_i.isFinished()) + { + Node eqc = (*eqcs2_i); + eq::EqClassIterator eqc2_i = eq::EqClassIterator(eqc, this); + ss << "Eqc( " << eqc << " ) : { "; + while (!eqc2_i.isFinished()) + { + if ((*eqc2_i) != eqc && (*eqc2_i).getKind() != kind::EQUAL) + { + ss << (*eqc2_i) << " "; + } + ++eqc2_i; + } + ss << " } " << std::endl; + ++eqcs2_i; + } + return ss.str(); +} + bool EqualityEngine::areEqual(TNode t1, TNode t2) const { Debug("equality") << d_name << "::eq::areEqual(" << t1 << "," << t2 << ")"; diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index b81a17dcf..d1c0ece95 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -93,6 +93,9 @@ class EqualityEngine : public context::ContextNotifyObj { */ void setMasterEqualityEngine(EqualityEngine* master); + /** Print the equivalence classes for debugging */ + std::string debugPrintEqc() const; + /** Statistics about the equality engine instance */ struct Statistics { -- 2.30.2