From: mudathirmahgoub Date: Thu, 16 Dec 2021 15:31:47 +0000 (-0600) Subject: Add regression bags-of-bags-subtypes.smt2 (#7814) X-Git-Tag: cvc5-1.0.0~657 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=35b05367c5caa47f4be367c257b4a9c411ebfd38;p=cvc5.git 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 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)