Add operator MakeBagOp for constructing bags (#5209)

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

3 files changed, 26 insertions, 4 deletions

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,13 +578,23 @@ 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()