From f3c6bb510a87f390c51bf3cecc079cc9c9615ea4 Mon Sep 17 00:00:00 2001 From: mudathirmahgoub Date: Tue, 6 Oct 2020 08:23:40 -0500 Subject: [PATCH] Add operators bag.from_set, bag.to_set to the theory of bags (#5186) --- src/api/cvc4cpp.cpp | 4 ++ src/api/cvc4cppkind.h | 16 ++++++++ src/parser/smt2/smt2.cpp | 2 + src/theory/bags/bags_rewriter.cpp | 29 ++++++++++++++ src/theory/bags/bags_rewriter.h | 13 ++++++ src/theory/bags/kinds | 4 ++ src/theory/bags/rewrites.cpp | 2 + src/theory/bags/rewrites.h | 4 +- src/theory/bags/theory_bags.cpp | 2 + src/theory/bags/theory_bags_type_rules.h | 40 +++++++++++++++++++ test/unit/theory/theory_bags_rewriter_black.h | 27 +++++++++++++ .../theory/theory_bags_type_rules_black.h | 26 ++++++++++-- 12 files changed, 164 insertions(+), 5 deletions(-) diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 30e95714d..f19ee2bf7 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -267,6 +267,8 @@ const static std::unordered_map s_kinds{ {BAG_CARD, CVC4::Kind::BAG_CARD}, {BAG_CHOOSE, CVC4::Kind::BAG_CHOOSE}, {BAG_IS_SINGLETON, CVC4::Kind::BAG_IS_SINGLETON}, + {BAG_FROM_SET, CVC4::Kind::BAG_FROM_SET}, + {BAG_TO_SET, CVC4::Kind::BAG_TO_SET}, /* Strings ------------------------------------------------------------- */ {STRING_CONCAT, CVC4::Kind::STRING_CONCAT}, {STRING_IN_REGEXP, CVC4::Kind::STRING_IN_REGEXP}, @@ -570,6 +572,8 @@ const static std::unordered_map {CVC4::Kind::BAG_CARD, BAG_CARD}, {CVC4::Kind::BAG_CHOOSE, BAG_CHOOSE}, {CVC4::Kind::BAG_IS_SINGLETON, BAG_IS_SINGLETON}, + {CVC4::Kind::BAG_FROM_SET, BAG_FROM_SET}, + {CVC4::Kind::BAG_TO_SET, BAG_TO_SET}, /* Strings --------------------------------------------------------- */ {CVC4::Kind::STRING_CONCAT, STRING_CONCAT}, {CVC4::Kind::STRING_IN_REGEXP, STRING_IN_REGEXP}, diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h index 5910ef1c9..6f84a9959 100644 --- a/src/api/cvc4cppkind.h +++ b/src/api/cvc4cppkind.h @@ -2074,6 +2074,22 @@ enum CVC4_PUBLIC Kind : int32_t * mkTerm(Kind kind, Term child) */ BAG_IS_SINGLETON, + /** + * Bag.from_set converts a set to a bag. + * Parameters: 1 + * -[1]: Term of set sort + * Create with: + * mkTerm(Kind kind, Term child) + */ + BAG_FROM_SET, + /** + * Bag.to_set converts a bag to a set. + * Parameters: 1 + * -[1]: Term of bag sort + * Create with: + * mkTerm(Kind kind, Term child) + */ + BAG_TO_SET, /* Strings --------------------------------------------------------------- */ diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index c154db399..84e25c36b 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -704,6 +704,8 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) addOperator(api::BAG_CARD, "bag.card"); addOperator(api::BAG_CHOOSE, "bag.choose"); addOperator(api::BAG_IS_SINGLETON, "bag.is_singleton"); + addOperator(api::BAG_FROM_SET, "bag.from_set"); + addOperator(api::BAG_TO_SET, "bag.to_set"); } if(d_logic.isTheoryEnabled(theory::THEORY_STRINGS)) { defineType("String", d_solver->getStringSort()); diff --git a/src/theory/bags/bags_rewriter.cpp b/src/theory/bags/bags_rewriter.cpp index dd6565a5b..1faaf55c0 100644 --- a/src/theory/bags/bags_rewriter.cpp +++ b/src/theory/bags/bags_rewriter.cpp @@ -71,6 +71,8 @@ RewriteResponse BagsRewriter::postRewrite(TNode n) case BAG_CHOOSE: response = rewriteChoose(n); break; case BAG_CARD: response = rewriteCard(n); break; case BAG_IS_SINGLETON: response = rewriteIsSingleton(n); break; + case BAG_FROM_SET: response = rewriteFromSet(n); break; + case BAG_TO_SET: response = rewriteToSet(n); break; default: response = BagsRewriteResponse(n, Rewrite::NONE); break; } } @@ -429,6 +431,33 @@ BagsRewriteResponse BagsRewriter::rewriteIsSingleton(const TNode& n) const return BagsRewriteResponse(n, Rewrite::NONE); } +BagsRewriteResponse BagsRewriter::rewriteFromSet(const TNode& n) const +{ + Assert(n.getKind() == BAG_FROM_SET); + if (n[0].getKind() == SINGLETON) + { + // (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); + return BagsRewriteResponse(bag, Rewrite::FROM_SINGLETON); + } + return BagsRewriteResponse(n, Rewrite::NONE); +} + +BagsRewriteResponse BagsRewriter::rewriteToSet(const TNode& n) const +{ + Assert(n.getKind() == BAG_TO_SET); + if (n[0].getKind() == MK_BAG && n[0][1].isConst() + && n[0][1].getConst().sgn() == 1) + { + // (bag.to_set (mkBag x n)) = (singleton (singleton_op T) x) + // where n is a positive constant and T is the type of the bag's elements + Node bag = d_nm->mkSingleton(n[0][0].getType(), n[0][0]); + return BagsRewriteResponse(bag, Rewrite::TO_SINGLETON); + } + return BagsRewriteResponse(n, Rewrite::NONE); +} + } // namespace bags } // namespace theory } // namespace CVC4 diff --git a/src/theory/bags/bags_rewriter.h b/src/theory/bags/bags_rewriter.h index d165be910..d36a21ccf 100644 --- a/src/theory/bags/bags_rewriter.h +++ b/src/theory/bags/bags_rewriter.h @@ -181,6 +181,19 @@ class BagsRewriter : public TheoryRewriter */ BagsRewriteResponse rewriteIsSingleton(const TNode& n) const; + /** + * rewrites for n include: + * - (bag.from_set (singleton (singleton_op Int) x)) = (mkBag x 1) + */ + BagsRewriteResponse rewriteFromSet(const TNode& n) const; + + /** + * rewrites for n include: + * - (bag.to_set (mkBag x n)) = (singleton (singleton_op T) x) + * where n is a positive constant and T is the type of the bag's elements + */ + BagsRewriteResponse rewriteToSet(const TNode& n) const; + private: /** Reference to the rewriter statistics. */ NodeManager* d_nm; diff --git a/src/theory/bags/kinds b/src/theory/bags/kinds index cdbef58de..72326de08 100644 --- a/src/theory/bags/kinds +++ b/src/theory/bags/kinds @@ -53,6 +53,8 @@ operator MK_BAG 2 "constructs a bag from one element along with its operator BAG_IS_SINGLETON 1 "return whether the given bag is a singleton" operator BAG_CARD 1 "bag cardinality operator" +operator BAG_FROM_SET 1 "converts a set to a bag" +operator BAG_TO_SET 1 "converts a bag to a set" # The operator choose returns an element from a given bag. # If bag A = {("a", 1)}, then the term (choose A) is equivalent to the term a. @@ -72,6 +74,8 @@ typerule EMPTYBAG ::CVC4::theory::bags::EmptyBagTypeRule typerule BAG_CARD ::CVC4::theory::bags::CardTypeRule typerule BAG_CHOOSE ::CVC4::theory::bags::ChooseTypeRule typerule BAG_IS_SINGLETON ::CVC4::theory::bags::IsSingletonTypeRule +typerule BAG_FROM_SET ::CVC4::theory::bags::FromSetTypeRule +typerule BAG_TO_SET ::CVC4::theory::bags::ToSetTypeRule construle UNION_DISJOINT ::CVC4::theory::bags::BinaryOperatorTypeRule construle MK_BAG ::CVC4::theory::bags::MkBagTypeRule diff --git a/src/theory/bags/rewrites.cpp b/src/theory/bags/rewrites.cpp index 758f8a6e6..be3b3cc71 100644 --- a/src/theory/bags/rewrites.cpp +++ b/src/theory/bags/rewrites.cpp @@ -31,6 +31,7 @@ const char* toString(Rewrite r) case Rewrite::CONSTANT_EVALUATION: return "CONSTANT_EVALUATION"; case Rewrite::COUNT_EMPTY: return "COUNT_EMPTY"; case Rewrite::COUNT_MK_BAG: return "COUNT_MK_BAG"; + case Rewrite::FROM_SINGLETON: return "FROM_SINGLETON"; case Rewrite::IDENTICAL_NODES: return "IDENTICAL_NODES"; case Rewrite::INTERSECTION_EMPTY_LEFT: return "INTERSECTION_EMPTY_LEFT"; case Rewrite::INTERSECTION_EMPTY_RIGHT: return "INTERSECTION_EMPTY_RIGHT"; @@ -53,6 +54,7 @@ const char* toString(Rewrite r) case Rewrite::SUBTRACT_RETURN_LEFT: return "SUBTRACT_RETURN_LEFT"; case Rewrite::SUBTRACT_SAME: return "SUBTRACT_SAME"; case Rewrite::UNION_DISJOINT_EMPTY_LEFT: return "UNION_DISJOINT_EMPTY_LEFT"; + case Rewrite::TO_SINGLETON: return "TO_SINGLETON"; case Rewrite::UNION_DISJOINT_EMPTY_RIGHT: return "UNION_DISJOINT_EMPTY_RIGHT"; case Rewrite::UNION_DISJOINT_MAX_MIN: return "UNION_DISJOINT_MAX_MIN"; diff --git a/src/theory/bags/rewrites.h b/src/theory/bags/rewrites.h index 13b0ff202..dc1921e24 100644 --- a/src/theory/bags/rewrites.h +++ b/src/theory/bags/rewrites.h @@ -29,13 +29,14 @@ namespace bags { */ enum class Rewrite : uint32_t { - NONE, // no rewrite happened + NONE, // no rewrite happened CARD_DISJOINT, CARD_MK_BAG, CHOOSE_MK_BAG, CONSTANT_EVALUATION, COUNT_EMPTY, COUNT_MK_BAG, + FROM_SINGLETON, IDENTICAL_NODES, INTERSECTION_EMPTY_LEFT, INTERSECTION_EMPTY_RIGHT, @@ -55,6 +56,7 @@ enum class Rewrite : uint32_t SUBTRACT_MIN, SUBTRACT_RETURN_LEFT, SUBTRACT_SAME, + TO_SINGLETON, UNION_DISJOINT_EMPTY_LEFT, UNION_DISJOINT_EMPTY_RIGHT, UNION_DISJOINT_MAX_MIN, diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp index e4cd64b48..9dcad9bb1 100644 --- a/src/theory/bags/theory_bags.cpp +++ b/src/theory/bags/theory_bags.cpp @@ -65,6 +65,8 @@ void TheoryBags::finishInit() d_equalityEngine->addFunctionKind(BAG_COUNT); d_equalityEngine->addFunctionKind(MK_BAG); d_equalityEngine->addFunctionKind(BAG_CARD); + d_equalityEngine->addFunctionKind(BAG_FROM_SET); + d_equalityEngine->addFunctionKind(BAG_TO_SET); } void TheoryBags::postCheck(Effort level) {} diff --git a/src/theory/bags/theory_bags_type_rules.h b/src/theory/bags/theory_bags_type_rules.h index e4279479d..67293e222 100644 --- a/src/theory/bags/theory_bags_type_rules.h +++ b/src/theory/bags/theory_bags_type_rules.h @@ -232,6 +232,46 @@ struct ChooseTypeRule } }; /* struct ChooseTypeRule */ +struct FromSetTypeRule +{ + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + { + Assert(n.getKind() == kind::BAG_FROM_SET); + TypeNode setType = n[0].getType(check); + if (check) + { + if (!setType.isSet()) + { + throw TypeCheckingExceptionPrivate( + n, "bag.from_set operator expects a set, a non-set is found"); + } + } + TypeNode elementType = setType.getSetElementType(); + TypeNode bagType = nodeManager->mkBagType(elementType); + return bagType; + } +}; /* struct FromSetTypeRule */ + +struct ToSetTypeRule +{ + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + { + Assert(n.getKind() == kind::BAG_TO_SET); + TypeNode bagType = n[0].getType(check); + if (check) + { + if (!bagType.isBag()) + { + throw TypeCheckingExceptionPrivate( + n, "bag.to_set operator expects a bag, a non-bag is found"); + } + } + TypeNode elementType = bagType.getBagElementType(); + TypeNode setType = nodeManager->mkSetType(elementType); + return setType; + } +}; /* struct ToSetTypeRule */ + struct BagsProperties { static Cardinality computeCardinality(TypeNode type) diff --git a/test/unit/theory/theory_bags_rewriter_black.h b/test/unit/theory/theory_bags_rewriter_black.h index d51805854..98f56fd44 100644 --- a/test/unit/theory/theory_bags_rewriter_black.h +++ b/test/unit/theory/theory_bags_rewriter_black.h @@ -584,6 +584,33 @@ class BagsTypeRuleBlack : public CxxTest::TestSuite && response2.d_status == REWRITE_AGAIN_FULL); } + void testFromSet() + { + Node x = d_nm->mkSkolem("x", d_nm->stringType()); + Node singleton = d_nm->mkSingleton(d_nm->stringType(), x); + + // (bag.from_set (singleton (singleton_op Int) x)) = (mkBag x 1) + 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); + TS_ASSERT(response.d_node == bag + && response.d_status == REWRITE_AGAIN_FULL); + } + + void testToSet() + { + Node x = d_nm->mkSkolem("x", d_nm->stringType()); + Node bag = d_nm->mkNode(MK_BAG, 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); + RewriteResponse response = d_rewriter->postRewrite(n); + Node singleton = d_nm->mkSingleton(d_nm->stringType(), x); + TS_ASSERT(response.d_node == singleton + && response.d_status == REWRITE_AGAIN_FULL); + } + private: std::unique_ptr d_em; std::unique_ptr d_smt; diff --git a/test/unit/theory/theory_bags_type_rules_black.h b/test/unit/theory/theory_bags_type_rules_black.h index 536a82630..d6c225bad 100644 --- a/test/unit/theory/theory_bags_type_rules_black.h +++ b/test/unit/theory/theory_bags_type_rules_black.h @@ -76,16 +76,34 @@ 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 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 positive = + d_nm->mkNode(MK_BAG, elements[0], d_nm->mkConst(Rational(1))); // only positive multiplicity are constants - TS_ASSERT(! MkBagTypeRule::computeIsConst(d_nm.get(), negative)); - TS_ASSERT(! MkBagTypeRule::computeIsConst(d_nm.get(), zero)); + TS_ASSERT(!MkBagTypeRule::computeIsConst(d_nm.get(), negative)); + TS_ASSERT(!MkBagTypeRule::computeIsConst(d_nm.get(), zero)); TS_ASSERT(MkBagTypeRule::computeIsConst(d_nm.get(), positive)); } + void testFromSetOperator() + { + vector elements = getNStrings(1); + Node set = d_nm->mkSingleton(d_nm->stringType(), elements[0]); + TS_ASSERT_THROWS_NOTHING(d_nm->mkNode(BAG_FROM_SET, set)); + TS_ASSERT(d_nm->mkNode(BAG_FROM_SET, set).getType().isBag()); + } + + void testToSetOperator() + { + vector elements = getNStrings(1); + Node bag = d_nm->mkNode(MK_BAG, 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()); + } + private: std::unique_ptr d_em; std::unique_ptr d_smt; -- 2.30.2