diff options
Diffstat (limited to 'test')
-rw-r--r-- | test/unit/theory/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/unit/theory/theory_bags_normal_form_white.h | 512 | ||||
-rw-r--r-- | test/unit/theory/theory_bags_type_rules_white.h | 7 |
3 files changed, 520 insertions, 0 deletions
diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt index 481c80f26..8cfd43989 100644 --- a/test/unit/theory/CMakeLists.txt +++ b/test/unit/theory/CMakeLists.txt @@ -14,6 +14,7 @@ cvc4_add_unit_test_white(evaluator_white theory) cvc4_add_unit_test_white(logic_info_white theory) cvc4_add_unit_test_white(sequences_rewriter_white theory) cvc4_add_unit_test_white(theory_arith_white theory) +cvc4_add_unit_test_white(theory_bags_normal_form_white theory) cvc4_add_unit_test_white(theory_bags_rewriter_white theory) cvc4_add_unit_test_white(theory_bags_type_rules_white theory) cvc4_add_unit_test_white(theory_bv_rewriter_white theory) diff --git a/test/unit/theory/theory_bags_normal_form_white.h b/test/unit/theory/theory_bags_normal_form_white.h new file mode 100644 index 000000000..6f7d5bd8d --- /dev/null +++ b/test/unit/theory/theory_bags_normal_form_white.h @@ -0,0 +1,512 @@ +/********************* */ +/*! \file theory_bags_normal_form_white.h + ** \verbatim + ** Top contributors (to current version): + ** Mudathir Mohamed + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief White box testing of bags normal form + **/ + +#include <cxxtest/TestSuite.h> + +#include "expr/dtype.h" +#include "smt/smt_engine.h" +#include "theory/bags/bags_rewriter.h" +#include "theory/bags/normal_form.h" +#include "theory/strings/type_enumerator.h" + +using namespace CVC4; +using namespace CVC4::smt; +using namespace CVC4::theory; +using namespace CVC4::kind; +using namespace CVC4::theory::bags; +using namespace std; + +typedef expr::Attribute<Node, Node> attribute; + +class BagsNormalFormWhite : public CxxTest::TestSuite +{ + public: + void setUp() override + { + d_em.reset(new ExprManager()); + d_smt.reset(new SmtEngine(d_em.get())); + d_nm.reset(NodeManager::fromExprManager(d_em.get())); + d_smt->finishInit(); + d_rewriter.reset(new BagsRewriter(nullptr)); + } + + void tearDown() override + { + d_rewriter.reset(); + d_smt.reset(); + d_nm.release(); + d_em.reset(); + } + + std::vector<Node> getNStrings(size_t n) + { + std::vector<Node> elements(n); + CVC4::theory::strings::StringEnumerator enumerator(d_nm->stringType()); + + for (size_t i = 0; i < n; i++) + { + ++enumerator; + elements[i] = *enumerator; + } + + return elements; + } + + void testEmptyBagNormalForm() + { + Node emptybag = d_nm->mkConst(EmptyBag(d_nm->stringType())); + // empty bags are in normal form + TS_ASSERT(emptybag.isConst()); + Node n = NormalForm::evaluate(emptybag); + TS_ASSERT(emptybag == n); + } + + void testBagEquality() {} + + void testMkBagConstantElement() + { + vector<Node> elements = getNStrings(1); + Node negative = d_nm->mkBag( + d_nm->stringType(), elements[0], d_nm->mkConst(Rational(-1))); + Node zero = d_nm->mkBag( + d_nm->stringType(), elements[0], d_nm->mkConst(Rational(0))); + Node positive = d_nm->mkBag( + d_nm->stringType(), elements[0], d_nm->mkConst(Rational(1))); + Node emptybag = + d_nm->mkConst(EmptyBag(d_nm->mkBagType(d_nm->stringType()))); + + TS_ASSERT(!negative.isConst()); + TS_ASSERT(!zero.isConst()); + TS_ASSERT(emptybag == NormalForm::evaluate(negative)); + TS_ASSERT(emptybag == NormalForm::evaluate(zero)); + TS_ASSERT(positive == NormalForm::evaluate(positive)); + } + + void testBagCount() + { + // 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 + + Node zero = d_nm->mkConst(Rational(0)); + Node four = d_nm->mkConst(Rational(4)); + Node empty = d_nm->mkConst(EmptyBag(d_nm->mkBagType(d_nm->stringType()))); + Node x = d_nm->mkConst(String("x")); + Node y = d_nm->mkConst(String("y")); + Node z = d_nm->mkConst(String("z")); + Node x_4 = d_nm->mkBag(d_nm->stringType(), x, d_nm->mkConst(Rational(4))); + Node y_5 = d_nm->mkBag(d_nm->stringType(), y, d_nm->mkConst(Rational(5))); + Node z_5 = d_nm->mkBag(d_nm->stringType(), z, d_nm->mkConst(Rational(5))); + + Node input1 = d_nm->mkNode(BAG_COUNT, x, empty); + Node output1 = zero; + TS_ASSERT(output1 == NormalForm::evaluate(input1)); + + Node input2 = d_nm->mkNode(BAG_COUNT, x, y_5); + Node output2 = zero; + TS_ASSERT(output2 == NormalForm::evaluate(input2)); + + Node input3 = d_nm->mkNode(BAG_COUNT, x, x_4); + Node output3 = four; + TS_ASSERT(output2 == NormalForm::evaluate(input2)); + + Node unionDisjointXY = d_nm->mkNode(UNION_DISJOINT, x_4, y_5); + Node input4 = d_nm->mkNode(BAG_COUNT, x, unionDisjointXY); + Node output4 = four; + TS_ASSERT(output3 == NormalForm::evaluate(input3)); + + Node unionDisjointYZ = d_nm->mkNode(UNION_DISJOINT, y_5, z_5); + Node input5 = d_nm->mkNode(BAG_COUNT, x, unionDisjointYZ); + Node output5 = zero; + TS_ASSERT(output4 == NormalForm::evaluate(input4)); + } + + void testUnionMax() + { + // 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))) + // output: + // (union_disjoint A B) + // where A = (MK_BAG "x" 4) + // B = (union_disjoint (MK_BAG "y" 1) (MK_BAG "z" 2))) + + Node x = d_nm->mkConst(String("x")); + Node y = d_nm->mkConst(String("y")); + Node z = d_nm->mkConst(String("z")); + Node x_4 = d_nm->mkBag(d_nm->stringType(), x, d_nm->mkConst(Rational(4))); + Node x_3 = d_nm->mkBag(d_nm->stringType(), x, d_nm->mkConst(Rational(3))); + Node x_7 = d_nm->mkBag(d_nm->stringType(), x, d_nm->mkConst(Rational(7))); + Node z_2 = d_nm->mkBag(d_nm->stringType(), z, d_nm->mkConst(Rational(2))); + Node y_1 = d_nm->mkBag(d_nm->stringType(), y, d_nm->mkConst(Rational(1))); + + Node A = d_nm->mkNode(UNION_DISJOINT, x_4, z_2); + Node B = d_nm->mkNode(UNION_DISJOINT, x_3, y_1); + Node input = d_nm->mkNode(UNION_MAX, A, B); + + // output + Node output = d_nm->mkNode( + UNION_DISJOINT, x_4, d_nm->mkNode(UNION_DISJOINT, y_1, z_2)); + + TS_ASSERT(output.isConst()); + TS_ASSERT(output == NormalForm::evaluate(input)); + } + + void testUnionDisjoint1() + { + vector<Node> elements = getNStrings(3); + Node emptybag = + d_nm->mkConst(EmptyBag(d_nm->mkBagType(d_nm->stringType()))); + Node A = d_nm->mkBag( + d_nm->stringType(), elements[0], d_nm->mkConst(Rational(2))); + Node B = d_nm->mkBag( + d_nm->stringType(), elements[1], d_nm->mkConst(Rational(3))); + Node C = d_nm->mkBag( + d_nm->stringType(), elements[2], d_nm->mkConst(Rational(4))); + + Node unionDisjointAB = d_nm->mkNode(UNION_DISJOINT, A, B); + // unionDisjointAB is already in a normal form + TS_ASSERT(unionDisjointAB.isConst()); + TS_ASSERT(unionDisjointAB == NormalForm::evaluate(unionDisjointAB)); + + Node unionDisjointBA = d_nm->mkNode(UNION_DISJOINT, B, A); + // unionDisjointAB is is the normal form of unionDisjointBA + TS_ASSERT(!unionDisjointBA.isConst()); + TS_ASSERT(unionDisjointAB == NormalForm::evaluate(unionDisjointBA)); + + Node unionDisjointAB_C = d_nm->mkNode(UNION_DISJOINT, unionDisjointAB, C); + Node unionDisjointBC = d_nm->mkNode(UNION_DISJOINT, B, C); + Node unionDisjointA_BC = d_nm->mkNode(UNION_DISJOINT, A, unionDisjointBC); + // unionDisjointA_BC is the normal form of unionDisjointAB_C + TS_ASSERT(!unionDisjointAB_C.isConst()); + TS_ASSERT(unionDisjointA_BC.isConst()); + TS_ASSERT(unionDisjointA_BC == NormalForm::evaluate(unionDisjointAB_C)); + + Node unionDisjointAA = d_nm->mkNode(UNION_DISJOINT, A, A); + Node AA = d_nm->mkBag( + d_nm->stringType(), elements[0], d_nm->mkConst(Rational(4))); + TS_ASSERT(!unionDisjointAA.isConst()); + TS_ASSERT(AA.isConst()); + TS_ASSERT(AA == NormalForm::evaluate(unionDisjointAA)); + } + + void testUnionDisjoint2() + { + // 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))) + // output: + // (union_disjoint A B) + // where A = (MK_BAG "x" 7) + // B = (union_disjoint (MK_BAG "y" 1) (MK_BAG "z" 2))) + + Node x = d_nm->mkConst(String("x")); + Node y = d_nm->mkConst(String("y")); + Node z = d_nm->mkConst(String("z")); + Node x_4 = d_nm->mkBag(d_nm->stringType(), x, d_nm->mkConst(Rational(4))); + Node x_3 = d_nm->mkBag(d_nm->stringType(), x, d_nm->mkConst(Rational(3))); + Node x_7 = d_nm->mkBag(d_nm->stringType(), x, d_nm->mkConst(Rational(7))); + Node z_2 = d_nm->mkBag(d_nm->stringType(), z, d_nm->mkConst(Rational(2))); + Node y_1 = d_nm->mkBag(d_nm->stringType(), y, d_nm->mkConst(Rational(1))); + + Node A = d_nm->mkNode(UNION_DISJOINT, x_4, z_2); + Node B = d_nm->mkNode(UNION_DISJOINT, x_3, y_1); + Node input = d_nm->mkNode(UNION_DISJOINT, A, B); + + // output + Node output = d_nm->mkNode( + UNION_DISJOINT, x_7, d_nm->mkNode(UNION_DISJOINT, y_1, z_2)); + + TS_ASSERT(output.isConst()); + TS_ASSERT(output == NormalForm::evaluate(input)); + } + + void testIntersectionMin() + { + // 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))) + // output: + // (MK_BAG "x" 3) + + Node x = d_nm->mkConst(String("x")); + Node y = d_nm->mkConst(String("y")); + Node z = d_nm->mkConst(String("z")); + Node x_4 = d_nm->mkBag(d_nm->stringType(), x, d_nm->mkConst(Rational(4))); + Node x_3 = d_nm->mkBag(d_nm->stringType(), x, d_nm->mkConst(Rational(3))); + Node x_7 = d_nm->mkBag(d_nm->stringType(), x, d_nm->mkConst(Rational(7))); + Node z_2 = d_nm->mkBag(d_nm->stringType(), z, d_nm->mkConst(Rational(2))); + Node y_1 = d_nm->mkBag(d_nm->stringType(), y, d_nm->mkConst(Rational(1))); + + Node A = d_nm->mkNode(UNION_DISJOINT, x_4, z_2); + Node B = d_nm->mkNode(UNION_DISJOINT, x_3, y_1); + Node input = d_nm->mkNode(INTERSECTION_MIN, A, B); + + // output + Node output = x_3; + + TS_ASSERT(output.isConst()); + TS_ASSERT(output == NormalForm::evaluate(input)); + } + + void testDifferenceSubtract() + { + // 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))) + // output: + // (union_disjoint (MK_BAG "x" 1) (MK_BAG "z" 2)) + + Node x = d_nm->mkConst(String("x")); + Node y = d_nm->mkConst(String("y")); + Node z = d_nm->mkConst(String("z")); + Node x_1 = d_nm->mkBag(d_nm->stringType(), x, d_nm->mkConst(Rational(1))); + Node x_4 = d_nm->mkBag(d_nm->stringType(), x, d_nm->mkConst(Rational(4))); + Node x_3 = d_nm->mkBag(d_nm->stringType(), x, d_nm->mkConst(Rational(3))); + Node x_7 = d_nm->mkBag(d_nm->stringType(), x, d_nm->mkConst(Rational(7))); + Node z_2 = d_nm->mkBag(d_nm->stringType(), z, d_nm->mkConst(Rational(2))); + Node y_1 = d_nm->mkBag(d_nm->stringType(), y, d_nm->mkConst(Rational(1))); + + Node A = d_nm->mkNode(UNION_DISJOINT, x_4, z_2); + Node B = d_nm->mkNode(UNION_DISJOINT, x_3, y_1); + Node input = d_nm->mkNode(DIFFERENCE_SUBTRACT, A, B); + + // output + Node output = d_nm->mkNode(UNION_DISJOINT, x_1, z_2); + + TS_ASSERT(output.isConst()); + TS_ASSERT(output == NormalForm::evaluate(input)); + } + + void testDifferenceRemove() + { + // 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))) + // output: + // (MK_BAG "z" 2) + + Node x = d_nm->mkConst(String("x")); + Node y = d_nm->mkConst(String("y")); + Node z = d_nm->mkConst(String("z")); + Node x_1 = d_nm->mkBag(d_nm->stringType(), x, d_nm->mkConst(Rational(1))); + Node x_4 = d_nm->mkBag(d_nm->stringType(), x, d_nm->mkConst(Rational(4))); + Node x_3 = d_nm->mkBag(d_nm->stringType(), x, d_nm->mkConst(Rational(3))); + Node x_7 = d_nm->mkBag(d_nm->stringType(), x, d_nm->mkConst(Rational(7))); + Node z_2 = d_nm->mkBag(d_nm->stringType(), z, d_nm->mkConst(Rational(2))); + Node y_1 = d_nm->mkBag(d_nm->stringType(), y, d_nm->mkConst(Rational(1))); + + Node A = d_nm->mkNode(UNION_DISJOINT, x_4, z_2); + Node B = d_nm->mkNode(UNION_DISJOINT, x_3, y_1); + Node input = d_nm->mkNode(DIFFERENCE_REMOVE, A, B); + + // output + Node output = z_2; + + TS_ASSERT(output.isConst()); + TS_ASSERT(output == NormalForm::evaluate(input)); + } + + void testChoose() + { + // Example + // ------- + // input: (choose (emptybag String)) + // output: "A"; the first element returned by the type enumerator + // input: (choose (MK_BAG "x" 4)) + // output: "x" + // input: (choose (union_disjoint (MK_BAG "x" 4) (MK_BAG "y" 1))) + // output: "x"; deterministically return the first element + Node empty = d_nm->mkConst(EmptyBag(d_nm->mkBagType(d_nm->stringType()))); + Node x = d_nm->mkConst(String("x")); + Node y = d_nm->mkConst(String("y")); + Node z = d_nm->mkConst(String("z")); + Node x_4 = d_nm->mkBag(d_nm->stringType(), x, d_nm->mkConst(Rational(4))); + Node y_1 = d_nm->mkBag(d_nm->stringType(), y, d_nm->mkConst(Rational(1))); + + Node input1 = d_nm->mkNode(BAG_CHOOSE, empty); + Node output1 = d_nm->mkConst(String("")); + + TS_ASSERT(output1 == NormalForm::evaluate(input1)); + + Node input2 = d_nm->mkNode(BAG_CHOOSE, x_4); + Node output2 = x; + TS_ASSERT(output2 == NormalForm::evaluate(input2)); + + Node union_disjoint = d_nm->mkNode(UNION_DISJOINT, x_4, y_1); + Node input3 = d_nm->mkNode(BAG_CHOOSE, union_disjoint); + Node output3 = x; + TS_ASSERT(output3 == NormalForm::evaluate(input3)); + } + + void testBagCard() + { + // Examples + // -------- + // - (card (emptybag String)) = 0 + // - (choose (MK_BAG "x" 4)) = 4 + // - (choose (union_disjoint (MK_BAG "x" 4) (MK_BAG "y" 1))) = 5 + Node empty = d_nm->mkConst(EmptyBag(d_nm->mkBagType(d_nm->stringType()))); + Node x = d_nm->mkConst(String("x")); + Node y = d_nm->mkConst(String("y")); + Node z = d_nm->mkConst(String("z")); + Node x_4 = d_nm->mkBag(d_nm->stringType(), x, d_nm->mkConst(Rational(4))); + Node y_1 = d_nm->mkBag(d_nm->stringType(), y, d_nm->mkConst(Rational(1))); + + Node input1 = d_nm->mkNode(BAG_CARD, empty); + Node output1 = d_nm->mkConst(Rational(0)); + + TS_ASSERT(output1 == NormalForm::evaluate(input1)); + + Node input2 = d_nm->mkNode(BAG_CARD, x_4); + Node output2 = d_nm->mkConst(Rational(4)); + TS_ASSERT(output2 == NormalForm::evaluate(input2)); + + Node union_disjoint = d_nm->mkNode(UNION_DISJOINT, x_4, y_1); + Node input3 = d_nm->mkNode(BAG_CARD, union_disjoint); + Node output3 = d_nm->mkConst(Rational(5)); + TS_ASSERT(output3 == NormalForm::evaluate(input3)); + } + + void testIsSingleton() + { + // 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))) = + // false + Node falseNode = d_nm->mkConst(false); + Node trueNode = d_nm->mkConst(true); + Node empty = d_nm->mkConst(EmptyBag(d_nm->mkBagType(d_nm->stringType()))); + Node x = d_nm->mkConst(String("x")); + Node y = d_nm->mkConst(String("y")); + Node z = d_nm->mkConst(String("z")); + Node x_1 = d_nm->mkBag(d_nm->stringType(), x, d_nm->mkConst(Rational(1))); + Node x_4 = d_nm->mkBag(d_nm->stringType(), x, d_nm->mkConst(Rational(4))); + Node y_1 = d_nm->mkBag(d_nm->stringType(), y, d_nm->mkConst(Rational(1))); + + Node input1 = d_nm->mkNode(BAG_IS_SINGLETON, empty); + Node output1 = falseNode; + TS_ASSERT(output1 == NormalForm::evaluate(input1)); + + Node input2 = d_nm->mkNode(BAG_IS_SINGLETON, x_1); + Node output2 = trueNode; + TS_ASSERT(output2 == NormalForm::evaluate(input2)); + + Node input3 = d_nm->mkNode(BAG_IS_SINGLETON, x_4); + Node output3 = falseNode; + TS_ASSERT(output2 == NormalForm::evaluate(input2)); + + Node union_disjoint = d_nm->mkNode(UNION_DISJOINT, x_1, y_1); + Node input4 = d_nm->mkNode(BAG_IS_SINGLETON, union_disjoint); + Node output4 = falseNode; + TS_ASSERT(output3 == NormalForm::evaluate(input3)); + } + + void testFromSet() + { + // 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)) + + Node emptyset = + d_nm->mkConst(EmptySet(d_nm->mkSetType(d_nm->stringType()))); + Node emptybag = + d_nm->mkConst(EmptyBag(d_nm->mkBagType(d_nm->stringType()))); + Node input1 = d_nm->mkNode(BAG_FROM_SET, emptyset); + Node output1 = emptybag; + TS_ASSERT(output1 == NormalForm::evaluate(input1)); + + Node x = d_nm->mkConst(String("x")); + Node y = d_nm->mkConst(String("y")); + + Node xSingleton = d_nm->mkSingleton(d_nm->stringType(), x); + Node ySingleton = d_nm->mkSingleton(d_nm->stringType(), y); + + Node x_1 = d_nm->mkBag(d_nm->stringType(), x, d_nm->mkConst(Rational(1))); + Node y_1 = d_nm->mkBag(d_nm->stringType(), y, d_nm->mkConst(Rational(1))); + + Node input2 = d_nm->mkNode(BAG_FROM_SET, xSingleton); + Node output2 = x_1; + TS_ASSERT(output2 == NormalForm::evaluate(input2)); + + // for normal sets, the first node is the largest, not smallest + Node normalSet = d_nm->mkNode(UNION, ySingleton, xSingleton); + Node input3 = d_nm->mkNode(BAG_FROM_SET, normalSet); + Node output3 = d_nm->mkNode(UNION_DISJOINT, x_1, y_1); + TS_ASSERT(output3 == NormalForm::evaluate(input3)); + } + + void testToSet() + { + // 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"))) + + Node emptyset = + d_nm->mkConst(EmptySet(d_nm->mkSetType(d_nm->stringType()))); + Node emptybag = + d_nm->mkConst(EmptyBag(d_nm->mkBagType(d_nm->stringType()))); + Node input1 = d_nm->mkNode(BAG_TO_SET, emptybag); + Node output1 = emptyset; + TS_ASSERT(output1 == NormalForm::evaluate(input1)); + + Node x = d_nm->mkConst(String("x")); + Node y = d_nm->mkConst(String("y")); + + Node xSingleton = d_nm->mkSingleton(d_nm->stringType(), x); + Node ySingleton = d_nm->mkSingleton(d_nm->stringType(), y); + + Node x_4 = d_nm->mkBag(d_nm->stringType(), x, d_nm->mkConst(Rational(4))); + Node y_5 = d_nm->mkBag(d_nm->stringType(), y, d_nm->mkConst(Rational(5))); + + Node input2 = d_nm->mkNode(BAG_TO_SET, x_4); + Node output2 = xSingleton; + TS_ASSERT(output2 == NormalForm::evaluate(input2)); + + // for normal sets, the first node is the largest, not smallest + Node normalBag = d_nm->mkNode(UNION_DISJOINT, x_4, y_5); + Node input3 = d_nm->mkNode(BAG_TO_SET, normalBag); + Node output3 = d_nm->mkNode(UNION, ySingleton, xSingleton); + TS_ASSERT(output3 == NormalForm::evaluate(input3)); + } + + private: + std::unique_ptr<ExprManager> d_em; + std::unique_ptr<SmtEngine> d_smt; + std::unique_ptr<NodeManager> d_nm; + std::unique_ptr<BagsRewriter> d_rewriter; +}; /* class BagsTypeRuleBlack */ diff --git a/test/unit/theory/theory_bags_type_rules_white.h b/test/unit/theory/theory_bags_type_rules_white.h index dfe2d4cac..5622a3000 100644 --- a/test/unit/theory/theory_bags_type_rules_white.h +++ b/test/unit/theory/theory_bags_type_rules_white.h @@ -104,6 +104,13 @@ class BagsTypeRuleWhite : public CxxTest::TestSuite Node bag = d_nm->mkBag(d_nm->stringType(), elements[0], d_nm->mkConst(Rational(10))); TS_ASSERT_THROWS_NOTHING(d_nm->mkNode(BAG_TO_SET, bag)); TS_ASSERT(d_nm->mkNode(BAG_TO_SET, bag).getType().isSet()); + std::cout<<"Rational(4, 4).isIntegral() " << d_nm->mkConst(Rational(4,4)).getType()<< std::endl; + std::cout<<"Rational(8, 4).isIntegral() " << d_nm->mkConst(Rational(8,4)).getType()<< std::endl; + std::cout<<"Rational(1, 4).isIntegral() " << d_nm->mkConst(Rational(1,4)).getType()<< std::endl; + + std::cout<<"Rational(4, 4).isIntegral() " << d_nm->mkNode(TO_REAL, d_nm->mkConst(Rational(4,4))).getType()<< std::endl; + std::cout<<"Rational(8, 4).isIntegral() " << d_nm->mkNode(TO_REAL, d_nm->mkConst(Rational(8,4))).getType()<< std::endl; + std::cout<<"Rational(1, 4).isIntegral() " << d_nm->mkNode(TO_REAL, d_nm->mkConst(Rational(1,4))).getType()<< std::endl; } private: |