Add operators bag.from_set, bag.to_set to the theory of bags (#5186)

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 30e95714d29fdfb559f4224524138c825a3069ee..f19ee2bf7feabec7160500da63b89f7e7ded1865 100644 (file)
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -267,6 +267,8 @@ const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> 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, Kind, CVC4::kind::KindHashFunction>
         {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 5910ef1c987ea4ea3ac0cdde1363bfd0be889451..6f84a9959484604ff1658faf9f68dd28fe6afd08 100644 (file)
--- 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 c154db399aad53eb9d60f5e650cdfb7e07d7b0b0..84e25c36ba0514f11fbdcd22fd14951e44cb3d93 100644 (file)
--- 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 dd6565a5b66088cea1fbc4a5dc8f89a1cf99e4d1..1faaf55c0194093decf87d2f48896326d239d09d 100644 (file)
--- 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<Rational>().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 d165be9107ac8f4d26522140af7c35ce93809da6..d36a21ccfdab5d914362be21ed267d0e376740ba 100644 (file)
--- 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 cdbef58dee64cb45b1fcf43903e4df99e33c9ab8..72326de080efa197f3182b7a3ca9137d8db33f66 100644 (file)
--- 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 758f8a6e6923c56a5262bdcc60bd1b8d2d76b593..be3b3cc714c451eb2c317cd19f2e8a636092516d 100644 (file)
--- 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 13b0ff202ddd25ecb07e21fb643f47416122e29f..dc1921e244fd055ff4f6e27ace18f76d850d1e01 100644 (file)
--- 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 e4cd64b48d7adde7e5550472dd921f55bc4197ad..9dcad9bb13da16ace73f1bf42fefb95bc848f103 100644 (file)
--- 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 e4279479df0d4d047273e19b432ee41faa9dd486..67293e2224e92045ed9149ce143265351b05a166 100644 (file)
--- 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 d518058544a0a69ef5e0eabacebaae16c7c479cb..98f56fd44de713b38317d2975742a5dbe2ce57b7 100644 (file)
--- 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<ExprManager> d_em;
   std::unique_ptr<SmtEngine> 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 536a82630b49ae13b6addeb8f97624d58a5fd3fc..d6c225bad12e14715c11ed5ab0daa8c55ca874e3 100644 (file)
--- 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<Node> 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<Node> 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<Node> 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<ExprManager> d_em;
   std::unique_ptr<SmtEngine> d_smt;