From 1415f6234cf8ca17711d384863a4a21867477577 Mon Sep 17 00:00:00 2001 From: mudathirmahgoub Date: Fri, 17 Dec 2021 14:23:02 -0600 Subject: [PATCH] Remove Rewriter::rewrite from bags type enumerator (#7827) --- .../bags/theory_bags_type_enumerator.cpp | 21 +++++++++++-------- 1 file changed, 12 insertions(+), 9 deletions(-) diff --git a/src/theory/bags/theory_bags_type_enumerator.cpp b/src/theory/bags/theory_bags_type_enumerator.cpp index 0bfef55d2..14fca3297 100644 --- a/src/theory/bags/theory_bags_type_enumerator.cpp +++ b/src/theory/bags/theory_bags_type_enumerator.cpp @@ -16,7 +16,7 @@ #include "theory/bags/theory_bags_type_enumerator.h" #include "expr/emptybag.h" -#include "theory/rewriter.h" +#include "theory/bags/normal_form.h" #include "theory_bags_type_enumerator.h" #include "util/rational.h" @@ -56,22 +56,25 @@ Node BagEnumerator::operator*() BagEnumerator& BagEnumerator::operator++() { - // increase the multiplicity by one - Node one = d_nodeManager->mkConstInt(Rational(1)); - TypeNode elementType = d_elementTypeEnumerator.getType(); - Node singleton = d_nodeManager->mkBag(elementType, d_element, one); if (d_currentBag.getKind() == kind::BAG_EMPTY) { + // return (bag d_element 1) + Node one = d_nodeManager->mkConstInt(Rational(1)); + TypeNode elementType = d_elementTypeEnumerator.getType(); + Node singleton = d_nodeManager->mkBag(elementType, d_element, one); d_currentBag = singleton; } else { - d_currentBag = d_nodeManager->mkNode( - kind::BAG_UNION_DISJOINT, singleton, d_currentBag); + // increase the multiplicity of one of the elements in the current bag + std::map elements = + NormalForm::getBagElements(d_currentBag); + Node element = elements.begin()->first; + elements[element] = elements[element] + Rational(1); + d_currentBag = NormalForm::constructConstantBagFromElements( + d_currentBag.getType(), elements); } - d_currentBag = Rewriter::rewrite(d_currentBag); - Assert(d_currentBag.isConst()); Trace("bag-type-enum") << "BagEnumerator::operator++ d_currentBag = " -- 2.30.2