From 098cee0ea412e24e24caa79307e2950a640279af Mon Sep 17 00:00:00 2001 From: mudathirmahgoub Date: Wed, 21 Oct 2020 08:19:55 -0500 Subject: [PATCH] Add operator MakeBagOp for constructing bags (#5209) This PR removes subtyping rules for bags and add operator MakeBagOp similar to SingletonOp --- src/CMakeLists.txt | 2 + src/api/cvc4cppkind.h | 3 +- src/expr/node_manager.cpp | 11 +++ src/expr/node_manager.h | 12 ++- src/expr/type_node.cpp | 7 +- src/theory/bags/bags_rewriter.cpp | 3 +- src/theory/bags/kinds | 10 ++- src/theory/bags/make_bag_op.cpp | 48 +++++++++++ src/theory/bags/make_bag_op.h | 63 ++++++++++++++ .../bags/theory_bags_type_enumerator.cpp | 3 +- src/theory/bags/theory_bags_type_rules.h | 49 +++++------ test/unit/theory/CMakeLists.txt | 4 +- ...r_black.h => theory_bags_rewriter_white.h} | 82 +++++++++++-------- ...black.h => theory_bags_type_rules_white.h} | 18 ++-- 14 files changed, 241 insertions(+), 74 deletions(-) create mode 100644 src/theory/bags/make_bag_op.cpp create mode 100644 src/theory/bags/make_bag_op.h rename test/unit/theory/{theory_bags_rewriter_black.h => theory_bags_rewriter_white.h} (90%) rename test/unit/theory/{theory_bags_type_rules_black.h => theory_bags_type_rules_white.h} (84%) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 4d96fa0b3..5966debc1 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -429,6 +429,8 @@ libcvc4_add_sources( theory/bags/bags_statistics.h theory/bags/inference_manager.cpp theory/bags/inference_manager.h + theory/bags/make_bag_op.cpp + theory/bags/make_bag_op.h theory/bags/normal_form.cpp theory/bags/normal_form.h theory/bags/rewrites.cpp diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h index 913a4a993..d6ee24f1e 100644 --- a/src/api/cvc4cppkind.h +++ b/src/api/cvc4cppkind.h @@ -1841,7 +1841,8 @@ enum CVC4_PUBLIC Kind : int32_t */ MEMBER, /** - * The set of the single element given as a parameter. + * Construct a singleton set from an element given as a parameter. + * The returned set has same type of the element. * Parameters: 1 * -[1]: Single element * Create with: diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index f8057006c..e9f121047 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -961,6 +961,17 @@ Node NodeManager::mkSingleton(const TypeNode& t, const TNode n) return singleton; } +Node NodeManager::mkBag(const TypeNode& t, const TNode n, const TNode m) +{ + Assert(n.getType().isSubtypeOf(t)) + << "Invalid operands for mkBag. The type '" << n.getType() + << "' of node '" << n << "' is not a subtype of '" << t << "'." + << std::endl; + Node op = mkConst(MakeBagOp(t)); + Node bag = mkNode(kind::MK_BAG, op, n, m); + return bag; +} + Node NodeManager::mkAbstractValue(const TypeNode& type) { Node n = mkConst(AbstractValue(++d_abstractValueCount)); n.setAttribute(TypeAttr(), type); diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 5427c3b6a..8f2237523 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -578,12 +578,22 @@ class NodeManager { /** * Create a singleton set from the given element n. * @param t the element type of the returned set. - * Note that the type of n needs to be a subtype of t. + * Note that the type of n needs to be a subtype of t. * @param n the single element in the singleton. * @return a singleton set constructed from the element n. */ Node mkSingleton(const TypeNode& t, const TNode n); + /** + * Create a bag from the given element n along with its multiplicity m. + * @param t the element type of the returned bag. + * Note that the type of n needs to be a subtype of t. + * @param n the element that is used to to construct the bag + * @param m the multiplicity of the element n + * @return a bag that contains m occurrences of n. + */ + Node mkBag(const TypeNode& t, const TNode n, const TNode m); + /** * Create a constant of type T. It will have the appropriate * CONST_* kind defined for T. diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 659b1eef2..e917a9d0d 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -574,11 +574,12 @@ TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) { case kind::ARRAY_TYPE: case kind::DATATYPE_TYPE: case kind::PARAMETRIC_DATATYPE: - case kind::SEQUENCE_TYPE: return TypeNode(); + case kind::SEQUENCE_TYPE: case kind::SET_TYPE: + case kind::BAG_TYPE: { - // we don't support subtyping for sets - return TypeNode(); // return null type + // we don't support subtyping except for built in types Int and Real. + return TypeNode(); // return null type } case kind::SEXPR_TYPE: Unimplemented() diff --git a/src/theory/bags/bags_rewriter.cpp b/src/theory/bags/bags_rewriter.cpp index 1faaf55c0..c413a5e7e 100644 --- a/src/theory/bags/bags_rewriter.cpp +++ b/src/theory/bags/bags_rewriter.cpp @@ -438,7 +438,8 @@ BagsRewriteResponse BagsRewriter::rewriteFromSet(const TNode& n) const { // (bag.from_set (singleton (singleton_op Int) x)) = (mkBag x 1) Node one = d_nm->mkConst(Rational(1)); - Node bag = d_nm->mkNode(MK_BAG, n[0][0], one); + TypeNode type = n[0].getType().getSetElementType(); + Node bag = d_nm->mkBag(type, n[0][0], one); return BagsRewriteResponse(bag, Rewrite::FROM_SINGLETON); } return BagsRewriteResponse(n, Rewrite::NONE); diff --git a/src/theory/bags/kinds b/src/theory/bags/kinds index 72326de08..86e89e0bd 100644 --- a/src/theory/bags/kinds +++ b/src/theory/bags/kinds @@ -47,7 +47,14 @@ operator DIFFERENCE_REMOVE 2 "bag difference remove (removes shared elements)" operator BAG_IS_INCLUDED 2 "inclusion predicate for bags (less than or equal multiplicities)" operator BAG_COUNT 2 "multiplicity of an element in a bag" -operator MK_BAG 2 "constructs a bag from one element along with its multiplicity" + +constant MK_BAG_OP \ + ::CVC4::MakeBagOp \ + ::CVC4::MakeBagOpHashFunction \ + "theory/bags/make_bag_op.h" \ + "operator for MK_BAG; payload is an instance of the CVC4::MakeBagOp class" +parameterized MK_BAG MK_BAG_OP 2 \ +"constructs a bag from one element along with its multiplicity" # The operator bag-is-singleton returns whether the given bag is a singleton operator BAG_IS_SINGLETON 1 "return whether the given bag is a singleton" @@ -69,6 +76,7 @@ typerule DIFFERENCE_SUBTRACT ::CVC4::theory::bags::BinaryOperatorTypeRule typerule DIFFERENCE_REMOVE ::CVC4::theory::bags::BinaryOperatorTypeRule typerule BAG_IS_INCLUDED ::CVC4::theory::bags::IsIncludedTypeRule typerule BAG_COUNT ::CVC4::theory::bags::CountTypeRule +typerule MK_BAG_OP "SimpleTypeRule" typerule MK_BAG ::CVC4::theory::bags::MkBagTypeRule typerule EMPTYBAG ::CVC4::theory::bags::EmptyBagTypeRule typerule BAG_CARD ::CVC4::theory::bags::CardTypeRule diff --git a/src/theory/bags/make_bag_op.cpp b/src/theory/bags/make_bag_op.cpp new file mode 100644 index 000000000..6a535afc2 --- /dev/null +++ b/src/theory/bags/make_bag_op.cpp @@ -0,0 +1,48 @@ +/********************* */ +/*! \file bag_op.cpp + ** \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 a class for MK_BAG operator + **/ + +#include + +#include "expr/type_node.h" +#include "make_bag_op.h" + +namespace CVC4 { + +std::ostream& operator<<(std::ostream& out, const MakeBagOp& op) +{ + return out << "(mkBag_op " << op.getType() << ')'; +} + +size_t MakeBagOpHashFunction::operator()(const MakeBagOp& op) const +{ + return TypeNodeHashFunction()(op.getType()); +} + +MakeBagOp::MakeBagOp(const TypeNode& elementType) + : d_type(new TypeNode(elementType)) +{ +} + +MakeBagOp::MakeBagOp(const MakeBagOp& op) : d_type(new TypeNode(op.getType())) +{ +} + +const TypeNode& MakeBagOp::getType() const { return *d_type; } + +bool MakeBagOp::operator==(const MakeBagOp& op) const +{ + return getType() == op.getType(); +} + +} // namespace CVC4 diff --git a/src/theory/bags/make_bag_op.h b/src/theory/bags/make_bag_op.h new file mode 100644 index 000000000..b47930879 --- /dev/null +++ b/src/theory/bags/make_bag_op.h @@ -0,0 +1,63 @@ +/********************* */ +/*! \file mk_bag_op.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 a class for MK_BAG operator + **/ + +#include "cvc4_public.h" + +#ifndef CVC4__MAKE_BAG_OP_H +#define CVC4__MAKE_BAG_OP_H + +#include + +namespace CVC4 { + +class TypeNode; + +/** + * The class is an operator for kind MK_BAG used to construct bags. + * It specifies the type of the element especially when it is a constant. + * e.g. the type of rational 1 is Int, however + * (mkBag (mkBag_op Real) 1) is of type (Bag Real), not (Bag Int). + * Note that the type passed to the constructor is the element's type, not the + * bag type. + */ +class MakeBagOp +{ + public: + MakeBagOp(const TypeNode& elementType); + MakeBagOp(const MakeBagOp& op); + + /** return the type of the current object */ + const TypeNode& getType() const; + + bool operator==(const MakeBagOp& op) const; + + private: + MakeBagOp(); + /** a pointer to the type of the bag element */ + std::unique_ptr d_type; +}; /* class MakeBagOp */ + +std::ostream& operator<<(std::ostream& out, const MakeBagOp& op); + +/** + * Hash function for the MakeBagOpHashFunction objects. + */ +struct CVC4_PUBLIC MakeBagOpHashFunction +{ + size_t operator()(const MakeBagOp& op) const; +}; /* struct MakeBagOpHashFunction */ + +} // namespace CVC4 + +#endif /* CVC4__MAKE_BAG_OP_H */ diff --git a/src/theory/bags/theory_bags_type_enumerator.cpp b/src/theory/bags/theory_bags_type_enumerator.cpp index 7975bb379..727407937 100644 --- a/src/theory/bags/theory_bags_type_enumerator.cpp +++ b/src/theory/bags/theory_bags_type_enumerator.cpp @@ -54,7 +54,8 @@ BagEnumerator& BagEnumerator::operator++() { // increase the multiplicity by one Node one = d_nodeManager->mkConst(Rational(1)); - Node singleton = d_nodeManager->mkNode(kind::MK_BAG, d_element, one); + TypeNode elementType = d_elementTypeEnumerator.getType(); + Node singleton = d_nodeManager->mkBag(elementType, d_element, one); if (d_currentBag.getKind() == kind::EMPTYBAG) { d_currentBag = singleton; diff --git a/src/theory/bags/theory_bags_type_rules.h b/src/theory/bags/theory_bags_type_rules.h index 67293e222..75f57ec88 100644 --- a/src/theory/bags/theory_bags_type_rules.h +++ b/src/theory/bags/theory_bags_type_rules.h @@ -42,19 +42,11 @@ struct BinaryOperatorTypeRule TypeNode secondBagType = n[1].getType(check); if (secondBagType != bagType) { - if (n.getKind() == kind::INTERSECTION_MIN) - { - bagType = TypeNode::mostCommonTypeNode(secondBagType, bagType); - } - else - { - bagType = TypeNode::leastCommonTypeNode(secondBagType, bagType); - } - if (bagType.isNull()) - { - throw TypeCheckingExceptionPrivate( - n, "operator expects two bags of comparable types"); - } + std::stringstream ss; + ss << "Operator " << n.getKind() + << " expects two bags of the same type. Found types '" << bagType + << "' and '" << secondBagType << "'."; + throw TypeCheckingExceptionPrivate(n, ss.str()); } } return bagType; @@ -110,15 +102,9 @@ struct CountTypeRule n, "checking for membership in a non-bag"); } TypeNode elementType = n[0].getType(check); - // TODO(projects#226): comments from sets - // - // T : (Bag Int) - // B : (Bag Real) - // (= (as T (Bag Real)) B) - // (= (bag-count 0.5 B) 1) - // ...where (bag-count 0.5 T) is inferred - - if (!elementType.isComparableTo(bagType.getBagElementType())) + // e.g. (count 1 (mkBag (mkBag_op Real) 1.0 3))) is 3 whereas + // (count 1.0 (mkBag (mkBag_op Int) 1 3))) throws a typing error + if (!elementType.isSubtypeOf(bagType.getBagElementType())) { std::stringstream ss; ss << "member operating on bags of different types:\n" @@ -136,7 +122,10 @@ struct MkBagTypeRule { static TypeNode computeType(NodeManager* nm, TNode n, bool check) { - Assert(n.getKind() == kind::MK_BAG); + Assert(n.getKind() == kind::MK_BAG && n.hasOperator() + && n.getOperator().getKind() == kind::MK_BAG_OP); + MakeBagOp op = n.getOperator().getConst(); + TypeNode expectedElementType = op.getType(); if (check) { if (n.getNumChildren() != 2) @@ -153,9 +142,21 @@ struct MkBagTypeRule ss << "MK_BAG expects an integer for " << n[1] << ". Found" << type1; throw TypeCheckingExceptionPrivate(n, ss.str()); } + + TypeNode actualElementType = n[0].getType(check); + // the type of the element should be a subtype of the type of the operator + // e.g. (mkBag (mkBag_op Real) 1 1) where 1 is an Int + if (!actualElementType.isSubtypeOf(expectedElementType)) + { + std::stringstream ss; + ss << "The type '" << actualElementType + << "' of the element is not a subtype of '" << expectedElementType + << "' in term : " << n; + throw TypeCheckingExceptionPrivate(n, ss.str()); + } } - return nm->mkBagType(n[0].getType(check)); + return nm->mkBagType(expectedElementType); } static bool computeIsConst(NodeManager* nodeManager, TNode n) diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt index e541a24fb..481c80f26 100644 --- a/test/unit/theory/CMakeLists.txt +++ b/test/unit/theory/CMakeLists.txt @@ -14,8 +14,8 @@ 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_rewriter_black theory) -cvc4_add_unit_test_white(theory_bags_type_rules_black 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) cvc4_add_unit_test_white(theory_bv_white theory) cvc4_add_unit_test_white(theory_engine_white theory) diff --git a/test/unit/theory/theory_bags_rewriter_black.h b/test/unit/theory/theory_bags_rewriter_white.h similarity index 90% rename from test/unit/theory/theory_bags_rewriter_black.h rename to test/unit/theory/theory_bags_rewriter_white.h index 98f56fd44..b1c75fdbd 100644 --- a/test/unit/theory/theory_bags_rewriter_black.h +++ b/test/unit/theory/theory_bags_rewriter_white.h @@ -1,5 +1,5 @@ /********************* */ -/*! \file theory_bags_rewriter_black.h +/*! \file theory_bags_rewriter_white.h ** \verbatim ** Top contributors (to current version): ** Mudathir Mohamed @@ -9,7 +9,7 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Black box testing of bags rewriter + ** \brief White box testing of bags rewriter **/ #include @@ -28,7 +28,7 @@ using namespace std; typedef expr::Attribute attribute; -class BagsTypeRuleBlack : public CxxTest::TestSuite +class BagsTypeRuleWhite : public CxxTest::TestSuite { public: void setUp() override @@ -74,8 +74,8 @@ class BagsTypeRuleBlack : public CxxTest::TestSuite Node y = elements[1]; Node c = d_nm->mkSkolem("c", d_nm->integerType()); Node d = d_nm->mkSkolem("d", d_nm->integerType()); - Node bagX = d_nm->mkNode(MK_BAG, x, c); - Node bagY = d_nm->mkNode(MK_BAG, y, d); + Node bagX = d_nm->mkBag(d_nm->stringType(), x, c); + Node bagY = d_nm->mkBag(d_nm->stringType(), y, d); Node emptyBag = d_nm->mkConst(EmptyBag(d_nm->mkBagType(d_nm->stringType()))); @@ -89,11 +89,12 @@ class BagsTypeRuleBlack : public CxxTest::TestSuite void testMkBagConstantElement() { vector elements = getNStrings(1); - Node negative = - d_nm->mkNode(MK_BAG, elements[0], d_nm->mkConst(Rational(-1))); - Node zero = d_nm->mkNode(MK_BAG, elements[0], d_nm->mkConst(Rational(0))); - Node positive = - d_nm->mkNode(MK_BAG, elements[0], d_nm->mkConst(Rational(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()))); RewriteResponse negativeResponse = d_rewriter->postRewrite(negative); @@ -114,10 +115,14 @@ class BagsTypeRuleBlack : public CxxTest::TestSuite void testMkBagVariableElement() { Node skolem = d_nm->mkSkolem("x", d_nm->stringType()); - Node variable = d_nm->mkNode(MK_BAG, skolem, d_nm->mkConst(Rational(-1))); - Node negative = d_nm->mkNode(MK_BAG, skolem, d_nm->mkConst(Rational(-1))); - Node zero = d_nm->mkNode(MK_BAG, skolem, d_nm->mkConst(Rational(0))); - Node positive = d_nm->mkNode(MK_BAG, skolem, d_nm->mkConst(Rational(1))); + Node variable = + d_nm->mkBag(d_nm->stringType(), skolem, d_nm->mkConst(Rational(-1))); + Node negative = + d_nm->mkBag(d_nm->stringType(), skolem, d_nm->mkConst(Rational(-1))); + Node zero = + d_nm->mkBag(d_nm->stringType(), skolem, d_nm->mkConst(Rational(0))); + Node positive = + d_nm->mkBag(d_nm->stringType(), skolem, d_nm->mkConst(Rational(1))); Node emptybag = d_nm->mkConst(EmptyBag(d_nm->mkBagType(d_nm->stringType()))); RewriteResponse negativeResponse = d_rewriter->postRewrite(negative); @@ -140,7 +145,8 @@ class BagsTypeRuleBlack : public CxxTest::TestSuite int n = 3; Node skolem = d_nm->mkSkolem("x", d_nm->stringType()); Node emptyBag = d_nm->mkConst(EmptyBag(d_nm->mkBagType(skolem.getType()))); - Node bag = d_nm->mkNode(MK_BAG, skolem, d_nm->mkConst(Rational(n))); + Node bag = + d_nm->mkBag(d_nm->stringType(), skolem, d_nm->mkConst(Rational(n))); // (bag.count x emptybag) = 0 Node n1 = d_nm->mkNode(BAG_COUNT, skolem, emptyBag); @@ -161,8 +167,10 @@ class BagsTypeRuleBlack : public CxxTest::TestSuite vector elements = getNStrings(2); Node emptyBag = d_nm->mkConst(EmptyBag(d_nm->mkBagType(d_nm->stringType()))); - Node A = d_nm->mkNode(MK_BAG, elements[0], d_nm->mkConst(Rational(n))); - Node B = d_nm->mkNode(MK_BAG, elements[1], d_nm->mkConst(Rational(n + 1))); + Node A = d_nm->mkBag( + d_nm->stringType(), elements[0], d_nm->mkConst(Rational(n))); + Node B = d_nm->mkBag( + d_nm->stringType(), elements[1], d_nm->mkConst(Rational(n + 1))); Node unionMaxAB = d_nm->mkNode(UNION_MAX, A, B); Node unionMaxBA = d_nm->mkNode(UNION_MAX, B, A); Node unionDisjointAB = d_nm->mkNode(UNION_DISJOINT, A, B); @@ -241,8 +249,10 @@ class BagsTypeRuleBlack : public CxxTest::TestSuite vector elements = getNStrings(2); Node emptyBag = d_nm->mkConst(EmptyBag(d_nm->mkBagType(d_nm->stringType()))); - Node A = d_nm->mkNode(MK_BAG, elements[0], d_nm->mkConst(Rational(n))); - Node B = d_nm->mkNode(MK_BAG, elements[1], d_nm->mkConst(Rational(n + 1))); + Node A = d_nm->mkBag( + d_nm->stringType(), elements[0], d_nm->mkConst(Rational(n))); + Node B = d_nm->mkBag( + d_nm->stringType(), elements[1], d_nm->mkConst(Rational(n + 1))); Node unionDisjointAB = d_nm->mkNode(UNION_DISJOINT, A, B); Node unionDisjointBA = d_nm->mkNode(UNION_DISJOINT, B, A); Node unionMaxAB = d_nm->mkNode(UNION_MAX, A, B); @@ -285,8 +295,10 @@ class BagsTypeRuleBlack : public CxxTest::TestSuite vector elements = getNStrings(2); Node emptyBag = d_nm->mkConst(EmptyBag(d_nm->mkBagType(d_nm->stringType()))); - Node A = d_nm->mkNode(MK_BAG, elements[0], d_nm->mkConst(Rational(n))); - Node B = d_nm->mkNode(MK_BAG, elements[1], d_nm->mkConst(Rational(n + 1))); + Node A = d_nm->mkBag( + d_nm->stringType(), elements[0], d_nm->mkConst(Rational(n))); + Node B = d_nm->mkBag( + d_nm->stringType(), elements[1], d_nm->mkConst(Rational(n + 1))); Node unionMaxAB = d_nm->mkNode(UNION_MAX, A, B); Node unionMaxBA = d_nm->mkNode(UNION_MAX, B, A); Node unionDisjointAB = d_nm->mkNode(UNION_DISJOINT, A, B); @@ -365,8 +377,10 @@ class BagsTypeRuleBlack : public CxxTest::TestSuite vector elements = getNStrings(2); Node emptyBag = d_nm->mkConst(EmptyBag(d_nm->mkBagType(d_nm->stringType()))); - Node A = d_nm->mkNode(MK_BAG, elements[0], d_nm->mkConst(Rational(n))); - Node B = d_nm->mkNode(MK_BAG, elements[1], d_nm->mkConst(Rational(n + 1))); + Node A = d_nm->mkBag( + d_nm->stringType(), elements[0], d_nm->mkConst(Rational(n))); + Node B = d_nm->mkBag( + d_nm->stringType(), elements[1], d_nm->mkConst(Rational(n + 1))); Node unionMaxAB = d_nm->mkNode(UNION_MAX, A, B); Node unionMaxBA = d_nm->mkNode(UNION_MAX, B, A); Node unionDisjointAB = d_nm->mkNode(UNION_DISJOINT, A, B); @@ -447,8 +461,10 @@ class BagsTypeRuleBlack : public CxxTest::TestSuite vector elements = getNStrings(2); Node emptyBag = d_nm->mkConst(EmptyBag(d_nm->mkBagType(d_nm->stringType()))); - Node A = d_nm->mkNode(MK_BAG, elements[0], d_nm->mkConst(Rational(n))); - Node B = d_nm->mkNode(MK_BAG, elements[1], d_nm->mkConst(Rational(n + 1))); + Node A = d_nm->mkBag( + d_nm->stringType(), elements[0], d_nm->mkConst(Rational(n))); + Node B = d_nm->mkBag( + d_nm->stringType(), elements[1], d_nm->mkConst(Rational(n + 1))); Node unionMaxAB = d_nm->mkNode(UNION_MAX, A, B); Node unionMaxBA = d_nm->mkNode(UNION_MAX, B, A); Node unionDisjointAB = d_nm->mkNode(UNION_DISJOINT, A, B); @@ -515,7 +531,7 @@ class BagsTypeRuleBlack : public CxxTest::TestSuite { Node x = d_nm->mkSkolem("x", d_nm->stringType()); Node c = d_nm->mkConst(Rational(3)); - Node bag = d_nm->mkNode(MK_BAG, x, c); + Node bag = d_nm->mkBag(d_nm->stringType(), x, c); // (bag.choose (mkBag x c)) = x where c is a constant > 0 Node n1 = d_nm->mkNode(BAG_CHOOSE, bag); @@ -531,10 +547,12 @@ class BagsTypeRuleBlack : public CxxTest::TestSuite d_nm->mkConst(EmptyBag(d_nm->mkBagType(d_nm->stringType()))); Node zero = d_nm->mkConst(Rational(0)); Node c = d_nm->mkConst(Rational(3)); - Node bag = d_nm->mkNode(MK_BAG, x, c); + Node bag = d_nm->mkBag(d_nm->stringType(), x, c); vector elements = getNStrings(2); - Node A = d_nm->mkNode(MK_BAG, elements[0], d_nm->mkConst(Rational(4))); - Node B = d_nm->mkNode(MK_BAG, elements[1], d_nm->mkConst(Rational(5))); + Node A = d_nm->mkBag( + d_nm->stringType(), elements[0], d_nm->mkConst(Rational(4))); + Node B = d_nm->mkBag( + d_nm->stringType(), elements[1], d_nm->mkConst(Rational(5))); Node unionDisjointAB = d_nm->mkNode(UNION_DISJOINT, A, B); // TODO(projects#223): enable this test after implementing bags normal form @@ -566,7 +584,7 @@ class BagsTypeRuleBlack : public CxxTest::TestSuite d_nm->mkConst(EmptyBag(d_nm->mkBagType(d_nm->stringType()))); Node x = d_nm->mkSkolem("x", d_nm->stringType()); Node c = d_nm->mkSkolem("c", d_nm->integerType()); - Node bag = d_nm->mkNode(MK_BAG, x, c); + Node bag = d_nm->mkBag(d_nm->stringType(), x, c); // TODO(projects#223): complete this function // (bag.is_singleton emptybag) = false @@ -593,7 +611,7 @@ class BagsTypeRuleBlack : public CxxTest::TestSuite Node n = d_nm->mkNode(BAG_FROM_SET, singleton); RewriteResponse response = d_rewriter->postRewrite(n); Node one = d_nm->mkConst(Rational(1)); - Node bag = d_nm->mkNode(MK_BAG, x, one); + Node bag = d_nm->mkBag(d_nm->stringType(), x, one); TS_ASSERT(response.d_node == bag && response.d_status == REWRITE_AGAIN_FULL); } @@ -601,7 +619,7 @@ class BagsTypeRuleBlack : public CxxTest::TestSuite void testToSet() { Node x = d_nm->mkSkolem("x", d_nm->stringType()); - Node bag = d_nm->mkNode(MK_BAG, x, d_nm->mkConst(Rational(5))); + Node bag = d_nm->mkBag(d_nm->stringType(), x, d_nm->mkConst(Rational(5))); // (bag.to_set (mkBag x n)) = (singleton (singleton_op T) x) Node n = d_nm->mkNode(BAG_TO_SET, bag); diff --git a/test/unit/theory/theory_bags_type_rules_black.h b/test/unit/theory/theory_bags_type_rules_white.h similarity index 84% rename from test/unit/theory/theory_bags_type_rules_black.h rename to test/unit/theory/theory_bags_type_rules_white.h index d6c225bad..dfe2d4cac 100644 --- a/test/unit/theory/theory_bags_type_rules_black.h +++ b/test/unit/theory/theory_bags_type_rules_white.h @@ -28,7 +28,7 @@ using namespace std; typedef expr::Attribute attribute; -class BagsTypeRuleBlack : public CxxTest::TestSuite +class BagsTypeRuleWhite : public CxxTest::TestSuite { public: void setUp() override @@ -63,7 +63,8 @@ class BagsTypeRuleBlack : public CxxTest::TestSuite void testCountOperator() { vector elements = getNStrings(1); - Node bag = d_nm->mkNode(MK_BAG, elements[0], d_nm->mkConst(Rational(100))); + Node bag = d_nm->mkBag( + d_nm->stringType(), elements[0], d_nm->mkConst(Rational(100))); Node count = d_nm->mkNode(BAG_COUNT, elements[0], bag); Node node = d_nm->mkConst(Rational(10)); @@ -76,11 +77,12 @@ class BagsTypeRuleBlack : public CxxTest::TestSuite void testMkBagOperator() { vector elements = getNStrings(1); - Node negative = - d_nm->mkNode(MK_BAG, elements[0], d_nm->mkConst(Rational(-1))); - Node zero = d_nm->mkNode(MK_BAG, elements[0], d_nm->mkConst(Rational(0))); - Node positive = - d_nm->mkNode(MK_BAG, elements[0], d_nm->mkConst(Rational(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))); // only positive multiplicity are constants TS_ASSERT(!MkBagTypeRule::computeIsConst(d_nm.get(), negative)); @@ -99,7 +101,7 @@ class BagsTypeRuleBlack : public CxxTest::TestSuite void testToSetOperator() { vector elements = getNStrings(1); - Node bag = d_nm->mkNode(MK_BAG, elements[0], d_nm->mkConst(Rational(10))); + 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()); } -- 2.30.2