From 2bf6f49039b7c9fee6a7da846e329eb9be75713c Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 22 Jul 2021 11:57:46 -0500 Subject: [PATCH] Simplify computation of relevant terms in datatypes (#6885) This makes it so that we do not consider non-singleton equivalence classes of DT for non-datatype terms to be relevant. This impacts how model construction is done for datatypes. It's not clear why this method considered such terms to be relevant, I believe this was done to mask a previous bug; regressions now pass when this method is simplified. Doing this is definitely wrong when using central equality engine, hence the motivation for this simplification. --- src/theory/datatypes/theory_datatypes.cpp | 28 +++-------------------- 1 file changed, 3 insertions(+), 25 deletions(-) diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 53f128286..d951f94a7 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -1852,38 +1852,16 @@ void TheoryDatatypes::computeRelevantTerms(std::set& termSet) Trace("dt-cmi") << "Have " << termSet.size() << " relevant terms..." << std::endl; - //also include non-singleton equivalence classes TODO : revisit this + //also include non-singleton dt equivalence classes TODO : revisit this eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(d_equalityEngine); while( !eqcs_i.isFinished() ){ TNode r = (*eqcs_i); - bool addedFirst = false; - Node first; - TypeNode rtn = r.getType(); - if (!rtn.isBoolean()) + if (r.getType().isDatatype()) { eq::EqClassIterator eqc_i = eq::EqClassIterator(r, d_equalityEngine); while (!eqc_i.isFinished()) { - TNode n = (*eqc_i); - if (first.isNull()) - { - first = n; - // always include all datatypes - if (rtn.isDatatype()) - { - addedFirst = true; - termSet.insert(n); - } - } - else - { - if (!addedFirst) - { - addedFirst = true; - termSet.insert(first); - } - termSet.insert(n); - } + termSet.insert(*eqc_i); ++eqc_i; } } -- 2.30.2