diff options
Diffstat (limited to 'test')
25 files changed, 306 insertions, 285 deletions
diff --git a/test/regress/regress1/bags/choose1.smt2 b/test/regress/regress1/bags/choose1.smt2 index b157bbc70..53cd7c771 100644 --- a/test/regress/regress1/bags/choose1.smt2 +++ b/test/regress/regress1/bags/choose1.smt2 @@ -3,7 +3,7 @@ (set-info :status sat) (declare-fun A () (Bag Int)) (declare-fun a () Int) -(assert (not (= A (as emptybag (Bag Int))))) +(assert (not (= A (as bag.empty (Bag Int))))) (assert (= (bag.choose A) 10)) (assert (= a (bag.choose A))) (assert (exists ((x Int)) (and (= x (bag.choose A)) (= x a)))) diff --git a/test/regress/regress1/bags/choose3.smt2 b/test/regress/regress1/bags/choose3.smt2 index ffa9ae9a7..adf1a3e21 100644 --- a/test/regress/regress1/bags/choose3.smt2 +++ b/test/regress/regress1/bags/choose3.smt2 @@ -4,5 +4,5 @@ (set-info :status sat) (declare-fun A () (Bag Int)) (assert (= (bag.choose A) 10)) -(assert (= A (as emptybag (Bag Int)))) +(assert (= A (as bag.empty (Bag Int)))) (check-sat) diff --git a/test/regress/regress1/bags/choose4.smt2 b/test/regress/regress1/bags/choose4.smt2 index a0290b90b..cdf4065d4 100644 --- a/test/regress/regress1/bags/choose4.smt2 +++ b/test/regress/regress1/bags/choose4.smt2 @@ -3,7 +3,7 @@ (set-info :status sat) (declare-fun A () (Bag Int)) (declare-fun a () Int) -(assert (not (= A (as emptybag (Bag Int))))) +(assert (not (= A (as bag.empty (Bag Int))))) (assert (> (bag.count 10 A) 0)) (assert (= a (bag.choose A))) (check-sat) diff --git a/test/regress/regress1/bags/difference_remove1.smt2 b/test/regress/regress1/bags/difference_remove1.smt2 index f5a87c149..82f6ec53d 100644 --- a/test/regress/regress1/bags/difference_remove1.smt2 +++ b/test/regress/regress1/bags/difference_remove1.smt2 @@ -4,7 +4,7 @@ (declare-fun B () (Bag Int)) (declare-fun x () Int) (declare-fun y () Int) -(assert (= A (union_max (bag x 1) (bag y 2)))) -(assert (= A (union_disjoint B (bag y 2)))) +(assert (= A (bag.union_max (bag x 1) (bag y 2)))) +(assert (= A (bag.union_disjoint B (bag y 2)))) (assert (= x y)) (check-sat) diff --git a/test/regress/regress1/bags/duplicate_removal1.smt2 b/test/regress/regress1/bags/duplicate_removal1.smt2 index 2b662c6e5..27ce2360b 100644 --- a/test/regress/regress1/bags/duplicate_removal1.smt2 +++ b/test/regress/regress1/bags/duplicate_removal1.smt2 @@ -3,6 +3,6 @@ (set-option :produce-models true) (declare-fun A () (Bag String)) (declare-fun B () (Bag String)) -(assert (= B (duplicate_removal A))) -(assert (distinct (as emptybag (Bag String)) A B)) +(assert (= B (bag.duplicate_removal A))) +(assert (distinct (as bag.empty (Bag String)) A B)) (check-sat) diff --git a/test/regress/regress1/bags/duplicate_removal2.smt2 b/test/regress/regress1/bags/duplicate_removal2.smt2 index 7dacaae43..5382f773f 100644 --- a/test/regress/regress1/bags/duplicate_removal2.smt2 +++ b/test/regress/regress1/bags/duplicate_removal2.smt2 @@ -2,7 +2,7 @@ (set-info :status unsat) (declare-fun A () (Bag String)) (declare-fun B () (Bag String)) -(assert (= B (duplicate_removal A))) -(assert (distinct (as emptybag (Bag String)) A B)) -(assert (= B (union_max A B))) +(assert (= B (bag.duplicate_removal A))) +(assert (distinct (as bag.empty (Bag String)) A B)) +(assert (= B (bag.union_max A B))) (check-sat)
\ No newline at end of file diff --git a/test/regress/regress1/bags/emptybag1.smt2 b/test/regress/regress1/bags/emptybag1.smt2 index f7f92599d..61b29f414 100644 --- a/test/regress/regress1/bags/emptybag1.smt2 +++ b/test/regress/regress1/bags/emptybag1.smt2 @@ -4,7 +4,7 @@ (declare-fun x () String) (declare-fun y () Int) (assert (= x "x")) -(assert (= A (as emptybag (Bag String)))) +(assert (= A (as bag.empty (Bag String)))) (assert (= (bag.count x A) y)) (assert(> y 1)) (check-sat) diff --git a/test/regress/regress1/bags/fuzzy1.smt2 b/test/regress/regress1/bags/fuzzy1.smt2 index f9fee0ec4..79ccc4b82 100644 --- a/test/regress/regress1/bags/fuzzy1.smt2 +++ b/test/regress/regress1/bags/fuzzy1.smt2 @@ -5,6 +5,6 @@ (declare-fun c () Int) ; c here is zero (assert (and - (= b (difference_subtract b a)) ; b is empty + (= b (bag.difference_subtract b a)) ; b is empty (= a (bag (tuple c 0) 1)))) ; a = {|(<0, 0>, 1)|} (check-sat) diff --git a/test/regress/regress1/bags/fuzzy2.smt2 b/test/regress/regress1/bags/fuzzy2.smt2 index 31da47f53..c7968b274 100644 --- a/test/regress/regress1/bags/fuzzy2.smt2 +++ b/test/regress/regress1/bags/fuzzy2.smt2 @@ -8,8 +8,8 @@ (let ((D (bag d c))) ; when c = zero, then D is empty (and (= a (bag (tuple 1 1) c)) ; when c = zero, then a is empty - (= a (union_max a D)) - (= a (difference_subtract a (bag d 1))) - (= a (union_disjoint a D)) - (= a (intersection_min a D))))) + (= a (bag.union_max a D)) + (= a (bag.difference_subtract a (bag d 1))) + (= a (bag.union_disjoint a D)) + (= a (bag.inter_min a D))))) (check-sat) diff --git a/test/regress/regress1/bags/fuzzy3.smt2 b/test/regress/regress1/bags/fuzzy3.smt2 index dd6dd02dc..a457bf9ae 100644 --- a/test/regress/regress1/bags/fuzzy3.smt2 +++ b/test/regress/regress1/bags/fuzzy3.smt2 @@ -8,6 +8,6 @@ (assert (not (= - (= A (difference_remove (bag d c) A)) + (= A (bag.difference_remove (bag d c) A)) (= A (bag (tuple c c) c))))) (check-sat) diff --git a/test/regress/regress1/bags/fuzzy4.smt2 b/test/regress/regress1/bags/fuzzy4.smt2 index b733a4862..5b24b8d6e 100644 --- a/test/regress/regress1/bags/fuzzy4.smt2 +++ b/test/regress/regress1/bags/fuzzy4.smt2 @@ -7,8 +7,8 @@ (assert (not (= - (= A (bag d (+ c (bag.count d (union_disjoint A A))))) - (= A (difference_remove (bag d c) A))))) + (= A (bag d (+ c (bag.count d (bag.union_disjoint A A))))) + (= A (bag.difference_remove (bag d c) A))))) (assert (= A (bag (tuple 0 0) 5))) (assert (= c (- 5))) (assert (= d (tuple 0 0))) diff --git a/test/regress/regress1/bags/fuzzy5.smt2 b/test/regress/regress1/bags/fuzzy5.smt2 index 2dea236a5..0674fad9c 100644 --- a/test/regress/regress1/bags/fuzzy5.smt2 +++ b/test/regress/regress1/bags/fuzzy5.smt2 @@ -10,7 +10,7 @@ (and (not (= (= A (bag (tuple 0 c) (+ c c))) - (= A (difference_remove (bag d c) A)))) + (= A (bag.difference_remove (bag d c) A)))) (not (= (= A (bag (tuple 0 1) c_plus_1)) (= A (bag (tuple c 1) c_plus_1))))))) diff --git a/test/regress/regress1/bags/intersection_min1.smt2 b/test/regress/regress1/bags/intersection_min1.smt2 index f5a515b9c..0ced4aa89 100644 --- a/test/regress/regress1/bags/intersection_min1.smt2 +++ b/test/regress/regress1/bags/intersection_min1.smt2 @@ -4,7 +4,7 @@ (declare-fun A () (Bag String)) (declare-fun B () (Bag String)) (declare-fun C () (Bag String)) -(assert (= C (intersection_min A B))) -(assert (distinct (as emptybag (Bag String)) C)) +(assert (= C (bag.inter_min A B))) +(assert (distinct (as bag.empty (Bag String)) C)) (assert (distinct A B C)) (check-sat)
\ No newline at end of file diff --git a/test/regress/regress1/bags/intersection_min2.smt2 b/test/regress/regress1/bags/intersection_min2.smt2 index 66afa2f3a..119f34665 100644 --- a/test/regress/regress1/bags/intersection_min2.smt2 +++ b/test/regress/regress1/bags/intersection_min2.smt2 @@ -3,7 +3,7 @@ (declare-fun A () (Bag String)) (declare-fun B () (Bag String)) (declare-fun C () (Bag String)) -(assert (= C (intersection_min A B))) -(assert (= C (union_disjoint A B))) -(assert (distinct (as emptybag (Bag String)) C)) +(assert (= C (bag.inter_min A B))) +(assert (= C (bag.union_disjoint A B))) +(assert (distinct (as bag.empty (Bag String)) C)) (check-sat) diff --git a/test/regress/regress1/bags/issue5759.smt2 b/test/regress/regress1/bags/issue5759.smt2 index ba3752e09..1c29afea6 100644 --- a/test/regress/regress1/bags/issue5759.smt2 +++ b/test/regress/regress1/bags/issue5759.smt2 @@ -4,7 +4,7 @@ (declare-fun A () (Bag Int)) (declare-fun B () (Bag Int)) (declare-fun x () Int) -(assert (not (= A (union_max (bag x 1) (bag 0 1))))) -(assert (= A (union_disjoint B (bag 0 1)))) +(assert (not (= A (bag.union_max (bag x 1) (bag 0 1))))) +(assert (= A (bag.union_disjoint B (bag 0 1)))) (assert (= x 1)) (check-sat)
\ No newline at end of file diff --git a/test/regress/regress1/bags/map1.smt2 b/test/regress/regress1/bags/map1.smt2 index 54d671415..c7dc3d636 100644 --- a/test/regress/regress1/bags/map1.smt2 +++ b/test/regress/regress1/bags/map1.smt2 @@ -5,8 +5,8 @@ (declare-fun x () Int) (declare-fun y () Int) (declare-fun f (Int) Int) -(assert (= A (union_max (bag x 1) (bag y 2)))) -(assert (= A (union_max (bag x 1) (bag y 2)))) +(assert (= A (bag.union_max (bag x 1) (bag y 2)))) +(assert (= A (bag.union_max (bag x 1) (bag y 2)))) (assert (= B (bag.map f A))) (assert (distinct (f x) (f y) x y)) (check-sat) diff --git a/test/regress/regress1/bags/map3.smt2 b/test/regress/regress1/bags/map3.smt2 index 637815fa5..ae0184008 100644 --- a/test/regress/regress1/bags/map3.smt2 +++ b/test/regress/regress1/bags/map3.smt2 @@ -6,5 +6,5 @@ (define-fun f ((x Int)) Int (+ x 1)) (assert (= B (bag.map f A))) (assert (= (bag.count (- 2) B) 57)) -(assert (= A (as emptybag (Bag Int)) )) +(assert (= A (as bag.empty (Bag Int)) )) (check-sat) diff --git a/test/regress/regress1/bags/subbag1.smt2 b/test/regress/regress1/bags/subbag1.smt2 index 055e47a17..7a6bf66d7 100644 --- a/test/regress/regress1/bags/subbag1.smt2 +++ b/test/regress/regress1/bags/subbag1.smt2 @@ -4,8 +4,8 @@ (declare-fun B () (Bag Int)) (declare-fun x () Int) (assert (= x 1)) -(assert (subbag A B)) -(assert (subbag B A)) +(assert (bag.subbag A B)) +(assert (bag.subbag B A)) (assert (= (bag.count x A) 5)) (assert (= (bag.count x B) 10)) (check-sat)
\ No newline at end of file diff --git a/test/regress/regress1/bags/subbag2.smt2 b/test/regress/regress1/bags/subbag2.smt2 index 6d5cde362..abdb3b7d9 100644 --- a/test/regress/regress1/bags/subbag2.smt2 +++ b/test/regress/regress1/bags/subbag2.smt2 @@ -4,8 +4,8 @@ (declare-fun B () (Bag Int)) (declare-fun x () Int) (declare-fun y () Int) -(assert (subbag A B)) -(assert (subbag B A)) +(assert (bag.subbag A B)) +(assert (bag.subbag B A)) (assert (= (bag.count x A) x)) (assert (= (bag.count y A) x)) (assert (distinct x y)) diff --git a/test/regress/regress1/bags/union_disjoint.smt2 b/test/regress/regress1/bags/union_disjoint.smt2 index d30ed4b14..fdb9d16d3 100644 --- a/test/regress/regress1/bags/union_disjoint.smt2 +++ b/test/regress/regress1/bags/union_disjoint.smt2 @@ -4,7 +4,7 @@ (declare-fun B () (Bag Int)) (declare-fun x () Int) (declare-fun y () Int) -(assert (= A (union_disjoint (bag x 1) (bag y 2)))) -(assert (= A (union_disjoint B (bag y 2)))) +(assert (= A (bag.union_disjoint (bag x 1) (bag y 2)))) +(assert (= A (bag.union_disjoint B (bag y 2)))) (assert (= x y)) (check-sat) diff --git a/test/regress/regress1/bags/union_max1.smt2 b/test/regress/regress1/bags/union_max1.smt2 index d278527b9..d41e1425a 100644 --- a/test/regress/regress1/bags/union_max1.smt2 +++ b/test/regress/regress1/bags/union_max1.smt2 @@ -4,7 +4,7 @@ (declare-fun B () (Bag Int)) (declare-fun x () Int) (declare-fun y () Int) -(assert (= A (union_max (bag x 1) (bag y 2)))) -(assert (= A (union_disjoint B (bag y 2)))) +(assert (= A (bag.union_max (bag x 1) (bag y 2)))) +(assert (= A (bag.union_disjoint B (bag y 2)))) (assert (= x y)) (check-sat)
\ No newline at end of file diff --git a/test/regress/regress1/bags/union_max2.smt2 b/test/regress/regress1/bags/union_max2.smt2 index dd4bceff5..1366130bf 100644 --- a/test/regress/regress1/bags/union_max2.smt2 +++ b/test/regress/regress1/bags/union_max2.smt2 @@ -4,8 +4,8 @@ (declare-fun B () (Bag Int)) (declare-fun x () Int) (declare-fun y () Int) -(assert (= A (union_max (bag x 1) (bag y 2)))) -(assert (= A (union_disjoint B (bag y 2)))) +(assert (= A (bag.union_max (bag x 1) (bag y 2)))) +(assert (= A (bag.union_disjoint B (bag y 2)))) (assert (= x y)) -(assert (distinct (as emptybag (Bag Int)) B)) +(assert (distinct (as bag.empty (Bag Int)) B)) (check-sat)
\ No newline at end of file diff --git a/test/unit/theory/theory_bags_normal_form_white.cpp b/test/unit/theory/theory_bags_normal_form_white.cpp index 6c52f539d..5f3abfcee 100644 --- a/test/unit/theory/theory_bags_normal_form_white.cpp +++ b/test/unit/theory/theory_bags_normal_form_white.cpp @@ -98,11 +98,11 @@ TEST_F(TestTheoryWhiteBagsNormalForm, bag_count) { // Examples // ------- - // (bag.count "x" (emptybag String)) = 0 - // (bag.count "x" (mkBag "y" 5)) = 0 - // (bag.count "x" (mkBag "x" 4)) = 4 - // (bag.count "x" (union_disjoint (mkBag "x" 4) (mkBag "y" 5)) = 4 - // (bag.count "x" (union_disjoint (mkBag "y" 5) (mkBag "z" 5)) = 0 + // (bag.count "x" (as bag.empty (Bag String))) = 0 + // (bag.count "x" (bag "y" 5)) = 0 + // (bag.count "x" (bag "x" 4)) = 4 + // (bag.count "x" (bag.union_disjoint (bag "x" 4) (bag "y" 5)) = 4 + // (bag.count "x" (bag.union_disjoint (bag "y" 5) (bag "z" 5)) = 0 Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)); Node four = d_nodeManager->mkConst(CONST_RATIONAL, Rational(4)); @@ -136,12 +136,12 @@ TEST_F(TestTheoryWhiteBagsNormalForm, bag_count) Node output3 = four; ASSERT_EQ(output2, NormalForm::evaluate(input2)); - Node unionDisjointXY = d_nodeManager->mkNode(UNION_DISJOINT, x_4, y_5); + Node unionDisjointXY = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_4, y_5); Node input4 = d_nodeManager->mkNode(BAG_COUNT, x, unionDisjointXY); Node output4 = four; ASSERT_EQ(output3, NormalForm::evaluate(input3)); - Node unionDisjointYZ = d_nodeManager->mkNode(UNION_DISJOINT, y_5, z_5); + Node unionDisjointYZ = d_nodeManager->mkNode(BAG_UNION_DISJOINT, y_5, z_5); Node input5 = d_nodeManager->mkNode(BAG_COUNT, x, unionDisjointYZ); Node output5 = zero; ASSERT_EQ(output4, NormalForm::evaluate(input4)); @@ -151,14 +151,15 @@ TEST_F(TestTheoryWhiteBagsNormalForm, duplicate_removal) { // Examples // -------- - // - (duplicate_removal (emptybag String)) = (emptybag String) - // - (duplicate_removal (mkBag "x" 4)) = (emptybag "x" 1) - // - (duplicate_removal (disjoint_union (mkBag "x" 3) (mkBag "y" 5)) = - // (disjoint_union (mkBag "x" 1) (mkBag "y" 1) + // - (bag.duplicate_removal (as bag.empty (Bag String))) = (as bag.empty (Bag + // String)) + // - (bag.duplicate_removal (bag "x" 4)) = (bag.empty"x" 1) + // - (bag.duplicate_removal (bag.union_disjoint(bag "x" 3) (bag "y" 5)) = + // (bag.union_disjoint(bag "x" 1) (bag "y" 1) Node emptybag = d_nodeManager->mkConst( EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType()))); - Node input1 = d_nodeManager->mkNode(DUPLICATE_REMOVAL, emptybag); + Node input1 = d_nodeManager->mkNode(BAG_DUPLICATE_REMOVAL, emptybag); Node output1 = emptybag; ASSERT_EQ(output1, NormalForm::evaluate(input1)); @@ -183,13 +184,13 @@ TEST_F(TestTheoryWhiteBagsNormalForm, duplicate_removal) y, d_nodeManager->mkConst(CONST_RATIONAL, Rational(5))); - Node input2 = d_nodeManager->mkNode(DUPLICATE_REMOVAL, x_4); + Node input2 = d_nodeManager->mkNode(BAG_DUPLICATE_REMOVAL, x_4); Node output2 = x_1; ASSERT_EQ(output2, NormalForm::evaluate(input2)); - Node normalBag = d_nodeManager->mkNode(UNION_DISJOINT, x_4, y_5); - Node input3 = d_nodeManager->mkNode(DUPLICATE_REMOVAL, normalBag); - Node output3 = d_nodeManager->mkNode(UNION_DISJOINT, x_1, y_1); + Node normalBag = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_4, y_5); + Node input3 = d_nodeManager->mkNode(BAG_DUPLICATE_REMOVAL, normalBag); + Node output3 = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_1, y_1); ASSERT_EQ(output3, NormalForm::evaluate(input3)); } @@ -197,13 +198,13 @@ TEST_F(TestTheoryWhiteBagsNormalForm, union_max) { // Example // ------- - // input: (union_max A B) - // where A = (union_disjoint (MK_BAG "x" 4) (MK_BAG "z" 2))) - // B = (union_disjoint (MK_BAG "x" 3) (MK_BAG "y" 1))) + // input: (bag.union_max A B) + // where A = (bag.union_disjoint (bag "x" 4) (bag "z" 2))) + // B = (bag.union_disjoint (bag "x" 3) (bag "y" 1))) // output: - // (union_disjoint A B) - // where A = (MK_BAG "x" 4) - // B = (union_disjoint (MK_BAG "y" 1) (MK_BAG "z" 2))) + // (bag.union_disjoint A B) + // where A = (bag "x" 4) + // B = (bag.union_disjoint (bag "y" 1) (bag "z" 2))) Node x = d_nodeManager->mkConst(String("x")); Node y = d_nodeManager->mkConst(String("y")); @@ -229,13 +230,15 @@ TEST_F(TestTheoryWhiteBagsNormalForm, union_max) y, d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))); - Node A = d_nodeManager->mkNode(UNION_DISJOINT, x_4, z_2); - Node B = d_nodeManager->mkNode(UNION_DISJOINT, x_3, y_1); - Node input = d_nodeManager->mkNode(UNION_MAX, A, B); + Node A = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_4, z_2); + Node B = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_3, y_1); + Node input = d_nodeManager->mkNode(BAG_UNION_MAX, A, B); // output Node output = d_nodeManager->mkNode( - UNION_DISJOINT, x_4, d_nodeManager->mkNode(UNION_DISJOINT, y_1, z_2)); + BAG_UNION_DISJOINT, + x_4, + d_nodeManager->mkNode(BAG_UNION_DISJOINT, y_1, z_2)); ASSERT_TRUE(output.isConst()); ASSERT_EQ(output, NormalForm::evaluate(input)); @@ -259,27 +262,27 @@ TEST_F(TestTheoryWhiteBagsNormalForm, union_disjoint1) elements[2], d_nodeManager->mkConst(CONST_RATIONAL, Rational(4))); - Node unionDisjointAB = d_nodeManager->mkNode(UNION_DISJOINT, A, B); + Node unionDisjointAB = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, B); // unionDisjointAB is already in a normal form ASSERT_TRUE(unionDisjointAB.isConst()); ASSERT_EQ(unionDisjointAB, NormalForm::evaluate(unionDisjointAB)); - Node unionDisjointBA = d_nodeManager->mkNode(UNION_DISJOINT, B, A); - // unionDisjointAB is is the normal form of unionDisjointBA + Node unionDisjointBA = d_nodeManager->mkNode(BAG_UNION_DISJOINT, B, A); + // unionDisjointAB is the normal form of unionDisjointBA ASSERT_FALSE(unionDisjointBA.isConst()); ASSERT_EQ(unionDisjointAB, NormalForm::evaluate(unionDisjointBA)); Node unionDisjointAB_C = - d_nodeManager->mkNode(UNION_DISJOINT, unionDisjointAB, C); - Node unionDisjointBC = d_nodeManager->mkNode(UNION_DISJOINT, B, C); + d_nodeManager->mkNode(BAG_UNION_DISJOINT, unionDisjointAB, C); + Node unionDisjointBC = d_nodeManager->mkNode(BAG_UNION_DISJOINT, B, C); Node unionDisjointA_BC = - d_nodeManager->mkNode(UNION_DISJOINT, A, unionDisjointBC); + d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, unionDisjointBC); // unionDisjointA_BC is the normal form of unionDisjointAB_C ASSERT_FALSE(unionDisjointAB_C.isConst()); ASSERT_TRUE(unionDisjointA_BC.isConst()); ASSERT_EQ(unionDisjointA_BC, NormalForm::evaluate(unionDisjointAB_C)); - Node unionDisjointAA = d_nodeManager->mkNode(UNION_DISJOINT, A, A); + Node unionDisjointAA = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, A); Node AA = d_nodeManager->mkBag(d_nodeManager->stringType(), elements[0], @@ -293,13 +296,13 @@ TEST_F(TestTheoryWhiteBagsNormalForm, union_disjoint2) { // Example // ------- - // input: (union_disjoint A B) - // where A = (union_disjoint (MK_BAG "x" 4) (MK_BAG "z" 2))) - // B = (union_disjoint (MK_BAG "x" 3) (MK_BAG "y" 1))) + // input: (bag.union_disjoint A B) + // where A = (bag.union_disjoint (bag "x" 4) (bag "z" 2))) + // B = (bag.union_disjoint (bag "x" 3) (bag "y" 1))) // output: - // (union_disjoint A B) - // where A = (MK_BAG "x" 7) - // B = (union_disjoint (MK_BAG "y" 1) (MK_BAG "z" 2))) + // (bag.union_disjoint A B) + // where A = (bag "x" 7) + // B = (bag.union_disjoint (bag "y" 1) (bag "z" 2))) Node x = d_nodeManager->mkConst(String("x")); Node y = d_nodeManager->mkConst(String("y")); @@ -325,13 +328,15 @@ TEST_F(TestTheoryWhiteBagsNormalForm, union_disjoint2) y, d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))); - Node A = d_nodeManager->mkNode(UNION_DISJOINT, x_4, z_2); - Node B = d_nodeManager->mkNode(UNION_DISJOINT, x_3, y_1); - Node input = d_nodeManager->mkNode(UNION_DISJOINT, A, B); + Node A = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_4, z_2); + Node B = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_3, y_1); + Node input = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, B); // output Node output = d_nodeManager->mkNode( - UNION_DISJOINT, x_7, d_nodeManager->mkNode(UNION_DISJOINT, y_1, z_2)); + BAG_UNION_DISJOINT, + x_7, + d_nodeManager->mkNode(BAG_UNION_DISJOINT, y_1, z_2)); ASSERT_TRUE(output.isConst()); ASSERT_EQ(output, NormalForm::evaluate(input)); @@ -341,11 +346,11 @@ TEST_F(TestTheoryWhiteBagsNormalForm, intersection_min) { // Example // ------- - // input: (intersection_min A B) - // where A = (union_disjoint (MK_BAG "x" 4) (MK_BAG "z" 2))) - // B = (union_disjoint (MK_BAG "x" 3) (MK_BAG "y" 1))) + // input: (bag.inter_min A B) + // where A = (bag.union_disjoint (bag "x" 4) (bag "z" 2))) + // B = (bag.union_disjoint (bag "x" 3) (bag "y" 1))) // output: - // (MK_BAG "x" 3) + // (bag "x" 3) Node x = d_nodeManager->mkConst(String("x")); Node y = d_nodeManager->mkConst(String("y")); @@ -371,9 +376,9 @@ TEST_F(TestTheoryWhiteBagsNormalForm, intersection_min) y, d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))); - Node A = d_nodeManager->mkNode(UNION_DISJOINT, x_4, z_2); - Node B = d_nodeManager->mkNode(UNION_DISJOINT, x_3, y_1); - Node input = d_nodeManager->mkNode(INTERSECTION_MIN, A, B); + Node A = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_4, z_2); + Node B = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_3, y_1); + Node input = d_nodeManager->mkNode(BAG_INTER_MIN, A, B); // output Node output = x_3; @@ -386,11 +391,11 @@ TEST_F(TestTheoryWhiteBagsNormalForm, difference_subtract) { // Example // ------- - // input: (difference_subtract A B) - // where A = (union_disjoint (MK_BAG "x" 4) (MK_BAG "z" 2))) - // B = (union_disjoint (MK_BAG "x" 3) (MK_BAG "y" 1))) + // input: (bag.difference_subtract A B) + // where A = (bag.union_disjoint (bag "x" 4) (bag "z" 2))) + // B = (bag.union_disjoint (bag "x" 3) (bag "y" 1))) // output: - // (union_disjoint (MK_BAG "x" 1) (MK_BAG "z" 2)) + // (bag.union_disjoint (bag "x" 1) (bag "z" 2)) Node x = d_nodeManager->mkConst(String("x")); Node y = d_nodeManager->mkConst(String("y")); @@ -420,12 +425,12 @@ TEST_F(TestTheoryWhiteBagsNormalForm, difference_subtract) y, d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))); - Node A = d_nodeManager->mkNode(UNION_DISJOINT, x_4, z_2); - Node B = d_nodeManager->mkNode(UNION_DISJOINT, x_3, y_1); - Node input = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, A, B); + Node A = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_4, z_2); + Node B = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_3, y_1); + Node input = d_nodeManager->mkNode(BAG_DIFFERENCE_SUBTRACT, A, B); // output - Node output = d_nodeManager->mkNode(UNION_DISJOINT, x_1, z_2); + Node output = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_1, z_2); ASSERT_TRUE(output.isConst()); ASSERT_EQ(output, NormalForm::evaluate(input)); @@ -435,11 +440,11 @@ TEST_F(TestTheoryWhiteBagsNormalForm, difference_remove) { // Example // ------- - // input: (difference_remove A B) - // where A = (union_disjoint (MK_BAG "x" 4) (MK_BAG "z" 2))) - // B = (union_disjoint (MK_BAG "x" 3) (MK_BAG "y" 1))) + // input: (bag.difference_remove A B) + // where A = (bag.union_disjoint (bag "x" 4) (bag "z" 2))) + // B = (bag.union_disjoint (bag "x" 3) (bag "y" 1))) // output: - // (MK_BAG "z" 2) + // (bag "z" 2) Node x = d_nodeManager->mkConst(String("x")); Node y = d_nodeManager->mkConst(String("y")); @@ -469,9 +474,9 @@ TEST_F(TestTheoryWhiteBagsNormalForm, difference_remove) y, d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))); - Node A = d_nodeManager->mkNode(UNION_DISJOINT, x_4, z_2); - Node B = d_nodeManager->mkNode(UNION_DISJOINT, x_3, y_1); - Node input = d_nodeManager->mkNode(DIFFERENCE_REMOVE, A, B); + Node A = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_4, z_2); + Node B = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_3, y_1); + Node input = d_nodeManager->mkNode(BAG_DIFFERENCE_REMOVE, A, B); // output Node output = z_2; @@ -484,9 +489,9 @@ TEST_F(TestTheoryWhiteBagsNormalForm, bag_card) { // Examples // -------- - // - (card (emptybag String)) = 0 - // - (choose (MK_BAG "x" 4)) = 4 - // - (choose (union_disjoint (MK_BAG "x" 4) (MK_BAG "y" 1))) = 5 + // - (bag.card (as bag.empty (Bag String))) = 0 + // - (bag.choose (bag "x" 4)) = 4 + // - (bag.choose (bag.union_disjoint (bag "x" 4) (bag "y" 1))) = 5 Node empty = d_nodeManager->mkConst( EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType()))); Node x = d_nodeManager->mkConst(String("x")); @@ -510,7 +515,7 @@ TEST_F(TestTheoryWhiteBagsNormalForm, bag_card) Node output2 = d_nodeManager->mkConst(CONST_RATIONAL, Rational(4)); ASSERT_EQ(output2, NormalForm::evaluate(input2)); - Node union_disjoint = d_nodeManager->mkNode(UNION_DISJOINT, x_4, y_1); + Node union_disjoint = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_4, y_1); Node input3 = d_nodeManager->mkNode(BAG_CARD, union_disjoint); Node output3 = d_nodeManager->mkConst(CONST_RATIONAL, Rational(5)); ASSERT_EQ(output3, NormalForm::evaluate(input3)); @@ -520,10 +525,10 @@ TEST_F(TestTheoryWhiteBagsNormalForm, is_singleton) { // Examples // -------- - // - (bag.is_singleton (emptybag String)) = false - // - (bag.is_singleton (MK_BAG "x" 1)) = true - // - (bag.is_singleton (MK_BAG "x" 4)) = false - // - (bag.is_singleton (union_disjoint (MK_BAG "x" 1) (MK_BAG "y" 1))) = + // - (bag.is_singleton (as bag.empty (Bag String))) = false + // - (bag.is_singleton (bag "x" 1)) = true + // - (bag.is_singleton (bag "x" 4)) = false + // - (bag.is_singleton (bag.union_disjoint (bag "x" 1) (bag "y" 1))) = // false Node falseNode = d_nodeManager->mkConst(false); Node trueNode = d_nodeManager->mkConst(true); @@ -557,7 +562,7 @@ TEST_F(TestTheoryWhiteBagsNormalForm, is_singleton) Node output3 = falseNode; ASSERT_EQ(output2, NormalForm::evaluate(input2)); - Node union_disjoint = d_nodeManager->mkNode(UNION_DISJOINT, x_1, y_1); + Node union_disjoint = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_1, y_1); Node input4 = d_nodeManager->mkNode(BAG_IS_SINGLETON, union_disjoint); Node output4 = falseNode; ASSERT_EQ(output3, NormalForm::evaluate(input3)); @@ -567,10 +572,10 @@ TEST_F(TestTheoryWhiteBagsNormalForm, from_set) { // Examples // -------- - // - (bag.from_set (emptyset String)) = (emptybag String) - // - (bag.from_set (singleton "x")) = (mkBag "x" 1) - // - (bag.to_set (union (singleton "x") (singleton "y"))) = - // (disjoint_union (mkBag "x" 1) (mkBag "y" 1)) + // - (bag.from_set (as set.empty (Bag String))) = (as bag.empty (Bag String)) + // - (bag.from_set (set.singleton "x")) = (bag "x" 1) + // - (bag.from_set (set.union (set.singleton "x") (set.singleton "y"))) = + // (bag.union_disjoint (bag "x" 1) (bag "y" 1)) Node emptyset = d_nodeManager->mkConst( EmptySet(d_nodeManager->mkSetType(d_nodeManager->stringType()))); @@ -602,7 +607,7 @@ TEST_F(TestTheoryWhiteBagsNormalForm, from_set) // for normal sets, the first node is the largest, not smallest Node normalSet = d_nodeManager->mkNode(SET_UNION, ySingleton, xSingleton); Node input3 = d_nodeManager->mkNode(BAG_FROM_SET, normalSet); - Node output3 = d_nodeManager->mkNode(UNION_DISJOINT, x_1, y_1); + Node output3 = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_1, y_1); ASSERT_EQ(output3, NormalForm::evaluate(input3)); } @@ -610,10 +615,10 @@ TEST_F(TestTheoryWhiteBagsNormalForm, to_set) { // Examples // -------- - // - (bag.to_set (emptybag String)) = (emptyset String) - // - (bag.to_set (mkBag "x" 4)) = (singleton "x") - // - (bag.to_set (disjoint_union (mkBag "x" 3) (mkBag "y" 5)) = - // (union (singleton "x") (singleton "y"))) + // - (bag.to_set (as bag.empty (Bag String))) = (as set.empty (Bag String)) + // - (bag.to_set (bag "x" 4)) = (set.singleton "x") + // - (bag.to_set (bag.union_disjoint(bag "x" 3) (bag "y" 5)) = + // (set.union (set.singleton "x") (set.singleton "y"))) Node emptyset = d_nodeManager->mkConst( EmptySet(d_nodeManager->mkSetType(d_nodeManager->stringType()))); @@ -643,7 +648,7 @@ TEST_F(TestTheoryWhiteBagsNormalForm, to_set) ASSERT_EQ(output2, NormalForm::evaluate(input2)); // for normal sets, the first node is the largest, not smallest - Node normalBag = d_nodeManager->mkNode(UNION_DISJOINT, x_4, y_5); + Node normalBag = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_4, y_5); Node input3 = d_nodeManager->mkNode(BAG_TO_SET, normalBag); Node output3 = d_nodeManager->mkNode(SET_UNION, ySingleton, xSingleton); ASSERT_EQ(output3, NormalForm::evaluate(input3)); diff --git a/test/unit/theory/theory_bags_rewriter_white.cpp b/test/unit/theory/theory_bags_rewriter_white.cpp index 639de0a66..ca142c6b9 100644 --- a/test/unit/theory/theory_bags_rewriter_white.cpp +++ b/test/unit/theory/theory_bags_rewriter_white.cpp @@ -183,13 +183,13 @@ TEST_F(TestTheoryWhiteBagsRewriter, bag_count) Node emptyBag = d_nodeManager->mkConst( EmptyBag(d_nodeManager->mkBagType(skolem.getType()))); - // (bag.count x emptybag) = 0 + // (bag.count x (as bag.empty (Bag String))) = 0 Node n1 = d_nodeManager->mkNode(BAG_COUNT, skolem, emptyBag); RewriteResponse response1 = d_rewriter->postRewrite(n1); ASSERT_TRUE(response1.d_status == REWRITE_AGAIN_FULL && response1.d_node == zero); - // (bag.count x (mkBag x c) = (ite (>= c 1) c 0) + // (bag.count x (bag x c) = (ite (>= c 1) c 0) Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), skolem, three); Node n2 = d_nodeManager->mkNode(BAG_COUNT, skolem, bag); RewriteResponse response2 = d_rewriter->postRewrite(n2); @@ -208,8 +208,8 @@ TEST_F(TestTheoryWhiteBagsRewriter, duplicate_removal) x, d_nodeManager->mkConst(CONST_RATIONAL, Rational(5))); - // (duplicate_removal (mkBag x n)) = (mkBag x 1) - Node n = d_nodeManager->mkNode(DUPLICATE_REMOVAL, bag); + // (bag.duplicate_removal (bag x n)) = (bag x 1) + Node n = d_nodeManager->mkNode(BAG_DUPLICATE_REMOVAL, bag); RewriteResponse response = d_rewriter->postRewrite(n); Node noDuplicate = d_nodeManager->mkBag(d_nodeManager->stringType(), @@ -233,73 +233,73 @@ TEST_F(TestTheoryWhiteBagsRewriter, union_max) d_nodeManager->stringType(), elements[1], d_nodeManager->mkConst(CONST_RATIONAL, Rational(n + 1))); - Node unionMaxAB = d_nodeManager->mkNode(UNION_MAX, A, B); - Node unionMaxBA = d_nodeManager->mkNode(UNION_MAX, B, A); - Node unionDisjointAB = d_nodeManager->mkNode(UNION_DISJOINT, A, B); - Node unionDisjointBA = d_nodeManager->mkNode(UNION_DISJOINT, B, A); + Node unionMaxAB = d_nodeManager->mkNode(BAG_UNION_MAX, A, B); + Node unionMaxBA = d_nodeManager->mkNode(BAG_UNION_MAX, B, A); + Node unionDisjointAB = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, B); + Node unionDisjointBA = d_nodeManager->mkNode(BAG_UNION_DISJOINT, B, A); - // (union_max A emptybag) = A - Node unionMax1 = d_nodeManager->mkNode(UNION_MAX, A, emptyBag); + // (bag.union_max A (as bag.empty (Bag String))) = A + Node unionMax1 = d_nodeManager->mkNode(BAG_UNION_MAX, A, emptyBag); RewriteResponse response1 = d_rewriter->postRewrite(unionMax1); ASSERT_TRUE(response1.d_node == A && response1.d_status == REWRITE_AGAIN_FULL); - // (union_max emptybag A) = A - Node unionMax2 = d_nodeManager->mkNode(UNION_MAX, emptyBag, A); + // (bag.union_max (as bag.empty (Bag String)) A) = A + Node unionMax2 = d_nodeManager->mkNode(BAG_UNION_MAX, emptyBag, A); RewriteResponse response2 = d_rewriter->postRewrite(unionMax2); ASSERT_TRUE(response2.d_node == A && response2.d_status == REWRITE_AGAIN_FULL); - // (union_max A A) = A - Node unionMax3 = d_nodeManager->mkNode(UNION_MAX, A, A); + // (bag.union_max A A) = A + Node unionMax3 = d_nodeManager->mkNode(BAG_UNION_MAX, A, A); RewriteResponse response3 = d_rewriter->postRewrite(unionMax3); ASSERT_TRUE(response3.d_node == A && response3.d_status == REWRITE_AGAIN_FULL); - // (union_max A (union_max A B)) = (union_max A B) - Node unionMax4 = d_nodeManager->mkNode(UNION_MAX, A, unionMaxAB); + // (bag.union_max A (bag.union_max A B)) = (bag.union_max A B) + Node unionMax4 = d_nodeManager->mkNode(BAG_UNION_MAX, A, unionMaxAB); RewriteResponse response4 = d_rewriter->postRewrite(unionMax4); ASSERT_TRUE(response4.d_node == unionMaxAB && response4.d_status == REWRITE_AGAIN_FULL); - // (union_max A (union_max B A)) = (union_max B A) - Node unionMax5 = d_nodeManager->mkNode(UNION_MAX, A, unionMaxBA); + // (bag.union_max A (bag.union_max B A)) = (bag.union_max B A) + Node unionMax5 = d_nodeManager->mkNode(BAG_UNION_MAX, A, unionMaxBA); RewriteResponse response5 = d_rewriter->postRewrite(unionMax5); ASSERT_TRUE(response5.d_node == unionMaxBA && response4.d_status == REWRITE_AGAIN_FULL); - // (union_max (union_max A B) A) = (union_max A B) - Node unionMax6 = d_nodeManager->mkNode(UNION_MAX, unionMaxAB, A); + // (bag.union_max (bag.union_max A B) A) = (bag.union_max A B) + Node unionMax6 = d_nodeManager->mkNode(BAG_UNION_MAX, unionMaxAB, A); RewriteResponse response6 = d_rewriter->postRewrite(unionMax6); ASSERT_TRUE(response6.d_node == unionMaxAB && response6.d_status == REWRITE_AGAIN_FULL); - // (union_max (union_max B A) A) = (union_max B A) - Node unionMax7 = d_nodeManager->mkNode(UNION_MAX, unionMaxBA, A); + // (bag.union_max (bag.union_max B A) A) = (bag.union_max B A) + Node unionMax7 = d_nodeManager->mkNode(BAG_UNION_MAX, unionMaxBA, A); RewriteResponse response7 = d_rewriter->postRewrite(unionMax7); ASSERT_TRUE(response7.d_node == unionMaxBA && response7.d_status == REWRITE_AGAIN_FULL); - // (union_max A (union_disjoint A B)) = (union_disjoint A B) - Node unionMax8 = d_nodeManager->mkNode(UNION_MAX, A, unionDisjointAB); + // (bag.union_max A (bag.union_disjoint A B)) = (bag.union_disjoint A B) + Node unionMax8 = d_nodeManager->mkNode(BAG_UNION_MAX, A, unionDisjointAB); RewriteResponse response8 = d_rewriter->postRewrite(unionMax8); ASSERT_TRUE(response8.d_node == unionDisjointAB && response8.d_status == REWRITE_AGAIN_FULL); - // (union_max A (union_disjoint B A)) = (union_disjoint B A) - Node unionMax9 = d_nodeManager->mkNode(UNION_MAX, A, unionDisjointBA); + // (bag.union_max A (bag.union_disjoint B A)) = (bag.union_disjoint B A) + Node unionMax9 = d_nodeManager->mkNode(BAG_UNION_MAX, A, unionDisjointBA); RewriteResponse response9 = d_rewriter->postRewrite(unionMax9); ASSERT_TRUE(response9.d_node == unionDisjointBA && response9.d_status == REWRITE_AGAIN_FULL); - // (union_max (union_disjoint A B) A) = (union_disjoint A B) - Node unionMax10 = d_nodeManager->mkNode(UNION_MAX, unionDisjointAB, A); + // (bag.union_max (bag.union_disjoint A B) A) = (bag.union_disjoint A B) + Node unionMax10 = d_nodeManager->mkNode(BAG_UNION_MAX, unionDisjointAB, A); RewriteResponse response10 = d_rewriter->postRewrite(unionMax10); ASSERT_TRUE(response10.d_node == unionDisjointAB && response10.d_status == REWRITE_AGAIN_FULL); - // (union_max (union_disjoint B A) A) = (union_disjoint B A) - Node unionMax11 = d_nodeManager->mkNode(UNION_MAX, unionDisjointBA, A); + // (bag.union_max (bag.union_disjoint B A) A) = (bag.union_disjoint B A) + Node unionMax11 = d_nodeManager->mkNode(BAG_UNION_MAX, unionDisjointBA, A); RewriteResponse response11 = d_rewriter->postRewrite(unionMax11); ASSERT_TRUE(response11.d_node == unionDisjointBA && response11.d_status == REWRITE_AGAIN_FULL); @@ -324,46 +324,46 @@ TEST_F(TestTheoryWhiteBagsRewriter, union_disjoint) elements[2], d_nodeManager->mkConst(CONST_RATIONAL, Rational(n + 2))); - Node unionDisjointAB = d_nodeManager->mkNode(UNION_DISJOINT, A, B); - Node unionDisjointBA = d_nodeManager->mkNode(UNION_DISJOINT, B, A); - Node unionMaxAB = d_nodeManager->mkNode(UNION_MAX, A, B); - Node unionMaxAC = d_nodeManager->mkNode(UNION_MAX, A, C); - Node unionMaxBA = d_nodeManager->mkNode(UNION_MAX, B, A); - Node intersectionAB = d_nodeManager->mkNode(INTERSECTION_MIN, A, B); - Node intersectionBA = d_nodeManager->mkNode(INTERSECTION_MIN, B, A); + Node unionDisjointAB = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, B); + Node unionDisjointBA = d_nodeManager->mkNode(BAG_UNION_DISJOINT, B, A); + Node unionMaxAB = d_nodeManager->mkNode(BAG_UNION_MAX, A, B); + Node unionMaxAC = d_nodeManager->mkNode(BAG_UNION_MAX, A, C); + Node unionMaxBA = d_nodeManager->mkNode(BAG_UNION_MAX, B, A); + Node intersectionAB = d_nodeManager->mkNode(BAG_INTER_MIN, A, B); + Node intersectionBA = d_nodeManager->mkNode(BAG_INTER_MIN, B, A); - // (union_disjoint A emptybag) = A - Node unionDisjoint1 = d_nodeManager->mkNode(UNION_DISJOINT, A, emptyBag); + // (bag.union_disjoint A (as bag.empty (Bag String))) = A + Node unionDisjoint1 = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, emptyBag); RewriteResponse response1 = d_rewriter->postRewrite(unionDisjoint1); ASSERT_TRUE(response1.d_node == A && response1.d_status == REWRITE_AGAIN_FULL); - // (union_disjoint emptybag A) = A - Node unionDisjoint2 = d_nodeManager->mkNode(UNION_DISJOINT, emptyBag, A); + // (bag.union_disjoint (as bag.empty (Bag String)) A) = A + Node unionDisjoint2 = d_nodeManager->mkNode(BAG_UNION_DISJOINT, emptyBag, A); RewriteResponse response2 = d_rewriter->postRewrite(unionDisjoint2); ASSERT_TRUE(response2.d_node == A && response2.d_status == REWRITE_AGAIN_FULL); - // (union_disjoint (union_max A B) (intersection_min B A)) = - // (union_disjoint A B) // sum(a,b) = max(a,b) + min(a,b) + // (bag.union_disjoint (bag.union_max A B) (bag.inter_min B A)) = + // (bag.union_disjoint A B) // sum(a,b) = max(a,b) + min(a,b) Node unionDisjoint3 = - d_nodeManager->mkNode(UNION_DISJOINT, unionMaxAB, intersectionBA); + d_nodeManager->mkNode(BAG_UNION_DISJOINT, unionMaxAB, intersectionBA); RewriteResponse response3 = d_rewriter->postRewrite(unionDisjoint3); ASSERT_TRUE(response3.d_node == unionDisjointAB && response3.d_status == REWRITE_AGAIN_FULL); - // (union_disjoint (intersection_min B A)) (union_max A B) = - // (union_disjoint B A) // sum(a,b) = max(a,b) + min(a,b) + // (bag.union_disjoint (bag.inter_min B A)) (bag.union_max A B) = + // (bag.union_disjoint B A) // sum(a,b) = max(a,b) + min(a,b) Node unionDisjoint4 = - d_nodeManager->mkNode(UNION_DISJOINT, unionMaxBA, intersectionBA); + d_nodeManager->mkNode(BAG_UNION_DISJOINT, unionMaxBA, intersectionBA); RewriteResponse response4 = d_rewriter->postRewrite(unionDisjoint4); ASSERT_TRUE(response4.d_node == unionDisjointBA && response4.d_status == REWRITE_AGAIN_FULL); - // (union_disjoint (intersection_min B A)) (union_max A B) = - // (union_disjoint B A) // sum(a,b) = max(a,b) + min(a,b) + // (bag.union_disjoint (bag.inter_min B A)) (bag.union_max A B) = + // (bag.union_disjoint B A) // sum(a,b) = max(a,b) + min(a,b) Node unionDisjoint5 = - d_nodeManager->mkNode(UNION_DISJOINT, unionMaxAC, intersectionAB); + d_nodeManager->mkNode(BAG_UNION_DISJOINT, unionMaxAC, intersectionAB); RewriteResponse response5 = d_rewriter->postRewrite(unionDisjoint5); ASSERT_TRUE(response5.d_node == unionDisjoint5 && response5.d_status == REWRITE_DONE); @@ -383,73 +383,75 @@ TEST_F(TestTheoryWhiteBagsRewriter, intersection_min) d_nodeManager->stringType(), elements[1], d_nodeManager->mkConst(CONST_RATIONAL, Rational(n + 1))); - Node unionMaxAB = d_nodeManager->mkNode(UNION_MAX, A, B); - Node unionMaxBA = d_nodeManager->mkNode(UNION_MAX, B, A); - Node unionDisjointAB = d_nodeManager->mkNode(UNION_DISJOINT, A, B); - Node unionDisjointBA = d_nodeManager->mkNode(UNION_DISJOINT, B, A); - - // (intersection_min A emptybag) = emptyBag - Node n1 = d_nodeManager->mkNode(INTERSECTION_MIN, A, emptyBag); + Node unionMaxAB = d_nodeManager->mkNode(BAG_UNION_MAX, A, B); + Node unionMaxBA = d_nodeManager->mkNode(BAG_UNION_MAX, B, A); + Node unionDisjointAB = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, B); + Node unionDisjointBA = d_nodeManager->mkNode(BAG_UNION_DISJOINT, B, A); + + // (bag.inter_min A (as bag.empty (Bag String)) = + // (as bag.empty (Bag String)) + Node n1 = d_nodeManager->mkNode(BAG_INTER_MIN, A, emptyBag); RewriteResponse response1 = d_rewriter->postRewrite(n1); ASSERT_TRUE(response1.d_node == emptyBag && response1.d_status == REWRITE_AGAIN_FULL); - // (intersection_min emptybag A) = emptyBag - Node n2 = d_nodeManager->mkNode(INTERSECTION_MIN, emptyBag, A); + // (bag.inter_min (as bag.empty (Bag String)) A) = + // (as bag.empty (Bag String)) + Node n2 = d_nodeManager->mkNode(BAG_INTER_MIN, emptyBag, A); RewriteResponse response2 = d_rewriter->postRewrite(n2); ASSERT_TRUE(response2.d_node == emptyBag && response2.d_status == REWRITE_AGAIN_FULL); - // (intersection_min A A) = A - Node n3 = d_nodeManager->mkNode(INTERSECTION_MIN, A, A); + // (bag.inter_min A A) = A + Node n3 = d_nodeManager->mkNode(BAG_INTER_MIN, A, A); RewriteResponse response3 = d_rewriter->postRewrite(n3); ASSERT_TRUE(response3.d_node == A && response3.d_status == REWRITE_AGAIN_FULL); - // (intersection_min A (union_max A B) = A - Node n4 = d_nodeManager->mkNode(INTERSECTION_MIN, A, unionMaxAB); + // (bag.inter_min A (bag.union_max A B) = A + Node n4 = d_nodeManager->mkNode(BAG_INTER_MIN, A, unionMaxAB); RewriteResponse response4 = d_rewriter->postRewrite(n4); ASSERT_TRUE(response4.d_node == A && response4.d_status == REWRITE_AGAIN_FULL); - // (intersection_min A (union_max B A) = A - Node n5 = d_nodeManager->mkNode(INTERSECTION_MIN, A, unionMaxBA); + // (bag.inter_min A (bag.union_max B A) = A + Node n5 = d_nodeManager->mkNode(BAG_INTER_MIN, A, unionMaxBA); RewriteResponse response5 = d_rewriter->postRewrite(n5); ASSERT_TRUE(response5.d_node == A && response4.d_status == REWRITE_AGAIN_FULL); - // (intersection_min (union_max A B) A) = A - Node n6 = d_nodeManager->mkNode(INTERSECTION_MIN, unionMaxAB, A); + // (bag.inter_min (bag.union_max A B) A) = A + Node n6 = d_nodeManager->mkNode(BAG_INTER_MIN, unionMaxAB, A); RewriteResponse response6 = d_rewriter->postRewrite(n6); ASSERT_TRUE(response6.d_node == A && response6.d_status == REWRITE_AGAIN_FULL); - // (intersection_min (union_max B A) A) = A - Node n7 = d_nodeManager->mkNode(INTERSECTION_MIN, unionMaxBA, A); + // (bag.inter_min (bag.union_max B A) A) = A + Node n7 = d_nodeManager->mkNode(BAG_INTER_MIN, unionMaxBA, A); RewriteResponse response7 = d_rewriter->postRewrite(n7); ASSERT_TRUE(response7.d_node == A && response7.d_status == REWRITE_AGAIN_FULL); - // (intersection_min A (union_disjoint A B) = A - Node n8 = d_nodeManager->mkNode(INTERSECTION_MIN, A, unionDisjointAB); + // (bag.inter_min A (bag.union_disjoint A B) = A + Node n8 = d_nodeManager->mkNode(BAG_INTER_MIN, A, unionDisjointAB); RewriteResponse response8 = d_rewriter->postRewrite(n8); ASSERT_TRUE(response8.d_node == A && response8.d_status == REWRITE_AGAIN_FULL); - // (intersection_min A (union_disjoint B A) = A - Node n9 = d_nodeManager->mkNode(INTERSECTION_MIN, A, unionDisjointBA); + // (bag.inter_min A (bag.union_disjoint B A) = A + Node n9 = d_nodeManager->mkNode(BAG_INTER_MIN, A, unionDisjointBA); RewriteResponse response9 = d_rewriter->postRewrite(n9); ASSERT_TRUE(response9.d_node == A && response9.d_status == REWRITE_AGAIN_FULL); - // (intersection_min (union_disjoint A B) A) = A - Node n10 = d_nodeManager->mkNode(INTERSECTION_MIN, unionDisjointAB, A); + // (bag.inter_min (bag.union_disjoint A B) A) = A + Node n10 = d_nodeManager->mkNode(BAG_INTER_MIN, unionDisjointAB, A); RewriteResponse response10 = d_rewriter->postRewrite(n10); ASSERT_TRUE(response10.d_node == A && response10.d_status == REWRITE_AGAIN_FULL); - // (intersection_min (union_disjoint B A) A) = A - Node n11 = d_nodeManager->mkNode(INTERSECTION_MIN, unionDisjointBA, A); + // (bag.inter_min (bag.union_disjoint B A) A) = A + Node n11 = d_nodeManager->mkNode(BAG_INTER_MIN, unionDisjointBA, A); RewriteResponse response11 = d_rewriter->postRewrite(n11); ASSERT_TRUE(response11.d_node == A && response11.d_status == REWRITE_AGAIN_FULL); @@ -469,75 +471,82 @@ TEST_F(TestTheoryWhiteBagsRewriter, difference_subtract) d_nodeManager->stringType(), elements[1], d_nodeManager->mkConst(CONST_RATIONAL, Rational(n + 1))); - Node unionMaxAB = d_nodeManager->mkNode(UNION_MAX, A, B); - Node unionMaxBA = d_nodeManager->mkNode(UNION_MAX, B, A); - Node unionDisjointAB = d_nodeManager->mkNode(UNION_DISJOINT, A, B); - Node unionDisjointBA = d_nodeManager->mkNode(UNION_DISJOINT, B, A); - Node intersectionAB = d_nodeManager->mkNode(INTERSECTION_MIN, A, B); - Node intersectionBA = d_nodeManager->mkNode(INTERSECTION_MIN, B, A); - - // (difference_subtract A emptybag) = A - Node n1 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, A, emptyBag); + Node unionMaxAB = d_nodeManager->mkNode(BAG_UNION_MAX, A, B); + Node unionMaxBA = d_nodeManager->mkNode(BAG_UNION_MAX, B, A); + Node unionDisjointAB = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, B); + Node unionDisjointBA = d_nodeManager->mkNode(BAG_UNION_DISJOINT, B, A); + Node intersectionAB = d_nodeManager->mkNode(BAG_INTER_MIN, A, B); + Node intersectionBA = d_nodeManager->mkNode(BAG_INTER_MIN, B, A); + + // (bag.difference_subtract A (as bag.empty (Bag String)) = A + Node n1 = d_nodeManager->mkNode(BAG_DIFFERENCE_SUBTRACT, A, emptyBag); RewriteResponse response1 = d_rewriter->postRewrite(n1); ASSERT_TRUE(response1.d_node == A && response1.d_status == REWRITE_AGAIN_FULL); - // (difference_subtract emptybag A) = emptyBag - Node n2 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, emptyBag, A); + // (bag.difference_subtract (as bag.empty (Bag String)) A) = + // (as bag.empty (Bag String)) + Node n2 = d_nodeManager->mkNode(BAG_DIFFERENCE_SUBTRACT, emptyBag, A); RewriteResponse response2 = d_rewriter->postRewrite(n2); ASSERT_TRUE(response2.d_node == emptyBag && response2.d_status == REWRITE_AGAIN_FULL); - // (difference_subtract A A) = emptybag - Node n3 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, A, A); + // (bag.difference_subtract A A) = (as bag.empty (Bag String)) + Node n3 = d_nodeManager->mkNode(BAG_DIFFERENCE_SUBTRACT, A, A); RewriteResponse response3 = d_rewriter->postRewrite(n3); ASSERT_TRUE(response3.d_node == emptyBag && response3.d_status == REWRITE_AGAIN_FULL); - // (difference_subtract (union_disjoint A B) A) = B - Node n4 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, unionDisjointAB, A); + // (bag.difference_subtract (bag.union_disjoint A B) A) = B + Node n4 = d_nodeManager->mkNode(BAG_DIFFERENCE_SUBTRACT, unionDisjointAB, A); RewriteResponse response4 = d_rewriter->postRewrite(n4); ASSERT_TRUE(response4.d_node == B && response4.d_status == REWRITE_AGAIN_FULL); - // (difference_subtract (union_disjoint B A) A) = B - Node n5 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, unionDisjointBA, A); + // (bag.difference_subtract (bag.union_disjoint B A) A) = B + Node n5 = d_nodeManager->mkNode(BAG_DIFFERENCE_SUBTRACT, unionDisjointBA, A); RewriteResponse response5 = d_rewriter->postRewrite(n5); ASSERT_TRUE(response5.d_node == B && response4.d_status == REWRITE_AGAIN_FULL); - // (difference_subtract A (union_disjoint A B)) = emptybag - Node n6 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, A, unionDisjointAB); + // (bag.difference_subtract A (bag.union_disjoint A B)) = + // (as bag.empty (Bag String)) + Node n6 = d_nodeManager->mkNode(BAG_DIFFERENCE_SUBTRACT, A, unionDisjointAB); RewriteResponse response6 = d_rewriter->postRewrite(n6); ASSERT_TRUE(response6.d_node == emptyBag && response6.d_status == REWRITE_AGAIN_FULL); - // (difference_subtract A (union_disjoint B A)) = emptybag - Node n7 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, A, unionDisjointBA); + // (bag.difference_subtract A (bag.union_disjoint B A)) = + // (as bag.empty (Bag String)) + Node n7 = d_nodeManager->mkNode(BAG_DIFFERENCE_SUBTRACT, A, unionDisjointBA); RewriteResponse response7 = d_rewriter->postRewrite(n7); ASSERT_TRUE(response7.d_node == emptyBag && response7.d_status == REWRITE_AGAIN_FULL); - // (difference_subtract A (union_max A B)) = emptybag - Node n8 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, A, unionMaxAB); + // (bag.difference_subtract A (bag.union_max A B)) = + // (as bag.empty (Bag String)) + Node n8 = d_nodeManager->mkNode(BAG_DIFFERENCE_SUBTRACT, A, unionMaxAB); RewriteResponse response8 = d_rewriter->postRewrite(n8); ASSERT_TRUE(response8.d_node == emptyBag && response8.d_status == REWRITE_AGAIN_FULL); - // (difference_subtract A (union_max B A)) = emptybag - Node n9 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, A, unionMaxBA); + // (bag.difference_subtract A (bag.union_max B A)) = + // (as bag.empty (Bag String)) + Node n9 = d_nodeManager->mkNode(BAG_DIFFERENCE_SUBTRACT, A, unionMaxBA); RewriteResponse response9 = d_rewriter->postRewrite(n9); ASSERT_TRUE(response9.d_node == emptyBag && response9.d_status == REWRITE_AGAIN_FULL); - // (difference_subtract (intersection_min A B) A) = emptybag - Node n10 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, intersectionAB, A); + // (bag.difference_subtract (bag.inter_min A B) A) = + // (as bag.empty (Bag String)) + Node n10 = d_nodeManager->mkNode(BAG_DIFFERENCE_SUBTRACT, intersectionAB, A); RewriteResponse response10 = d_rewriter->postRewrite(n10); ASSERT_TRUE(response10.d_node == emptyBag && response10.d_status == REWRITE_AGAIN_FULL); - // (difference_subtract (intersection_min B A) A) = emptybag - Node n11 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, intersectionBA, A); + // (bag.difference_subtract (bag.inter_min B A) A) = + // (as bag.empty (Bag String)) + Node n11 = d_nodeManager->mkNode(BAG_DIFFERENCE_SUBTRACT, intersectionBA, A); RewriteResponse response11 = d_rewriter->postRewrite(n11); ASSERT_TRUE(response11.d_node == emptyBag && response11.d_status == REWRITE_AGAIN_FULL); @@ -557,63 +566,70 @@ TEST_F(TestTheoryWhiteBagsRewriter, difference_remove) d_nodeManager->stringType(), elements[1], d_nodeManager->mkConst(CONST_RATIONAL, Rational(n + 1))); - Node unionMaxAB = d_nodeManager->mkNode(UNION_MAX, A, B); - Node unionMaxBA = d_nodeManager->mkNode(UNION_MAX, B, A); - Node unionDisjointAB = d_nodeManager->mkNode(UNION_DISJOINT, A, B); - Node unionDisjointBA = d_nodeManager->mkNode(UNION_DISJOINT, B, A); - Node intersectionAB = d_nodeManager->mkNode(INTERSECTION_MIN, A, B); - Node intersectionBA = d_nodeManager->mkNode(INTERSECTION_MIN, B, A); - - // (difference_remove A emptybag) = A - Node n1 = d_nodeManager->mkNode(DIFFERENCE_REMOVE, A, emptyBag); + Node unionMaxAB = d_nodeManager->mkNode(BAG_UNION_MAX, A, B); + Node unionMaxBA = d_nodeManager->mkNode(BAG_UNION_MAX, B, A); + Node unionDisjointAB = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, B); + Node unionDisjointBA = d_nodeManager->mkNode(BAG_UNION_DISJOINT, B, A); + Node intersectionAB = d_nodeManager->mkNode(BAG_INTER_MIN, A, B); + Node intersectionBA = d_nodeManager->mkNode(BAG_INTER_MIN, B, A); + + // (bag.difference_remove A (as bag.empty (Bag String)) = A + Node n1 = d_nodeManager->mkNode(BAG_DIFFERENCE_REMOVE, A, emptyBag); RewriteResponse response1 = d_rewriter->postRewrite(n1); ASSERT_TRUE(response1.d_node == A && response1.d_status == REWRITE_AGAIN_FULL); - // (difference_remove emptybag A) = emptyBag - Node n2 = d_nodeManager->mkNode(DIFFERENCE_REMOVE, emptyBag, A); + // (bag.difference_remove (as bag.empty (Bag String)) A)= + // (as bag.empty (Bag String)) + Node n2 = d_nodeManager->mkNode(BAG_DIFFERENCE_REMOVE, emptyBag, A); RewriteResponse response2 = d_rewriter->postRewrite(n2); ASSERT_TRUE(response2.d_node == emptyBag && response2.d_status == REWRITE_AGAIN_FULL); - // (difference_remove A A) = emptybag - Node n3 = d_nodeManager->mkNode(DIFFERENCE_REMOVE, A, A); + // (bag.difference_remove A A) = (as bag.empty (Bag String)) + Node n3 = d_nodeManager->mkNode(BAG_DIFFERENCE_REMOVE, A, A); RewriteResponse response3 = d_rewriter->postRewrite(n3); ASSERT_TRUE(response3.d_node == emptyBag && response3.d_status == REWRITE_AGAIN_FULL); - // (difference_remove A (union_disjoint A B)) = emptybag - Node n6 = d_nodeManager->mkNode(DIFFERENCE_REMOVE, A, unionDisjointAB); + // (bag.difference_remove A (bag.union_disjoint A B)) = + // (as bag.empty (Bag String)) + Node n6 = d_nodeManager->mkNode(BAG_DIFFERENCE_REMOVE, A, unionDisjointAB); RewriteResponse response6 = d_rewriter->postRewrite(n6); ASSERT_TRUE(response6.d_node == emptyBag && response6.d_status == REWRITE_AGAIN_FULL); - // (difference_remove A (union_disjoint B A)) = emptybag - Node n7 = d_nodeManager->mkNode(DIFFERENCE_REMOVE, A, unionDisjointBA); + // (bag.difference_remove A (bag.union_disjoint B A)) = + // (as bag.empty (Bag String)) + Node n7 = d_nodeManager->mkNode(BAG_DIFFERENCE_REMOVE, A, unionDisjointBA); RewriteResponse response7 = d_rewriter->postRewrite(n7); ASSERT_TRUE(response7.d_node == emptyBag && response7.d_status == REWRITE_AGAIN_FULL); - // (difference_remove A (union_max A B)) = emptybag - Node n8 = d_nodeManager->mkNode(DIFFERENCE_REMOVE, A, unionMaxAB); + // (bag.difference_remove A (bag.union_max A B)) = + // (as bag.empty (Bag String)) + Node n8 = d_nodeManager->mkNode(BAG_DIFFERENCE_REMOVE, A, unionMaxAB); RewriteResponse response8 = d_rewriter->postRewrite(n8); ASSERT_TRUE(response8.d_node == emptyBag && response8.d_status == REWRITE_AGAIN_FULL); - // (difference_remove A (union_max B A)) = emptybag - Node n9 = d_nodeManager->mkNode(DIFFERENCE_REMOVE, A, unionMaxBA); + // (bag.difference_remove A (bag.union_max B A)) = + // (as bag.empty (Bag String)) + Node n9 = d_nodeManager->mkNode(BAG_DIFFERENCE_REMOVE, A, unionMaxBA); RewriteResponse response9 = d_rewriter->postRewrite(n9); ASSERT_TRUE(response9.d_node == emptyBag && response9.d_status == REWRITE_AGAIN_FULL); - // (difference_remove (intersection_min A B) A) = emptybag - Node n10 = d_nodeManager->mkNode(DIFFERENCE_REMOVE, intersectionAB, A); + // (bag.difference_remove (bag.inter_min A B) A) = + // (as bag.empty (Bag String)) + Node n10 = d_nodeManager->mkNode(BAG_DIFFERENCE_REMOVE, intersectionAB, A); RewriteResponse response10 = d_rewriter->postRewrite(n10); ASSERT_TRUE(response10.d_node == emptyBag && response10.d_status == REWRITE_AGAIN_FULL); - // (difference_remove (intersection_min B A) A) = emptybag - Node n11 = d_nodeManager->mkNode(DIFFERENCE_REMOVE, intersectionBA, A); + // (bag.difference_remove (bag.inter_min B A) A) = + // (as bag.empty (Bag String)) + Node n11 = d_nodeManager->mkNode(BAG_DIFFERENCE_REMOVE, intersectionBA, A); RewriteResponse response11 = d_rewriter->postRewrite(n11); ASSERT_TRUE(response11.d_node == emptyBag && response11.d_status == REWRITE_AGAIN_FULL); @@ -625,7 +641,7 @@ TEST_F(TestTheoryWhiteBagsRewriter, choose) Node c = d_nodeManager->mkConst(CONST_RATIONAL, Rational(3)); Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), x, c); - // (bag.choose (mkBag x c)) = x where c is a constant > 0 + // (bag.choose (bag x c)) = x where c is a constant > 0 Node n1 = d_nodeManager->mkNode(BAG_CHOOSE, bag); RewriteResponse response1 = d_rewriter->postRewrite(n1); ASSERT_TRUE(response1.d_node == x @@ -649,22 +665,21 @@ TEST_F(TestTheoryWhiteBagsRewriter, bag_card) d_nodeManager->mkBag(d_nodeManager->stringType(), elements[1], d_nodeManager->mkConst(CONST_RATIONAL, Rational(5))); - Node unionDisjointAB = d_nodeManager->mkNode(UNION_DISJOINT, A, B); + Node unionDisjointAB = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, B); - // TODO(projects#223): enable this test after implementing bags normal form - // // (bag.card emptybag) = 0 - // Node n1 = d_nodeManager->mkNode(BAG_CARD, emptyBag); - // RewriteResponse response1 = d_rewriter->postRewrite(n1); - // ASSERT_TRUE(response1.d_node == zero && response1.d_status == - // REWRITE_AGAIN_FULL); + // (bag.card (as bag.empty (Bag String)) = 0 + Node n1 = d_nodeManager->mkNode(BAG_CARD, emptyBag); + RewriteResponse response1 = d_rewriter->postRewrite(n1); + ASSERT_TRUE(response1.d_node == zero + && response1.d_status == REWRITE_AGAIN_FULL); - // (bag.card (mkBag x c)) = c where c is a constant > 0 + // (bag.card (bag x c)) = c where c is a constant > 0 Node n2 = d_nodeManager->mkNode(BAG_CARD, bag); RewriteResponse response2 = d_rewriter->postRewrite(n2); ASSERT_TRUE(response2.d_node == c && response2.d_status == REWRITE_AGAIN_FULL); - // (bag.card (union-disjoint A B)) = (+ (bag.card A) (bag.card B)) + // (bag.card (bag.union_disjoint A B)) = (+ (bag.card A) (bag.card B)) Node n3 = d_nodeManager->mkNode(BAG_CARD, unionDisjointAB); Node cardA = d_nodeManager->mkNode(BAG_CARD, A); Node cardB = d_nodeManager->mkNode(BAG_CARD, B); @@ -682,14 +697,13 @@ TEST_F(TestTheoryWhiteBagsRewriter, is_singleton) Node c = d_skolemManager->mkDummySkolem("c", d_nodeManager->integerType()); Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), x, c); - // TODO(projects#223): complete this function - // (bag.is_singleton emptybag) = false - // Node n1 = d_nodeManager->mkNode(BAG_IS_SINGLETON, emptybag); - // RewriteResponse response1 = d_rewriter->postRewrite(n1); - // ASSERT_TRUE(response1.d_node == d_nodeManager->mkConst(false) - // && response1.d_status == REWRITE_AGAIN_FULL); + // (bag.is_singleton (as bag.empty (Bag String)) = false + Node n1 = d_nodeManager->mkNode(BAG_IS_SINGLETON, emptybag); + RewriteResponse response1 = d_rewriter->postRewrite(n1); + ASSERT_TRUE(response1.d_node == d_nodeManager->mkConst(false) + && response1.d_status == REWRITE_AGAIN_FULL); - // (bag.is_singleton (mkBag x c) = (c == 1) + // (bag.is_singleton (bag x c) = (c == 1) Node n2 = d_nodeManager->mkNode(BAG_IS_SINGLETON, bag); RewriteResponse response2 = d_rewriter->postRewrite(n2); Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)); @@ -703,7 +717,7 @@ TEST_F(TestTheoryWhiteBagsRewriter, from_set) Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType()); Node singleton = d_nodeManager->mkSingleton(d_nodeManager->stringType(), x); - // (bag.from_set (singleton (singleton_op Int) x)) = (mkBag x 1) + // (bag.from_set (set.singleton (set.singleton_op Int) x)) = (bag x 1) Node n = d_nodeManager->mkNode(BAG_FROM_SET, singleton); RewriteResponse response = d_rewriter->postRewrite(n); Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)); @@ -720,7 +734,7 @@ TEST_F(TestTheoryWhiteBagsRewriter, to_set) x, d_nodeManager->mkConst(CONST_RATIONAL, Rational(5))); - // (bag.to_set (mkBag x n)) = (singleton (singleton_op T) x) + // (bag.to_set (bag x n)) = (set.singleton (set.singleton_op T) x) Node n = d_nodeManager->mkNode(BAG_TO_SET, bag); RewriteResponse response = d_rewriter->postRewrite(n); Node singleton = d_nodeManager->mkSingleton(d_nodeManager->stringType(), x); @@ -739,7 +753,8 @@ TEST_F(TestTheoryWhiteBagsRewriter, map) Node bound = d_nodeManager->mkNode(kind::BOUND_VAR_LIST, xString); Node lambda = d_nodeManager->mkNode(LAMBDA, bound, empty); - // (bag.map (lambda ((x U)) t) emptybag) = emptybag + // (bag.map (lambda ((x U)) t) (as bag.empty (Bag String)) = + // (as bag.empty (Bag String)) Node n1 = d_nodeManager->mkNode(BAG_MAP, lambda, emptybagString); RewriteResponse response1 = d_rewriter->postRewrite(n1); ASSERT_TRUE(response1.d_node == emptybagString @@ -756,14 +771,15 @@ TEST_F(TestTheoryWhiteBagsRewriter, map) d_nodeManager->mkBag(d_nodeManager->stringType(), b, d_nodeManager->mkConst(CONST_RATIONAL, Rational(4))); - Node unionDisjointAB = d_nodeManager->mkNode(UNION_DISJOINT, A, B); + Node unionDisjointAB = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, B); ASSERT_TRUE(unionDisjointAB.isConst()); - // (bag.map (lambda ((x Int)) "") (union_disjoint (bag "a" 3) (bag "b" 4))) = - // (bag "" 7)) + // (bag.map + // (lambda ((x Int)) "") + // (bag.union_disjoint (bag "a" 3) (bag "b" 4))) = + // (bag "" 7)) Node n2 = d_nodeManager->mkNode(BAG_MAP, lambda, unionDisjointAB); - Node rewritten = Rewriter::rewrite(n2); Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), diff --git a/test/unit/theory/theory_bags_type_rules_white.cpp b/test/unit/theory/theory_bags_type_rules_white.cpp index b516685af..7b5b3be2c 100644 --- a/test/unit/theory/theory_bags_type_rules_white.cpp +++ b/test/unit/theory/theory_bags_type_rules_white.cpp @@ -71,8 +71,8 @@ TEST_F(TestTheoryWhiteBagsTypeRule, duplicate_removal_operator) d_nodeManager->stringType(), elements[0], d_nodeManager->mkConst(CONST_RATIONAL, Rational(10))); - ASSERT_NO_THROW(d_nodeManager->mkNode(DUPLICATE_REMOVAL, bag)); - ASSERT_EQ(d_nodeManager->mkNode(DUPLICATE_REMOVAL, bag).getType(), + ASSERT_NO_THROW(d_nodeManager->mkNode(BAG_DUPLICATE_REMOVAL, bag)); + ASSERT_EQ(d_nodeManager->mkNode(BAG_DUPLICATE_REMOVAL, bag).getType(), bag.getType()); } @@ -93,9 +93,9 @@ TEST_F(TestTheoryWhiteBagsTypeRule, mkBag_operator) d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))); // only positive multiplicity are constants - ASSERT_FALSE(MkBagTypeRule::computeIsConst(d_nodeManager, negative)); - ASSERT_FALSE(MkBagTypeRule::computeIsConst(d_nodeManager, zero)); - ASSERT_TRUE(MkBagTypeRule::computeIsConst(d_nodeManager, positive)); + ASSERT_FALSE(BagMakeTypeRule::computeIsConst(d_nodeManager, negative)); + ASSERT_FALSE(BagMakeTypeRule::computeIsConst(d_nodeManager, zero)); + ASSERT_TRUE(BagMakeTypeRule::computeIsConst(d_nodeManager, positive)); } TEST_F(TestTheoryWhiteBagsTypeRule, from_set_operator) |