Add posRewriteEqual to bags rewriter (#5498)

This PR fixes #5460 by adding posRewriteEqual to bags rewriter

4 files changed, 45 insertions, 3 deletions

diff --git a/src/theory/bags/bags_rewriter.cpp b/src/theory/bags/bags_rewriter.cpp
index f0540e9b7..9479d2cc2 100644
--- a/src/theory/bags/bags_rewriter.cpp
+++ b/src/theory/bags/bags_rewriter.cpp
@@ -51,6 +51,10 @@ RewriteResponse BagsRewriter::postRewrite(TNode n)
     // no need to rewrite n if it is already in a normal form
     response = BagsRewriteResponse(n, Rewrite::NONE);
   }
+  else if(n.getKind() == EQUAL)
+  {
+    response = postRewriteEqual(n);
+  }
   else if (NormalForm::areChildrenConstants(n))
   {
     Node value = NormalForm::evaluate(n);
@@ -98,7 +102,7 @@ RewriteResponse BagsRewriter::preRewrite(TNode n)
   Kind k = n.getKind();
   switch (k)
   {
-    case EQUAL: response = rewriteEqual(n); break;
+    case EQUAL: response = preRewriteEqual(n); break;
     case SUBBAG: response = rewriteSubBag(n); break;
     default: response = BagsRewriteResponse(n, Rewrite::NONE);
   }
@@ -117,7 +121,7 @@ RewriteResponse BagsRewriter::preRewrite(TNode n)
   return RewriteResponse(RewriteStatus::REWRITE_DONE, n);
 }
 
-BagsRewriteResponse BagsRewriter::rewriteEqual(const TNode& n) const
+BagsRewriteResponse BagsRewriter::preRewriteEqual(const TNode& n) const
 {
   Assert(n.getKind() == EQUAL);
   if (n[0] == n[1])
@@ -475,6 +479,30 @@ BagsRewriteResponse BagsRewriter::rewriteToSet(const TNode& n) const
   return BagsRewriteResponse(n, Rewrite::NONE);
 }
 
+BagsRewriteResponse BagsRewriter::postRewriteEqual(const TNode& n) const
+{
+  Assert(n.getKind() == kind::EQUAL);
+  if (n[0] == n[1])
+  {
+    Node ret = NodeManager::currentNM()->mkConst(true);
+    return BagsRewriteResponse(ret, Rewrite::EQ_REFL);
+  }
+
+  if (n[0].isConst() && n[1].isConst())
+  {
+    Node ret = NodeManager::currentNM()->mkConst(false);
+    return BagsRewriteResponse(ret, Rewrite::EQ_CONST_FALSE);
+  }
+
+  // standard ordering
+  if (n[0] > n[1])
+  {
+    Node ret = NodeManager::currentNM()->mkNode(kind::EQUAL, n[1], n[0]);
+    return BagsRewriteResponse(ret, Rewrite::EQ_SYM);
+  }
+  return BagsRewriteResponse(n, Rewrite::NONE);
+}
+
 }  // namespace bags
 }  // namespace theory
 }  // namespace CVC4
diff --git a/src/theory/bags/bags_rewriter.h b/src/theory/bags/bags_rewriter.h
index 8be6b948a..a9b3b90bb 100644
--- a/src/theory/bags/bags_rewriter.h
+++ b/src/theory/bags/bags_rewriter.h
@@ -60,7 +60,7 @@ class BagsRewriter : public TheoryRewriter
    * rewrites for n include:
    * - (= A A) = true where A is a bag
    */
-  BagsRewriteResponse rewriteEqual(const TNode& n) const;
+  BagsRewriteResponse preRewriteEqual(const TNode& n) const;
 
   /**
    * rewrites for n include:
@@ -202,6 +202,14 @@ class BagsRewriter : public TheoryRewriter
    */
   BagsRewriteResponse rewriteToSet(const TNode& n) const;
 
+  /**
+   *  rewrites for n include:
+   *  - (= A A) = true
+   *  - (= A B) = false if A and B are different bag constants
+   *  - (= B A) = (= A B) if A < B and at least one of A or B is not a constant
+   */
+  BagsRewriteResponse postRewriteEqual(const TNode& n) const;
+
  private:
   /** Reference to the rewriter statistics. */
   NodeManager* d_nm;
diff --git a/src/theory/bags/rewrites.cpp b/src/theory/bags/rewrites.cpp
index d640bcdce..85d0820af 100644
--- a/src/theory/bags/rewrites.cpp
+++ b/src/theory/bags/rewrites.cpp
@@ -32,6 +32,9 @@ const char* toString(Rewrite r)
     case Rewrite::COUNT_EMPTY: return "COUNT_EMPTY";
     case Rewrite::COUNT_MK_BAG: return "COUNT_MK_BAG";
     case Rewrite::DUPLICATE_REMOVAL_MK_BAG: return "DUPLICATE_REMOVAL_MK_BAG";
+    case Rewrite::EQ_CONST_FALSE: return "EQ_CONST_FALSE";
+    case Rewrite::EQ_REFL: return "EQ_REFL";
+    case Rewrite::EQ_SYM: return "EQ_SYM";
     case Rewrite::FROM_SINGLETON: return "FROM_SINGLETON";
     case Rewrite::IDENTICAL_NODES: return "IDENTICAL_NODES";
     case Rewrite::INTERSECTION_EMPTY_LEFT: return "INTERSECTION_EMPTY_LEFT";
diff --git a/src/theory/bags/rewrites.h b/src/theory/bags/rewrites.h
index 36e30ca68..5574aa080 100644
--- a/src/theory/bags/rewrites.h
+++ b/src/theory/bags/rewrites.h
@@ -37,6 +37,9 @@ enum class Rewrite : uint32_t
   COUNT_EMPTY,
   COUNT_MK_BAG,
   DUPLICATE_REMOVAL_MK_BAG,
+  EQ_CONST_FALSE,
+  EQ_REFL,
+  EQ_SYM,
   FROM_SINGLETON,
   IDENTICAL_NODES,
   INTERSECTION_EMPTY_LEFT,