diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-03-20 06:42:51 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-03-20 11:42:51 +0000 |
commit | 02dd48563db0c5effd608eda70d4c262309322a6 (patch) | |
tree | a64819d326b5d9d029e47b6ba14ead7c7b23628c /src/theory/theory_model.cpp | |
parent | a374f7b577b48908d623cf7b64594f1c98cfb8b7 (diff) |
Improved tracing for equivalence classes of EE (#6169)
Helps debugging model issues.
Diffstat (limited to 'src/theory/theory_model.cpp')
-rw-r--r-- | src/theory/theory_model.cpp | 33 |
1 files changed, 26 insertions, 7 deletions
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<const Node, Node>& r : d_reps) + { + ss << r.first << " -> " << r.second << std::endl; + } + ss << "---" << std::endl; + return ss.str(); +} + } /* namespace CVC4::theory */ } /* namespace CVC4 */ |