Remove Rewriter::rewrite from bags type enumerator (#7827)

diff --git a/src/theory/bags/theory_bags_type_enumerator.cpp b/src/theory/bags/theory_bags_type_enumerator.cpp
index 0bfef55d249b2bdf619cd17f57434bf62818ffab..14fca3297dc0df6bdb4ac3ac40ffbb372f205d50 100644 (file)
--- 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<Node, Rational> 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 = "