diff options
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/CMakeLists.txt | 2 | ||||
-rw-r--r-- | test/regress/regress1/bags/fuzzy4.smt2 | 15 | ||||
-rw-r--r-- | test/regress/regress1/bags/fuzzy5.smt2 | 21 | ||||
-rw-r--r-- | test/unit/theory/theory_bags_rewriter_white.cpp | 28 |
4 files changed, 53 insertions, 13 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 3f099cf67..5d1ff9b49 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1591,6 +1591,8 @@ set(regress_1_tests regress1/bags/fuzzy1.smt2 regress1/bags/fuzzy2.smt2 regress1/bags/fuzzy3.smt2 + regress1/bags/fuzzy4.smt2 + regress1/bags/fuzzy5.smt2 regress1/bags/intersection_min1.smt2 regress1/bags/intersection_min2.smt2 regress1/bags/issue5759.smt2 diff --git a/test/regress/regress1/bags/fuzzy4.smt2 b/test/regress/regress1/bags/fuzzy4.smt2 new file mode 100644 index 000000000..b733a4862 --- /dev/null +++ b/test/regress/regress1/bags/fuzzy4.smt2 @@ -0,0 +1,15 @@ +(set-logic ALL) +(set-option :produce-models true) +(set-info :status sat) +(declare-fun A () (Bag (Tuple Int Int))) +(declare-fun c () Int) +(declare-fun d () (Tuple Int Int)) +(assert + (not + (= + (= A (bag d (+ c (bag.count d (union_disjoint A A))))) + (= A (difference_remove (bag d c) A))))) +(assert (= A (bag (tuple 0 0) 5))) +(assert (= c (- 5))) +(assert (= d (tuple 0 0))) +(check-sat) diff --git a/test/regress/regress1/bags/fuzzy5.smt2 b/test/regress/regress1/bags/fuzzy5.smt2 new file mode 100644 index 000000000..2dea236a5 --- /dev/null +++ b/test/regress/regress1/bags/fuzzy5.smt2 @@ -0,0 +1,21 @@ +(set-logic ALL) +(set-option :produce-models true) +(set-info :status sat) +(declare-fun A () (Bag (Tuple Int Int))) +(declare-fun c () Int) +(declare-fun d () (Tuple Int Int)) + +(assert + (let ((c_plus_1 (+ c 1))) + (and + (not + (= (= A (bag (tuple 0 c) (+ c c))) + (= A (difference_remove (bag d c) A)))) + (not + (= (= A (bag (tuple 0 1) c_plus_1)) + (= A (bag (tuple c 1) c_plus_1))))))) + +;(assert (= A (bag (tuple 0 1) 2))) +;(assert (= c 1)) +;(assert (= d (tuple 0 1))) +(check-sat)
\ No newline at end of file diff --git a/test/unit/theory/theory_bags_rewriter_white.cpp b/test/unit/theory/theory_bags_rewriter_white.cpp index 025d5aec7..7250f581c 100644 --- a/test/unit/theory/theory_bags_rewriter_white.cpp +++ b/test/unit/theory/theory_bags_rewriter_white.cpp @@ -165,25 +165,29 @@ TEST_F(TestTheoryWhiteBagsRewriter, mkBag_variable_element) TEST_F(TestTheoryWhiteBagsRewriter, bag_count) { - int n = 3; + Node zero = d_nodeManager->mkConst(Rational(0)); + Node one = d_nodeManager->mkConst(Rational(1)); + Node three = d_nodeManager->mkConst(Rational(3)); Node skolem = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType()); Node emptyBag = d_nodeManager->mkConst( EmptyBag(d_nodeManager->mkBagType(skolem.getType()))); - Node bag = d_nodeManager->mkBag( - d_nodeManager->stringType(), skolem, d_nodeManager->mkConst(Rational(n))); // (bag.count x emptybag) = 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 == d_nodeManager->mkConst(Rational(0))); + && response1.d_node == zero); - // (bag.count x (mkBag x c) = c where c > 0 is a constant + // (bag.count x (mkBag 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); + + Node geq = d_nodeManager->mkNode(GEQ, three, one); + Node ite = d_nodeManager->mkNode(ITE, geq, three, zero); ASSERT_TRUE(response2.d_status == REWRITE_AGAIN_FULL - && response2.d_node == d_nodeManager->mkConst(Rational(n))); + && response2.d_node == ite); } TEST_F(TestTheoryWhiteBagsRewriter, duplicate_removal) @@ -715,12 +719,10 @@ TEST_F(TestTheoryWhiteBagsRewriter, map) std::vector<Node> elements = getNStrings(2); Node a = d_nodeManager->mkConst(String("a")); Node b = d_nodeManager->mkConst(String("b")); - Node A = d_nodeManager->mkBag(d_nodeManager->stringType(), - a, - d_nodeManager->mkConst(Rational(3))); - Node B = d_nodeManager->mkBag(d_nodeManager->stringType(), - b, - d_nodeManager->mkConst(Rational(4))); + Node A = d_nodeManager->mkBag( + d_nodeManager->stringType(), a, d_nodeManager->mkConst(Rational(3))); + Node B = d_nodeManager->mkBag( + d_nodeManager->stringType(), b, d_nodeManager->mkConst(Rational(4))); Node unionDisjointAB = d_nodeManager->mkNode(UNION_DISJOINT, A, B); ASSERT_TRUE(unionDisjointAB.isConst()); @@ -729,7 +731,7 @@ TEST_F(TestTheoryWhiteBagsRewriter, map) // (bag "" 7)) Node n2 = d_nodeManager->mkNode(BAG_MAP, lambda, unionDisjointAB); - Node rewritten = Rewriter:: rewrite(n2); + Node rewritten = Rewriter::rewrite(n2); Node bag = d_nodeManager->mkBag( d_nodeManager->stringType(), empty, d_nodeManager->mkConst(Rational(7))); ASSERT_TRUE(rewritten == bag); |