Add regression bags-of-bags-subtypes.smt2 (#7814)

diff --git a/src/theory/bags/inference_generator.cpp b/src/theory/bags/inference_generator.cpp
index cb6a3ea7092b7812dd15af32b5173fe49cc214ed..9be0c2b9375e02e9dedf7c68959dfd926724ae49 100644 (file)
--- 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 6943b72508bbe17cf522cc36b25a779dac4066d2..05abda285a34d59281446e55c0f5b56c71389f79 100644 (file)
--- 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 (file)
index 0000000..b48228c
--- /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)