From 35b05367c5caa47f4be367c257b4a9c411ebfd38 Mon Sep 17 00:00:00 2001
From: mudathirmahgoub <mudathirmahgoub@gmail.com>
Date: Thu, 16 Dec 2021 09:31:47 -0600
Subject: [PATCH] Add regression bags-of-bags-subtypes.smt2 (#7814)

---
 src/theory/bags/inference_generator.cpp          | 16 ++++++++--------
 test/regress/CMakeLists.txt                      |  1 +
 .../regress1/bags/bags-of-bags-subtypes.smt2     | 14 ++++++++++++++
 3 files changed, 23 insertions(+), 8 deletions(-)
 create mode 100644 test/regress/regress1/bags/bags-of-bags-subtypes.smt2

diff --git a/src/theory/bags/inference_generator.cpp b/src/theory/bags/inference_generator.cpp
index cb6a3ea70..9be0c2b93 100644
--- a/src/theory/bags/inference_generator.cpp
+++ b/src/theory/bags/inference_generator.cpp
@@ -43,7 +43,7 @@ InferenceGenerator::InferenceGenerator(SolverState* state, InferenceManager* im)
 InferInfo InferenceGenerator::nonNegativeCount(Node n, Node e)
 {
   Assert(n.getType().isBag());
-  Assert(e.getType() == n.getType().getBagElementType());
+  Assert(e.getType().isSubtypeOf(n.getType().getBagElementType()));
 
   InferInfo inferInfo(d_im, InferenceId::BAGS_NON_NEGATIVE_COUNT);
   Node count = d_nm->mkNode(BAG_COUNT, e, n);
@@ -56,7 +56,7 @@ InferInfo InferenceGenerator::nonNegativeCount(Node n, Node e)
 InferInfo InferenceGenerator::bagMake(Node n, Node e)
 {
   Assert(n.getKind() == BAG_MAKE);
-  Assert(e.getType() == n.getType().getBagElementType());
+  Assert(e.getType().isSubtypeOf(n.getType().getBagElementType()));
 
   /*
    * (ite (and (= e x) (>= c 1))
@@ -156,7 +156,7 @@ InferInfo InferenceGenerator::empty(Node n, Node e)
 InferInfo InferenceGenerator::unionDisjoint(Node n, Node e)
 {
   Assert(n.getKind() == BAG_UNION_DISJOINT && n[0].getType().isBag());
-  Assert(e.getType() == n[0].getType().getBagElementType());
+  Assert(e.getType().isSubtypeOf(n[0].getType().getBagElementType()));
 
   Node A = n[0];
   Node B = n[1];
@@ -178,7 +178,7 @@ InferInfo InferenceGenerator::unionDisjoint(Node n, Node e)
 InferInfo InferenceGenerator::unionMax(Node n, Node e)
 {
   Assert(n.getKind() == BAG_UNION_MAX && n[0].getType().isBag());
-  Assert(e.getType() == n[0].getType().getBagElementType());
+  Assert(e.getType().isSubtypeOf(n[0].getType().getBagElementType()));
 
   Node A = n[0];
   Node B = n[1];
@@ -201,7 +201,7 @@ InferInfo InferenceGenerator::unionMax(Node n, Node e)
 InferInfo InferenceGenerator::intersection(Node n, Node e)
 {
   Assert(n.getKind() == BAG_INTER_MIN && n[0].getType().isBag());
-  Assert(e.getType() == n[0].getType().getBagElementType());
+  Assert(e.getType().isSubtypeOf(n[0].getType().getBagElementType()));
 
   Node A = n[0];
   Node B = n[1];
@@ -222,7 +222,7 @@ InferInfo InferenceGenerator::intersection(Node n, Node e)
 InferInfo InferenceGenerator::differenceSubtract(Node n, Node e)
 {
   Assert(n.getKind() == BAG_DIFFERENCE_SUBTRACT && n[0].getType().isBag());
-  Assert(e.getType() == n[0].getType().getBagElementType());
+  Assert(e.getType().isSubtypeOf(n[0].getType().getBagElementType()));
 
   Node A = n[0];
   Node B = n[1];
@@ -244,7 +244,7 @@ InferInfo InferenceGenerator::differenceSubtract(Node n, Node e)
 InferInfo InferenceGenerator::differenceRemove(Node n, Node e)
 {
   Assert(n.getKind() == BAG_DIFFERENCE_REMOVE && n[0].getType().isBag());
-  Assert(e.getType() == n[0].getType().getBagElementType());
+  Assert(e.getType().isSubtypeOf(n[0].getType().getBagElementType()));
 
   Node A = n[0];
   Node B = n[1];
@@ -266,7 +266,7 @@ InferInfo InferenceGenerator::differenceRemove(Node n, Node e)
 InferInfo InferenceGenerator::duplicateRemoval(Node n, Node e)
 {
   Assert(n.getKind() == BAG_DUPLICATE_REMOVAL && n[0].getType().isBag());
-  Assert(e.getType() == n[0].getType().getBagElementType());
+  Assert(e.getType().isSubtypeOf(n[0].getType().getBagElementType()));
 
   Node A = n[0];
   InferInfo inferInfo(d_im, InferenceId::BAGS_DUPLICATE_REMOVAL);
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 6943b7250..05abda285 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1604,6 +1604,7 @@ set(regress_1_tests
   regress1/bug681.smt2
   regress1/bug694-Unapply1.scala-0.smt2
   regress1/bug800.smt2
+  regress1/bags/bags-of-bags-subtypes.smt2
   regress1/bags/card1.smt2
   regress1/bags/card2.smt2
   regress1/bags/choose1.smt2
diff --git a/test/regress/regress1/bags/bags-of-bags-subtypes.smt2 b/test/regress/regress1/bags/bags-of-bags-subtypes.smt2
new file mode 100644
index 000000000..b48228c93
--- /dev/null
+++ b/test/regress/regress1/bags/bags-of-bags-subtypes.smt2
@@ -0,0 +1,14 @@
+(set-logic ALL)
+(set-info :status sat)
+
+(declare-fun s () (Bag (Bag Real)))
+(declare-fun t () (Bag (Bag Real)))
+
+(declare-fun x () (Bag Real))
+(declare-fun y () (Bag Real))
+
+(assert (>= (bag.count 0.5 y) 1))
+(assert (>= (bag.count y s) 1))
+(assert (or (= s t) (= s (bag (bag 1.0 1) 1)) (= s (bag (bag 0.0 1) 1))))
+
+(check-sat)
-- 
2.30.2