Add operator MakeBagOp for constructing bags (#5209)

This PR removes subtyping rules for bags and add operator MakeBagOp similar to SingletonOp

6 files changed, 149 insertions, 27 deletions

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<RBuiltinOperator>"
 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 <iostream>
+
+#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 <memory>
+
+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<TypeNode> 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<MakeBagOp>();
+    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)