Add skeleton for theory of bags (multisets) (#5100)

This PR adds initial headers and mostly empty source files for the theory of bags (multisets).
It acts as a basis for future commits.
It includes straightforward implementation for typing rules an enumerator for bags.

37 files changed, 1631 insertions, 12 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 2279c7097..1bc393053 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -402,6 +402,21 @@ libcvc4_add_sources(
   theory/assertion.h
   theory/atom_requests.cpp
   theory/atom_requests.h
+  theory/bags/inference_manager.cpp
+  theory/bags/inference_manager.h
+  theory/bags/normal_form.cpp
+  theory/bags/normal_form.h
+  theory/bags/solver_state.cpp
+  theory/bags/solver_state.h
+  theory/bags/term_registry.cpp
+  theory/bags/term_registry.h
+  theory/bags/theory_bags.cpp
+  theory/bags/theory_bags.h
+  theory/bags/theory_bags_rewriter.cpp
+  theory/bags/theory_bags_rewriter.h
+  theory/bags/theory_bags_type_enumerator.cpp
+  theory/bags/theory_bags_type_enumerator.h
+  theory/bags/theory_bags_type_rules.h
   theory/booleans/circuit_propagator.cpp
   theory/booleans/circuit_propagator.h
   theory/booleans/proof_checker.cpp
@@ -908,6 +923,7 @@ set(KINDS_FILES
   ${PROJECT_SOURCE_DIR}/src/theory/datatypes/kinds
   ${PROJECT_SOURCE_DIR}/src/theory/sep/kinds
   ${PROJECT_SOURCE_DIR}/src/theory/sets/kinds
+  ${PROJECT_SOURCE_DIR}/src/theory/bags/kinds
   ${PROJECT_SOURCE_DIR}/src/theory/strings/kinds
   ${PROJECT_SOURCE_DIR}/src/theory/quantifiers/kinds)
 
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 47cc7234f..401f62cae 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -254,6 +254,19 @@ const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> s_kinds{
     {COMPREHENSION, CVC4::Kind::COMPREHENSION},
     {CHOOSE, CVC4::Kind::CHOOSE},
     {IS_SINGLETON, CVC4::Kind::IS_SINGLETON},
+    /* Bags ---------------------------------------------------------------- */
+    {UNION_MAX, CVC4::Kind::UNION_MAX},
+    {UNION_DISJOINT, CVC4::Kind::UNION_DISJOINT},
+    {INTERSECTION_MIN, CVC4::Kind::INTERSECTION_MIN},
+    {DIFFERENCE_SUBTRACT, CVC4::Kind::DIFFERENCE_SUBTRACT},
+    {DIFFERENCE_REMOVE, CVC4::Kind::DIFFERENCE_REMOVE},
+    {BAG_IS_INCLUDED, CVC4::Kind::BAG_IS_INCLUDED},
+    {BAG_COUNT, CVC4::Kind::BAG_COUNT},
+    {MK_BAG, CVC4::Kind::MK_BAG},
+    {EMPTYBAG, CVC4::Kind::EMPTYBAG},
+    {BAG_CARD, CVC4::Kind::BAG_CARD},
+    {BAG_CHOOSE, CVC4::Kind::BAG_CHOOSE},
+    {BAG_IS_SINGLETON, CVC4::Kind::BAG_IS_SINGLETON},
     /* Strings ------------------------------------------------------------- */
     {STRING_CONCAT, CVC4::Kind::STRING_CONCAT},
     {STRING_IN_REGEXP, CVC4::Kind::STRING_IN_REGEXP},
@@ -544,6 +557,19 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction>
         {CVC4::Kind::COMPREHENSION, COMPREHENSION},
         {CVC4::Kind::CHOOSE, CHOOSE},
         {CVC4::Kind::IS_SINGLETON, IS_SINGLETON},
+        /* Bags ------------------------------------------------------------ */
+        {CVC4::Kind::UNION_MAX, UNION_MAX},
+        {CVC4::Kind::UNION_DISJOINT, UNION_DISJOINT},
+        {CVC4::Kind::INTERSECTION_MIN, INTERSECTION_MIN},
+        {CVC4::Kind::DIFFERENCE_SUBTRACT, DIFFERENCE_SUBTRACT},
+        {CVC4::Kind::DIFFERENCE_REMOVE, DIFFERENCE_REMOVE},
+        {CVC4::Kind::BAG_IS_INCLUDED, BAG_IS_INCLUDED},
+        {CVC4::Kind::BAG_COUNT, BAG_COUNT},
+        {CVC4::Kind::MK_BAG, MK_BAG},
+        {CVC4::Kind::EMPTYBAG, EMPTYBAG},
+        {CVC4::Kind::BAG_CARD, BAG_CARD},
+        {CVC4::Kind::BAG_CHOOSE, BAG_CHOOSE},
+        {CVC4::Kind::BAG_IS_SINGLETON, BAG_IS_SINGLETON},
         /* Strings --------------------------------------------------------- */
         {CVC4::Kind::STRING_CONCAT, STRING_CONCAT},
         {CVC4::Kind::STRING_IN_REGEXP, STRING_IN_REGEXP},
@@ -951,6 +977,8 @@ bool Sort::isArray() const { return d_type->isArray(); }
 
 bool Sort::isSet() const { return d_type->isSet(); }
 
+bool Sort::isBag() const { return TypeNode::fromType(*d_type).isBag(); }
+
 bool Sort::isSequence() const { return d_type->isSequence(); }
 
 bool Sort::isUninterpretedSort() const { return d_type->isSort(); }
@@ -1069,7 +1097,17 @@ Sort Sort::getSetElementSort() const
   return Sort(d_solver, SetType(*d_type).getElementType());
 }
 
-/* Set sort ------------------------------------------------------------ */
+/* Bag sort ------------------------------------------------------------ */
+
+Sort Sort::getBagElementSort() const
+{
+  CVC4_API_CHECK(isBag()) << "Not a bag sort.";
+  TypeNode typeNode = TypeNode::fromType(*d_type);
+  Type type = typeNode.getBagElementType().toType();
+  return Sort(d_solver, type);
+}
+
+/* Sequence sort ------------------------------------------------------- */
 
 Sort Sort::getSequenceElementSort() const
 {
@@ -3495,6 +3533,20 @@ Sort Solver::mkSetSort(Sort elemSort) const
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
+Sort Solver::mkBagSort(Sort elemSort) const
+{
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4_API_ARG_CHECK_EXPECTED(!elemSort.isNull(), elemSort)
+      << "non-null element sort";
+  CVC4_API_SOLVER_CHECK_SORT(elemSort);
+
+  TypeNode typeNode = TypeNode::fromType(*elemSort.d_type);
+  Type type = getNodeManager()->mkBagType(typeNode).toType();
+  return Sort(this, type);
+
+  CVC4_API_SOLVER_TRY_CATCH_END;
+}
+
 Sort Solver::mkSequenceSort(Sort elemSort) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
@@ -3645,6 +3697,21 @@ Term Solver::mkEmptySet(Sort s) const
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
+Term Solver::mkEmptyBag(Sort s) const
+{
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4_API_ARG_CHECK_EXPECTED(s.isNull() || s.isBag(), s)
+      << "null sort or bag sort";
+
+  CVC4_API_ARG_CHECK_EXPECTED(s.isNull() || this == s.d_solver, s)
+      << "bag sort associated to this solver object";
+
+  return mkValHelper<CVC4::EmptyBag>(
+      CVC4::EmptyBag(TypeNode::fromType(*s.d_type)));
+
+  CVC4_API_SOLVER_TRY_CATCH_END;
+}
+
 Term Solver::mkSepNil(Sort sort) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 2cb042540..c66113f31 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -387,6 +387,12 @@ class CVC4_PUBLIC Sort
   bool isSet() const;
 
   /**
+   * Is this a Bag sort?
+   * @return true if the sort is a Bag sort
+   */
+  bool isBag() const;
+
+  /**
    * Is this a Sequence sort?
    * @return true if the sort is a Sequence sort
    */
@@ -525,6 +531,13 @@ class CVC4_PUBLIC Sort
    */
   Sort getSetElementSort() const;
 
+  /* Bag sort ------------------------------------------------------------ */
+
+  /**
+   * @return the element sort of a bag sort
+   */
+  Sort getBagElementSort() const;
+
   /* Sequence sort ------------------------------------------------------- */
 
   /**
@@ -2304,6 +2317,13 @@ class CVC4_PUBLIC Solver
   Sort mkSetSort(Sort elemSort) const;
 
   /**
+   * Create a bag sort.
+   * @param elemSort the sort of the bag elements
+   * @return the bag sort
+   */
+  Sort mkBagSort(Sort elemSort) const;
+
+  /**
    * Create a sequence sort.
    * @param elemSort the sort of the sequence elements
    * @return the sequence sort
@@ -2569,6 +2589,13 @@ class CVC4_PUBLIC Solver
   Term mkEmptySet(Sort s) const;
 
   /**
+   * Create a constant representing an empty bag of the given sort.
+   * @param s the sort of the bag elements.
+   * @return the empty bag constant
+   */
+  Term mkEmptyBag(Sort s) const;
+
+  /**
    * Create a separation logic nil term.
    * @param sort the sort of the nil term
    * @return the separation logic nil term
diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h
index 94a212fe5..5910ef1c9 100644
--- a/src/api/cvc4cppkind.h
+++ b/src/api/cvc4cppkind.h
@@ -1964,6 +1964,116 @@ enum CVC4_PUBLIC Kind : int32_t
    *   mkTerm(Kind kind, Term child)
    */
   IS_SINGLETON,
+  /* Bags ------------------------------------------------------------------ */
+  /**
+   * Empty bag constant.
+   * Parameters: 1
+   *   -[1]: Sort of the bag elements
+   * Create with:
+   *   mkEmptyBag(Sort sort)
+   */
+  EMPTYBAG,
+  /**
+   * Bag max union.
+   * Parameters: 2
+   *   -[1]..[2]: Terms of bag sort
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  UNION_MAX,
+  /**
+   * Bag disjoint union (sum).
+   * Parameters: 2
+   *   -[1]..[2]: Terms of bag sort
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  UNION_DISJOINT,
+  /**
+   * Bag intersection (min).
+   * Parameters: 2
+   *   -[1]..[2]: Terms of bag sort
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  INTERSECTION_MIN,
+  /**
+   * Bag difference subtract (subtracts multiplicities of the second from the
+   * first).
+   * Parameters: 2
+   *   -[1]..[2]: Terms of bag sort
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  DIFFERENCE_SUBTRACT,
+  /**
+   * Bag difference 2 (removes shared elements in the two bags).
+   * Parameters: 2
+   *   -[1]..[2]: Terms of bag sort
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  DIFFERENCE_REMOVE,
+  /**
+   * Bag is included (first multiplicities <= second multiplicities).
+   * Parameters: 2
+   *   -[1]..[2]: Terms of set sort
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  BAG_IS_INCLUDED,
+  /**
+   * Element multiplicity in a bag
+   * Parameters: 2
+   *   -[1]..[2]: Terms of bag sort (Bag E), [1] an element of sort E
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  BAG_COUNT,
+  /**
+   * The bag of the single element given as a parameter.
+   * Parameters: 1
+   *   -[1]: Single element
+   * Create with:
+   *   mkTerm(Kind kind, Term child)
+   */
+  MK_BAG,
+  /**
+   * Bag cardinality.
+   * Parameters: 1
+   *   -[1]: Bag to determine the cardinality of
+   * Create with:
+   *   mkTerm(Kind kind, Term child)
+   */
+  BAG_CARD,
+  /**
+   * Returns an element from a given bag.
+   * If a bag A = {(x,n)} where n is the multiplicity, then the term (choose A)
+   * is equivalent to the term x.
+   * If the bag is empty, then (choose A) is an arbitrary value.
+   * If the bag contains distinct elements, then (choose A) will
+   * deterministically return an element in A.
+   * Parameters: 1
+   *   -[1]: Term of bag sort
+   * Create with:
+   *   mkTerm(Kind kind, Term child)
+   */
+  BAG_CHOOSE,
+  /**
+   * Bag is_singleton predicate (single element with multiplicity exactly one).
+   * Parameters: 1
+   *   -[1]: Term of bag sort, is [1] a singleton bag?
+   * Create with:
+   *   mkTerm(Kind kind, Term child)
+   */
+  BAG_IS_SINGLETON,
 
   /* Strings --------------------------------------------------------------- */
 
@@ -2664,6 +2774,8 @@ enum CVC4_PUBLIC Kind : int32_t
   SELECTOR_TYPE,
   /* set type, takes as parameter the type of the elements */
   SET_TYPE,
+  /* bag type, takes as parameter the type of the elements */
+  BAG_TYPE,
   /* sort tag */
   SORT_TAG,
   /* specifies types of user-declared 'uninterpreted' sorts */
diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index 14d84e320..1cc4e9a33 100644
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -21,6 +21,8 @@ libcvc4_add_sources(
   buffered_proof_generator.h
   emptyset.cpp
   emptyset.h
+  emptybag.cpp
+  emptybag.h
   expr_iomanip.cpp
   expr_iomanip.h
   expr_manager_scope.h
diff --git a/src/expr/emptybag.cpp b/src/expr/emptybag.cpp
new file mode 100644
index 000000000..888b3b92a
--- /dev/null
+++ b/src/expr/emptybag.cpp
@@ -0,0 +1,65 @@
+/*********************                                                        */
+/*! \file emptybag.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
+ **/
+
+#include "expr/emptybag.h"
+
+#include <iostream>
+
+#include "expr/type_node.h"
+
+namespace CVC4 {
+
+std::ostream& operator<<(std::ostream& out, const EmptyBag& asa)
+{
+  return out << "emptybag(" << asa.getType() << ')';
+}
+
+size_t EmptyBagHashFunction::operator()(const EmptyBag& es) const
+{
+  return TypeNodeHashFunction()(es.getType());
+}
+
+/**
+ * Constructs an emptybag of the specified type. Note that the argument
+ * is the type of the bag itself, NOT the type of the elements.
+ */
+EmptyBag::EmptyBag(const TypeNode& bagType) : d_type(new TypeNode(bagType)) {}
+
+EmptyBag::EmptyBag(const EmptyBag& es) : d_type(new TypeNode(es.getType())) {}
+
+EmptyBag& EmptyBag::operator=(const EmptyBag& es)
+{
+  (*d_type) = es.getType();
+  return *this;
+}
+
+EmptyBag::~EmptyBag() {}
+const TypeNode& EmptyBag::getType() const { return *d_type; }
+bool EmptyBag::operator==(const EmptyBag& es) const
+{
+  return getType() == es.getType();
+}
+
+bool EmptyBag::operator!=(const EmptyBag& es) const { return !(*this == es); }
+bool EmptyBag::operator<(const EmptyBag& es) const
+{
+  return getType() < es.getType();
+}
+
+bool EmptyBag::operator<=(const EmptyBag& es) const
+{
+  return getType() <= es.getType();
+}
+
+bool EmptyBag::operator>(const EmptyBag& es) const { return !(*this <= es); }
+bool EmptyBag::operator>=(const EmptyBag& es) const { return !(*this < es); }
+}  // namespace CVC4
diff --git a/src/expr/emptybag.h b/src/expr/emptybag.h
new file mode 100644
index 000000000..a16c12d86
--- /dev/null
+++ b/src/expr/emptybag.h
@@ -0,0 +1,63 @@
+/*********************                                                        */
+/*! \file emptybag.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 empty bags
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef CVC4__EMPTY_BAG_H
+#define CVC4__EMPTY_BAG_H
+
+#include <iosfwd>
+#include <memory>
+
+namespace CVC4 {
+
+class TypeNode;
+
+class CVC4_PUBLIC EmptyBag
+{
+ public:
+  /**
+   * Constructs an emptybag of the specified type. Note that the argument
+   * is the type of the bag itself, NOT the type of the elements.
+   */
+  EmptyBag(const TypeNode& bagType);
+  ~EmptyBag();
+  EmptyBag(const EmptyBag& other);
+  EmptyBag& operator=(const EmptyBag& other);
+
+  const TypeNode& getType() const;
+  bool operator==(const EmptyBag& es) const;
+  bool operator!=(const EmptyBag& es) const;
+  bool operator<(const EmptyBag& es) const;
+  bool operator<=(const EmptyBag& es) const;
+  bool operator>(const EmptyBag& es) const;
+  bool operator>=(const EmptyBag& es) const;
+
+ private:
+  EmptyBag();
+
+  /** the type of the empty bag itself (not the type of the elements)*/
+  std::unique_ptr<TypeNode> d_type;
+}; /* class EmptyBag */
+
+std::ostream& operator<<(std::ostream& out, const EmptyBag& es) CVC4_PUBLIC;
+
+struct CVC4_PUBLIC EmptyBagHashFunction
+{
+  size_t operator()(const EmptyBag& es) const;
+}; /* struct EmptyBagHashFunction */
+
+}  // namespace CVC4
+
+#endif /* CVC4__EMPTY_BAG_H */
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 6ac26fbee..3c3d6df4a 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -455,6 +455,18 @@ Node NodeManager::mkSkolem(const std::string& prefix, const TypeNode& type, cons
   return n;
 }
 
+TypeNode NodeManager::mkBagType(TypeNode elementType)
+{
+  CheckArgument(
+      !elementType.isNull(), elementType, "unexpected NULL element type");
+  CheckArgument(elementType.isFirstClass(),
+                elementType,
+                "cannot store types that are not first-class in bags. Try "
+                "option --uf-ho.");
+  Debug("bags") << "making bags type " << elementType << std::endl;
+  return mkTypeNode(kind::BAG_TYPE, elementType);
+}
+
 TypeNode NodeManager::mkSequenceType(TypeNode elementType)
 {
   CheckArgument(
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 0d62e686d..ef22101f0 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -565,13 +565,13 @@ class NodeManager {
 
   /** Create a instantiation constant with the given type. */
   Node mkInstConstant(const TypeNode& type);
-  
+
   /** Create a boolean term variable. */
   Node mkBooleanTermVariable();
 
   /** Make a new abstract value with the given type. */
   Node mkAbstractValue(const TypeNode& type);
-  
+
   /** make unique (per Type,Kind) variable. */
   Node mkNullaryOperator(const TypeNode& type, Kind k);
 
@@ -876,7 +876,7 @@ class NodeManager {
 
   /** Make the type of floating-point with <code>exp</code> bit exponent and
       <code>sig</code> bit significand */
-  inline TypeNode mkFloatingPointType(unsigned exp, unsigned sig);  
+  inline TypeNode mkFloatingPointType(unsigned exp, unsigned sig);
   inline TypeNode mkFloatingPointType(FloatingPointSize fs);
 
   /** Make the type of bitvectors of size <code>size</code> */
@@ -888,6 +888,9 @@ class NodeManager {
   /** Make the type of set with the given parameterization */
   inline TypeNode mkSetType(TypeNode elementType);
 
+  /** Make the type of bags with the given parameterization */
+  TypeNode mkBagType(TypeNode elementType);
+
   /** Make the type of sequences with the given parameterization */
   TypeNode mkSequenceType(TypeNode elementType);
 
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index ba3a26058..cbfb57747 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -692,4 +692,15 @@ const DType& TypeNode::getDType() const
   return (*this)[0].getDType();
 }
 
+bool TypeNode::isBag() const
+{
+  return getKind() == kind::BAG_TYPE;
+}
+
+TypeNode TypeNode::getBagElementType() const
+{
+  Assert(isBag());
+  return (*this)[0];
+}
+
 }/* CVC4 namespace */
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 0f134353a..9ed952369 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -452,7 +452,7 @@ public:
   /**
    * Is this a first-class type?
    * First-class types are types for which:
-   * (1) we handle equalities between terms of that type, and 
+   * (1) we handle equalities between terms of that type, and
    * (2) they are allowed to be parameters of parametric types (e.g. index or element types of arrays).
    *
    * Examples of types that are not first-class include constructor types,
@@ -518,6 +518,9 @@ public:
   /** Is this a Set type? */
   bool isSet() const;
 
+  /** Is this a Bag type? */
+  bool isBag() const;
+
   /** Is this a Sequence type? */
   bool isSequence() const;
 
@@ -539,6 +542,9 @@ public:
   /** Get the element type (for set types) */
   TypeNode getSetElementType() const;
 
+  /** Get the element type (for bag types) */
+  TypeNode getBagElementType() const;
+
   /** Get the element type (for sequence types) */
   TypeNode getSequenceElementType() const;
   /**
@@ -712,7 +718,7 @@ public:
   static TypeNode leastCommonTypeNode(TypeNode t0, TypeNode t1);
   static TypeNode mostCommonTypeNode(TypeNode t0, TypeNode t1);
 
-  /** get ensure type condition 
+  /** get ensure type condition
    *  Return value is a condition that implies that n has type tn.
   */
   static Node getEnsureTypeCondition( Node n, TypeNode tn );
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 1fdf5dda1..31ab49158 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -561,6 +561,10 @@ api::Term Parser::applyTypeAscription(api::Term t, api::Sort s)
   {
     t = d_solver->mkEmptySet(s);
   }
+  else if (k == api::EMPTYBAG)
+  {
+    t = d_solver->mkEmptyBag(s);
+  }
   else if (k == api::CONST_SEQUENCE)
   {
     if (!s.isSequence())
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 6f5d7fbe6..d478163b8 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -680,6 +680,7 @@ public:
    * Return term t with a type ascription applied to it. This is used for
    * syntax like (as t T) in smt2 and t::T in the CVC language. This includes:
    * - (as emptyset (Set T))
+   * - (as emptybag (Bag T))
    * - (as univset (Set T))
    * - (as sep.nil T)
    * - (cons T)
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 417ef5202..65f72eb28 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -2086,7 +2086,15 @@ sortSymbol[CVC4::api::Sort& t, CVC4::parser::DeclarationCheck check]
             PARSER_STATE->parseError("Illegal set type.");
           }
           t = SOLVER->mkSetSort( args[0] );
-        } else if(name == "Seq" && !PARSER_STATE->strictModeEnabled() &&
+        }
+        else if(name == "Bag" &&
+                  PARSER_STATE->isTheoryEnabled(theory::THEORY_BAGS) ) {
+          if(args.size() != 1) {
+            PARSER_STATE->parseError("Illegal bag type.");
+          }
+          t = SOLVER->mkBagSort( args[0] );
+        }
+        else if(name == "Seq" && !PARSER_STATE->strictModeEnabled() &&
                   PARSER_STATE->isTheoryEnabled(theory::THEORY_STRINGS) ) {
           if(args.size() != 1) {
             PARSER_STATE->parseError("Illegal sequence type.");
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 73d4c8c52..387117335 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -691,6 +691,21 @@ Command* Smt2::setLogic(std::string name, bool fromCommand)
     addOperator(api::TCLOSURE, "tclosure");
   }
 
+  if (d_logic.isTheoryEnabled(theory::THEORY_BAGS))
+  {
+    defineVar("emptybag", d_solver->mkEmptyBag(d_solver->getNullSort()));
+    addOperator(api::UNION_MAX, "union_max");
+    addOperator(api::UNION_DISJOINT, "union_disjoint");
+    addOperator(api::INTERSECTION_MIN, "intersection_min");
+    addOperator(api::DIFFERENCE_SUBTRACT, "difference_subtract");
+    addOperator(api::DIFFERENCE_REMOVE, "difference_remove");
+    addOperator(api::BAG_IS_INCLUDED, "bag.is_included");
+    addOperator(api::BAG_COUNT, "bag.count");
+    addOperator(api::MK_BAG, "mkBag");
+    addOperator(api::BAG_CARD, "bag.card");
+    addOperator(api::BAG_CHOOSE, "bag.choose");
+    addOperator(api::BAG_IS_SINGLETON, "bag.is_singleton");
+  }
   if(d_logic.isTheoryEnabled(theory::THEORY_STRINGS)) {
     defineType("String", d_solver->getStringSort());
     defineType("RegLan", d_solver->getRegExpSort());
@@ -821,7 +836,8 @@ void Smt2::checkLogicAllowsFreeSorts()
   if (!d_logic.isTheoryEnabled(theory::THEORY_UF)
       && !d_logic.isTheoryEnabled(theory::THEORY_ARRAYS)
       && !d_logic.isTheoryEnabled(theory::THEORY_DATATYPES)
-      && !d_logic.isTheoryEnabled(theory::THEORY_SETS))
+      && !d_logic.isTheoryEnabled(theory::THEORY_SETS)
+      && !d_logic.isTheoryEnabled(theory::THEORY_BAGS))
   {
     parseErrorLogic("Free sort symbols not allowed in ");
   }
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 1ac7cf0c8..9350111c7 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -283,6 +283,10 @@ void Smt2Printer::toStream(std::ostream& out,
     case kind::EMPTYSET:
       out << "(as emptyset " << n.getConst<EmptySet>().getType() << ")";
       break;
+
+    case kind::EMPTYBAG:
+      out << "(as emptybag " << n.getConst<EmptyBag>().getType() << ")";
+      break;
     case kind::BITVECTOR_EXTRACT_OP:
     {
       BitVectorExtract p = n.getConst<BitVectorExtract>();
@@ -745,6 +749,9 @@ void Smt2Printer::toStream(std::ostream& out,
   case kind::IS_SINGLETON: out << smtKindString(k, d_variant) << " "; break;
   case kind::UNIVERSE_SET:out << "(as univset " << n.getType() << ")";break;
 
+  // bags
+  case kind::BAG_TYPE:  out << smtKindString(k, d_variant) << " "; break;
+
     // fp theory
   case kind::FLOATINGPOINT_FP:
   case kind::FLOATINGPOINT_EQ:
@@ -1151,8 +1158,10 @@ static string smtKindString(Kind k, Variant v)
   case kind::JOIN: return "join";
   case kind::PRODUCT: return "product";
   case kind::TRANSPOSE: return "transpose";
-  case kind::TCLOSURE:
-    return "tclosure";
+  case kind::TCLOSURE: return "tclosure";
+
+  // bag theory
+  case kind::BAG_TYPE: return "Bag";
 
     // fp theory
   case kind::FLOATINGPOINT_FP: return "fp";
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index c1e05b10c..2dc0d52ac 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -561,6 +561,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
       || logic.isTheoryEnabled(THEORY_ARRAYS)
       || logic.isTheoryEnabled(THEORY_DATATYPES)
       || logic.isTheoryEnabled(THEORY_SETS)
+      || logic.isTheoryEnabled(THEORY_BAGS)
       // Non-linear arithmetic requires UF to deal with division/mod because
       // their expansion introduces UFs for the division/mod-by-zero case.
       // If we are eliminating non-linear arithmetic via solve-int-as-bv,
@@ -594,7 +595,8 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   {
     if (logic.isSharingEnabled() && !logic.isTheoryEnabled(THEORY_BV)
         && !logic.isTheoryEnabled(THEORY_STRINGS)
-        && !logic.isTheoryEnabled(THEORY_SETS))
+        && !logic.isTheoryEnabled(THEORY_SETS)
+        && !logic.isTheoryEnabled(THEORY_BAGS))
     {
       Trace("smt") << "setting theoryof-mode to term-based" << std::endl;
       options::theoryOfMode.set(options::TheoryOfMode::THEORY_OF_TERM_BASED);
@@ -1274,7 +1276,9 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     // introduces new literals into the search. This includes quantifiers
     // (quantifier instantiation), and the lemma schemas used in non-linear
     // and sets. We also can't use it if models are enabled.
-    if (logic.isTheoryEnabled(THEORY_SETS) || logic.isQuantified()
+    if (logic.isTheoryEnabled(THEORY_SETS)
+        || logic.isTheoryEnabled(THEORY_BAGS)
+        || logic.isQuantified()
         || options::produceModels() || options::produceAssignments()
         || options::checkModels()
         || (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear()))
diff --git a/src/theory/bags/inference_manager.cpp b/src/theory/bags/inference_manager.cpp
new file mode 100644
index 000000000..4d18ad926
--- /dev/null
+++ b/src/theory/bags/inference_manager.cpp
@@ -0,0 +1,35 @@
+/*********************                                                        */
+/*! \file inference_manager.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 Implementation of the inference manager for the theory of bags
+ **/
+
+#include "theory/bags/inference_manager.h"
+
+using namespace std;
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace bags {
+
+InferenceManager::InferenceManager(Theory& t,
+                                   SolverState& s,
+                                   ProofNodeManager* pnm)
+    : InferenceManagerBuffered(t, s, pnm), d_state(s)
+{
+  d_true = NodeManager::currentNM()->mkConst(true);
+  d_false = NodeManager::currentNM()->mkConst(false);
+}
+
+}  // namespace bags
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/bags/inference_manager.h b/src/theory/bags/inference_manager.h
new file mode 100644
index 000000000..4b4edbaef
--- /dev/null
+++ b/src/theory/bags/inference_manager.h
@@ -0,0 +1,57 @@
+/*********************                                                        */
+/*! \file inference_manager.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 The inference manager for the theory of bags.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__BAGS__INFERENCE_MANAGER_H
+#define CVC4__THEORY__BAGS__INFERENCE_MANAGER_H
+
+#include "theory/bags/solver_state.h"
+#include "theory/inference_manager_buffered.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bags {
+
+/** Inference manager
+ *
+ * This class manages inferences produced by the theory of bags. It manages
+ * whether inferences are processed as external lemmas on the output channel
+ * of theory of bags or internally as literals asserted to the equality engine
+ * of theory of bags. The latter literals are referred to as "facts".
+ */
+class InferenceManager : public InferenceManagerBuffered
+{
+  typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
+
+ public:
+  InferenceManager(Theory& t, SolverState& s, ProofNodeManager* pnm);
+
+ private:
+  /** constants */
+  Node d_true;
+  Node d_false;
+  /**
+   * Reference to the state object for the theory of bags. We store the
+   * (derived) state here, since it has additional methods required in this
+   * class.
+   */
+  SolverState& d_state;
+};
+
+}  // namespace bags
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__BAGS__INFERENCE_MANAGER_H */
diff --git a/src/theory/bags/kinds b/src/theory/bags/kinds
new file mode 100644
index 000000000..8093448a0
--- /dev/null
+++ b/src/theory/bags/kinds
@@ -0,0 +1,79 @@
+# kinds                                                               -*- sh -*-
+#
+# For documentation on this file format, please refer to
+# src/theory/builtin/kinds.
+#
+
+theory THEORY_BAGS \
+    ::CVC4::theory::bags::TheoryBags \
+    "theory/bags/theory_bags.h"
+typechecker "theory/bags/theory_bags_type_rules.h"
+rewriter ::CVC4::theory::bags::TheoryBagsRewriter \
+    "theory/bags/theory_bags_rewriter.h"
+
+properties parametric
+properties check propagate presolve
+
+# constants
+constant EMPTYBAG \
+    ::CVC4::EmptyBag \
+    ::CVC4::EmptyBagHashFunction \
+    "expr/emptybag.h" \
+    "the empty bag constant; payload is an instance of the CVC4::EmptyBag class"
+
+# the type
+operator BAG_TYPE 1 "bag type, takes as parameter the type of the elements"
+cardinality BAG_TYPE \
+    "::CVC4::theory::bags::BagsProperties::computeCardinality(%TYPE%)" \
+    "theory/bags/theory_bags_type_rules.h"
+well-founded BAG_TYPE \
+    "::CVC4::theory::bags::BagsProperties::isWellFounded(%TYPE%)" \
+    "::CVC4::theory::bags::BagsProperties::mkGroundTerm(%TYPE%)" \
+    "theory/bags/theory_bags_type_rules.h"
+enumerator BAG_TYPE \
+    "::CVC4::theory::bags::BagEnumerator" \
+    "theory/bags/theory_bags_type_enumerator.h"
+
+# operators
+operator UNION_MAX         2  "union for bags (max)"
+operator UNION_DISJOINT    2  "disjoint union for bags (sum)"
+operator INTERSECTION_MIN  2  "bag intersection (min)"
+
+# {("a", 2), ("b", 3)} \ {("a", 1)} = {("a", 1), ("b", 3)}
+operator DIFFERENCE_SUBTRACT    2  "bag difference1 (subtracts multiplicities)"
+
+# {("a", 2), ("b", 3)} \\ {("a", 1)} = {("b", 3)}
+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"
+
+# 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"
+
+operator BAG_CARD          1  "bag cardinality operator"
+
+# 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.
+# If the bag is empty, then (choose A) is an arbitrary value.
+# If the bag has cardinality > 1, then (choose A) will deterministically return an element in A.
+operator BAG_CHOOSE        1  "return an element in the bag given as a parameter"
+
+typerule UNION_MAX           ::CVC4::theory::bags::BinaryOperatorTypeRule
+typerule UNION_DISJOINT      ::CVC4::theory::bags::BinaryOperatorTypeRule
+typerule INTERSECTION_MIN    ::CVC4::theory::bags::BinaryOperatorTypeRule
+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              ::CVC4::theory::bags::MkBagTypeRule
+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
+
+construle UNION_DISJOINT     ::CVC4::theory::bags::BinaryOperatorTypeRule
+construle MK_BAG             ::CVC4::theory::bags::MkBagTypeRule
+
+endtheory
\ No newline at end of file
diff --git a/src/theory/bags/normal_form.cpp b/src/theory/bags/normal_form.cpp
new file mode 100644
index 000000000..d9248615b
--- /dev/null
+++ b/src/theory/bags/normal_form.cpp
@@ -0,0 +1,27 @@
+/*************************                                                    */
+/*! \file normal_form.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
+ **/
+
+#include "normal_form.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bags {
+
+bool NormalForm::checkNormalConstant(TNode n)
+{
+  // TODO(projects#223): complete this function
+  return false;
+}
+
+}  // namespace bags
+}  // namespace theory
+}  // namespace CVC4
\ No newline at end of file
diff --git a/src/theory/bags/normal_form.h b/src/theory/bags/normal_form.h
new file mode 100644
index 000000000..73fd8dba8
--- /dev/null
+++ b/src/theory/bags/normal_form.h
@@ -0,0 +1,44 @@
+/*********************                                                        */
+/*! \file normal_form.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 Normal form for bag constants.
+ **/
+
+#include "cvc4_private.h"
+#include <expr/node.h>
+
+#ifndef CVC4__THEORY__BAGS__NORMAL_FORM_H
+#define CVC4__THEORY__BAGS__NORMAL_FORM_H
+
+namespace CVC4 {
+namespace theory {
+namespace bags {
+
+class NormalForm
+{
+ public:
+  /**
+   * Returns true if n is considered a to be a (canonical) constant bag value.
+   * A canonical bag value is one whose AST is:
+   *   (disjoint-union (mk-bag e1 n1) ...
+   *        (disjoint-union (mk-bag e_{n-1} n_{n-1}) (mk-bag e_n n_n))))
+   * where c1 ... cn are constants and the node identifier of these constants
+   * are such that:
+   *   c1 > ... > cn.
+   * Also handles the corner cases of empty bag and singleton bag.
+   */
+  static bool checkNormalConstant(TNode n);
+};
+}  // namespace bags
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__BAGS__NORMAL_FORM_H */
diff --git a/src/theory/bags/solver_state.cpp b/src/theory/bags/solver_state.cpp
new file mode 100644
index 000000000..77204ae76
--- /dev/null
+++ b/src/theory/bags/solver_state.cpp
@@ -0,0 +1,35 @@
+/*********************                                                        */
+/*! \file solver_state.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 Implementation of bags state object
+ **/
+
+#include "theory/bags/solver_state.h"
+
+using namespace std;
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace bags {
+
+SolverState::SolverState(context::Context* c,
+                         context::UserContext* u,
+                         Valuation val)
+    : TheoryState(c, u, val)
+{
+  d_true = NodeManager::currentNM()->mkConst(true);
+  d_false = NodeManager::currentNM()->mkConst(false);
+}
+
+}  // namespace bags
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/bags/solver_state.h b/src/theory/bags/solver_state.h
new file mode 100644
index 000000000..f5b67cb78
--- /dev/null
+++ b/src/theory/bags/solver_state.h
@@ -0,0 +1,44 @@
+/*********************                                                        */
+/*! \file solver_state.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 Bags state object
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__BAGS__THEORY_SOLVER_STATE_H
+#define CVC4__THEORY__BAGS__THEORY_SOLVER_STATE_H
+
+#include <map>
+#include <vector>
+
+#include "theory/theory_state.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bags {
+
+class SolverState : public TheoryState
+{
+ public:
+  SolverState(context::Context* c, context::UserContext* u, Valuation val);
+
+ private:
+  /** constants */
+  Node d_true;
+  Node d_false;
+}; /* class SolverState */
+
+}  // namespace bags
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__BAGS__THEORY_SOLVER_STATE_H */
diff --git a/src/theory/bags/term_registry.cpp b/src/theory/bags/term_registry.cpp
new file mode 100644
index 000000000..60beef29f
--- /dev/null
+++ b/src/theory/bags/term_registry.cpp
@@ -0,0 +1,45 @@
+/*********************                                                        */
+/*! \file term_registry.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 Implementation of bags term registry object
+ **/
+
+#include "theory/bags/term_registry.h"
+
+using namespace std;
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace bags {
+
+TermRegistry::TermRegistry(SolverState& state, InferenceManager& im)
+    : d_im(im),
+      d_proxy(state.getUserContext()),
+      d_proxy_to_term(state.getUserContext())
+{
+}
+
+Node TermRegistry::getEmptyBag(TypeNode tn)
+{
+  std::map<TypeNode, Node>::iterator it = d_emptybag.find(tn);
+  if (it != d_emptybag.end())
+  {
+    return it->second;
+  }
+  Node n = NodeManager::currentNM()->mkConst(EmptySet(tn));
+  d_emptybag[tn] = n;
+  return n;
+}
+
+}  // namespace bags
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/bags/term_registry.h b/src/theory/bags/term_registry.h
new file mode 100644
index 000000000..d284126ee
--- /dev/null
+++ b/src/theory/bags/term_registry.h
@@ -0,0 +1,63 @@
+/*********************                                                        */
+/*! \file term_registry.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 Bags state object
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__BAGS__TERM_REGISTRY_H
+#define CVC4__THEORY__BAGS__TERM_REGISTRY_H
+
+#include <map>
+#include <vector>
+
+#include "context/cdhashmap.h"
+#include "theory/bags/inference_manager.h"
+#include "theory/bags/solver_state.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bags {
+
+/**
+ * Term registry, the purpose of this class is to maintain a database of
+ * commonly used terms, and mappings from bags to their "proxy variables".
+ */
+class TermRegistry
+{
+  typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeMap;
+
+ public:
+  TermRegistry(SolverState& state, InferenceManager& im);
+
+  /**
+   * Returns the existing empty bag for type tn
+   * or creates a new one and returns it.
+   **/
+  Node getEmptyBag(TypeNode tn);
+
+ private:
+  /** The inference manager */
+  InferenceManager& d_im;
+  /** Map from bag terms to their proxy variables */
+  NodeMap d_proxy;
+  /** Backwards map of above */
+  NodeMap d_proxy_to_term;
+  /** Map from types to empty bag of that type */
+  std::map<TypeNode, Node> d_emptybag;
+}; /* class Term */
+
+}  // namespace bags
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__BAGS__TERM_REGISTRY_H */
diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp
new file mode 100644
index 000000000..5ddd17302
--- /dev/null
+++ b/src/theory/bags/theory_bags.cpp
@@ -0,0 +1,139 @@
+/*********************                                                        */
+/*! \file theory_bags.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 Bags theory.
+ **/
+
+#include "theory/bags/theory_bags.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace bags {
+
+TheoryBags::TheoryBags(context::Context* c,
+                       context::UserContext* u,
+                       OutputChannel& out,
+                       Valuation valuation,
+                       const LogicInfo& logicInfo,
+                       ProofNodeManager* pnm)
+    : Theory(THEORY_BAGS, c, u, out, valuation, logicInfo, pnm),
+      d_state(c, u, valuation),
+      d_im(*this, d_state, pnm),
+      d_rewriter(),
+      d_notify(*this, d_im)
+{
+  // use the official theory state and inference manager objects
+  d_theoryState = &d_state;
+  d_inferManager = &d_im;
+}
+
+TheoryBags::~TheoryBags() {}
+
+TheoryRewriter* TheoryBags::getTheoryRewriter() { return &d_rewriter; }
+
+bool TheoryBags::needsEqualityEngine(EeSetupInfo& esi)
+{
+  esi.d_notify = &d_notify;
+  esi.d_name = "theory::bags::ee";
+  return true;
+}
+
+void TheoryBags::finishInit()
+{
+  Assert(d_equalityEngine != nullptr);
+
+  // choice is used to eliminate witness
+  d_valuation.setUnevaluatedKind(WITNESS);
+
+  // functions we are doing congruence over
+  d_equalityEngine->addFunctionKind(UNION_MAX);
+  d_equalityEngine->addFunctionKind(UNION_DISJOINT);
+  d_equalityEngine->addFunctionKind(INTERSECTION_MIN);
+  d_equalityEngine->addFunctionKind(DIFFERENCE_SUBTRACT);
+  d_equalityEngine->addFunctionKind(DIFFERENCE_REMOVE);
+  d_equalityEngine->addFunctionKind(BAG_COUNT);
+  d_equalityEngine->addFunctionKind(MK_BAG);
+  d_equalityEngine->addFunctionKind(BAG_CARD);
+}
+
+void TheoryBags::postCheck(Effort level) {}
+
+void TheoryBags::notifyFact(TNode atom,
+                            bool polarity,
+                            TNode fact,
+                            bool isInternal)
+{
+}
+
+bool TheoryBags::collectModelValues(TheoryModel* m,
+                                    const std::set<Node>& termBag)
+{
+  return true;
+}
+
+TrustNode TheoryBags::explain(TNode node) { return d_im.explainLit(node); }
+
+Node TheoryBags::getModelValue(TNode node) { return Node::null(); }
+
+void TheoryBags::preRegisterTerm(TNode node) {}
+
+TrustNode TheoryBags::expandDefinition(Node n)
+{
+  // TODO(projects#224): add choose and is_singleton here
+  return TrustNode::null();
+}
+
+void TheoryBags::presolve() {}
+
+/**************************** eq::NotifyClass *****************************/
+
+void TheoryBags::eqNotifyNewClass(TNode t)
+{
+  Assert(false) << "Not implemented yet" << std::endl;
+}
+
+void TheoryBags::eqNotifyMerge(TNode t1, TNode t2)
+{
+  Assert(false) << "Not implemented yet" << std::endl;
+}
+
+void TheoryBags::eqNotifyDisequal(TNode t1, TNode t2, TNode reason)
+{
+  Assert(false) << "Not implemented yet" << std::endl;
+}
+
+void TheoryBags::NotifyClass::eqNotifyNewClass(TNode t)
+{
+  Debug("bags-eq") << "[bags-eq] eqNotifyNewClass:"
+                   << " t = " << t << std::endl;
+  d_theory.eqNotifyNewClass(t);
+}
+
+void TheoryBags::NotifyClass::eqNotifyMerge(TNode t1, TNode t2)
+{
+  Debug("bags-eq") << "[bags-eq] eqNotifyMerge:"
+                   << " t1 = " << t1 << " t2 = " << t2 << std::endl;
+  d_theory.eqNotifyMerge(t1, t2);
+}
+
+void TheoryBags::NotifyClass::eqNotifyDisequal(TNode t1, TNode t2, TNode reason)
+{
+  Debug("bags-eq") << "[bags-eq] eqNotifyDisequal:"
+                   << " t1 = " << t1 << " t2 = " << t2 << " reason = " << reason
+                   << std::endl;
+  d_theory.eqNotifyDisequal(t1, t2, reason);
+}
+
+}  // namespace bags
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/bags/theory_bags.h b/src/theory/bags/theory_bags.h
new file mode 100644
index 000000000..44f7ae1b0
--- /dev/null
+++ b/src/theory/bags/theory_bags.h
@@ -0,0 +1,110 @@
+/*********************                                                        */
+/*! \file theory_bags.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 Bags theory.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__BAGS__THEORY_BAGS_H
+#define CVC4__THEORY__BAGS__THEORY_BAGS_H
+
+#include <memory>
+
+#include "theory/bags/inference_manager.h"
+#include "theory/bags/solver_state.h"
+#include "theory/bags/theory_bags_rewriter.h"
+#include "theory/theory.h"
+#include "theory/theory_eq_notify.h"
+#include "theory/uf/equality_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bags {
+
+class TheoryBags : public Theory
+{
+ public:
+  /** Constructs a new instance of TheoryBags w.r.t. the provided contexts. */
+  TheoryBags(context::Context* c,
+             context::UserContext* u,
+             OutputChannel& out,
+             Valuation valuation,
+             const LogicInfo& logicInfo,
+             ProofNodeManager* pnm);
+  ~TheoryBags() override;
+
+  //--------------------------------- initialization
+  /** get the official theory rewriter of this theory */
+  TheoryRewriter* getTheoryRewriter() override;
+  /**
+   * Returns true if we need an equality engine. If so, we initialize the
+   * information regarding how it should be setup. For details, see the
+   * documentation in Theory::needsEqualityEngine.
+   */
+  bool needsEqualityEngine(EeSetupInfo& esi) override;
+  /** finish initialization */
+  void finishInit() override;
+  //--------------------------------- end initialization
+
+  //--------------------------------- standard check
+  /** Post-check, called after the fact queue of the theory is processed. */
+  void postCheck(Effort level) override;
+  /** Notify fact */
+  void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) override;
+  //--------------------------------- end standard check
+  /** Collect model values in m based on the relevant terms given by termSet */
+  bool collectModelValues(TheoryModel* m,
+                          const std::set<Node>& termSet) override;
+  TrustNode explain(TNode) override;
+  Node getModelValue(TNode) override;
+  std::string identify() const override { return "THEORY_BAGS"; }
+  void preRegisterTerm(TNode node) override;
+  TrustNode expandDefinition(Node n) override;
+  void presolve() override;
+
+ private:
+  /** Functions to handle callbacks from equality engine */
+  class NotifyClass : public TheoryEqNotifyClass
+  {
+   public:
+    NotifyClass(TheoryBags& theory, TheoryInferenceManager& inferenceManager)
+
+        : TheoryEqNotifyClass(inferenceManager), d_theory(theory)
+    {
+    }
+    void eqNotifyNewClass(TNode t) override;
+    void eqNotifyMerge(TNode t1, TNode t2) override;
+    void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override;
+
+   private:
+    TheoryBags& d_theory;
+  };
+
+  /** The state of the bags solver at full effort */
+  SolverState d_state;
+  /** The inference manager */
+  InferenceManager d_im;
+  /** Instance of the above class */
+  NotifyClass d_notify;
+  /** The theory rewriter for this theory. */
+  TheoryBagsRewriter d_rewriter;
+
+  void eqNotifyNewClass(TNode t);
+  void eqNotifyMerge(TNode t1, TNode t2);
+  void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
+}; /* class TheoryBags */
+
+}  // namespace bags
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__BAGS__THEORY_BAGS_H */
diff --git a/src/theory/bags/theory_bags_rewriter.cpp b/src/theory/bags/theory_bags_rewriter.cpp
new file mode 100644
index 000000000..aaf0ab98c
--- /dev/null
+++ b/src/theory/bags/theory_bags_rewriter.cpp
@@ -0,0 +1,37 @@
+/*********************                                                        */
+/*! \file theory_bags_rewriter.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 Bags theory rewriter.
+ **/
+
+#include "theory/bags/theory_bags_rewriter.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace bags {
+
+RewriteResponse TheoryBagsRewriter::postRewrite(TNode node)
+{
+  // TODO(projects#225): complete the code here
+  return RewriteResponse(REWRITE_DONE, node);
+}
+
+RewriteResponse TheoryBagsRewriter::preRewrite(TNode node)
+{
+  // TODO(projects#225): complete the code here
+  return RewriteResponse(REWRITE_DONE, node);
+}
+
+}  // namespace bags
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/bags/theory_bags_rewriter.h b/src/theory/bags/theory_bags_rewriter.h
new file mode 100644
index 000000000..7be88636a
--- /dev/null
+++ b/src/theory/bags/theory_bags_rewriter.h
@@ -0,0 +1,38 @@
+/*********************                                                        */
+/*! \file theory_bags_rewriter.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 Bags theory rewriter.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__BAGS__THEORY_BAGS_REWRITER_H
+#define CVC4__THEORY__BAGS__THEORY_BAGS_REWRITER_H
+
+#include "theory/rewriter.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bags {
+
+class TheoryBagsRewriter : public TheoryRewriter
+{
+ public:
+  RewriteResponse postRewrite(TNode node) override;
+
+  RewriteResponse preRewrite(TNode node) override;
+}; /* class TheoryBagsRewriter */
+
+}  // namespace bags
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__BAGS__THEORY_BAGS_REWRITER_H */
diff --git a/src/theory/bags/theory_bags_type_enumerator.cpp b/src/theory/bags/theory_bags_type_enumerator.cpp
new file mode 100644
index 000000000..7975bb379
--- /dev/null
+++ b/src/theory/bags/theory_bags_type_enumerator.cpp
@@ -0,0 +1,85 @@
+/*********************                                                        */
+/*! \file theory_bags_type_enumerator.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 bag enumerator implementation
+ **/
+
+#include "theory/bags/theory_bags_type_enumerator.h"
+
+#include "expr/emptybag.h"
+#include "theory/rewriter.h"
+#include "theory_bags_type_enumerator.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bags {
+
+BagEnumerator::BagEnumerator(TypeNode type, TypeEnumeratorProperties* tep)
+    : TypeEnumeratorBase<BagEnumerator>(type),
+      d_nodeManager(NodeManager::currentNM()),
+      d_elementTypeEnumerator(type.getBagElementType(), tep)
+{
+  d_currentBag = d_nodeManager->mkConst(EmptyBag(type));
+  d_element = *d_elementTypeEnumerator;
+}
+
+BagEnumerator::BagEnumerator(const BagEnumerator& enumerator)
+    : TypeEnumeratorBase<BagEnumerator>(enumerator.getType()),
+      d_nodeManager(enumerator.d_nodeManager),
+      d_elementTypeEnumerator(enumerator.d_elementTypeEnumerator),
+      d_currentBag(enumerator.d_currentBag),
+      d_element(enumerator.d_element)
+{
+}
+
+BagEnumerator::~BagEnumerator() {}
+
+Node BagEnumerator::operator*()
+{
+  Trace("bag-type-enum") << "BagEnumerator::operator* d_currentBag = "
+                         << d_currentBag << std::endl;
+
+  return d_currentBag;
+}
+
+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);
+  if (d_currentBag.getKind() == kind::EMPTYBAG)
+  {
+    d_currentBag = singleton;
+  }
+  else
+  {
+    d_currentBag =
+        d_nodeManager->mkNode(kind::UNION_DISJOINT, singleton, d_currentBag);
+  }
+
+  d_currentBag = Rewriter::rewrite(d_currentBag);
+
+  Assert(d_currentBag.isConst());
+
+  Trace("bag-type-enum") << "BagEnumerator::operator++ d_currentBag = "
+                         << d_currentBag << std::endl;
+  return *this;
+}
+
+bool BagEnumerator::isFinished()
+{
+  // bags sequence is infinite and it never ends
+  return false;
+}
+
+}  // namespace bags
+}  // namespace theory
+}  // namespace CVC4
\ No newline at end of file
diff --git a/src/theory/bags/theory_bags_type_enumerator.h b/src/theory/bags/theory_bags_type_enumerator.h
new file mode 100644
index 000000000..26639afd8
--- /dev/null
+++ b/src/theory/bags/theory_bags_type_enumerator.h
@@ -0,0 +1,91 @@
+/*********************                                                        */
+/*! \file theory_bags_type_enumerator.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 type enumerator for bags
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__BAGS__TYPE_ENUMERATOR_H
+#define CVC4__THEORY__BAGS__TYPE_ENUMERATOR_H
+
+#include "expr/type_node.h"
+#include "theory/type_enumerator.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bags {
+
+class BagEnumerator : public TypeEnumeratorBase<BagEnumerator>
+{
+ public:
+  BagEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr);
+  BagEnumerator(const BagEnumerator& enumerator);
+  ~BagEnumerator();
+
+  Node operator*() override;
+
+  /**
+   * This operator iterates over the infinite bags constructed from the element
+   * type . Ideally iterating over bags of {1, 2, 3, ...} will return the
+   * following infinite sequence of bags, where n in the pair (m, n) means the
+   * multiplicity of the element m in the bag
+   * {},                    sum = 0, #elements = 0, cardinality = 0
+   *
+   * {(1,1)},               sum = 2, #elements = 1, cardinality = 1
+   *
+   * {(2,1)},               sum = 3, #elements = 2, cardinality = 1
+   * {(1,2)},               sum = 3, #elements = 2, cardinality = 2
+   *
+   * {(3, 1)},              sum = 4, #elements = 3, cardinality = 1
+   * {(2, 2)},              sum = 4, #elements = 3, cardinality = 2
+   * {(1, 3)},              sum = 4, #elements = 3, cardinality = 3
+   *
+   * {(4, 1)},              sum = 5, #elements = 4, cardinality = 1
+   * {(3, 2)},              sum = 5, #elements = 4, cardinality = 2
+   * {(1, 1),(2, 1)},       sum = 5, #elements = 4, cardinality = 2
+   * {(2, 3)},              sum = 5, #elements = 4, cardinality = 3
+   * {(1, 4)},              sum = 5, #elements = 4, cardinality = 4
+   *
+   * {(5, 1)},              sum = 6, #elements = 5, cardinality = 1
+   * {(4, 2)},              sum = 6, #elements = 5, cardinality = 2
+   * {(1, 1), (3,1)},       sum = 6, #elements = 5, cardinality = 2
+   * {(3, 3)},              sum = 6, #elements = 5, cardinality = 3
+   * {(1, 1), (2,2)},       sum = 6, #elements = 5, cardinality = 3
+   * {(1, 2), (2,1)},       sum = 6, #elements = 5, cardinality = 3
+   * {(2, 4)},              sum = 6, #elements = 5, cardinality = 4
+   * {(1, 5)},              sum = 6, #elements = 5, cardinality = 5
+   *
+   * This seems too expensive to implement.
+   * For now we are implementing an obvious solution
+   * {(1,1)}, {(1,2)}, {(1,3)}, ... which works for both fininte and infinite
+   * types
+   */
+  BagEnumerator& operator++() override;
+
+  bool isFinished() override;
+
+ private:
+  /** a pointer to the node manager */
+  NodeManager* d_nodeManager;
+  /** an enumerator for the set of pairs of element type x integer type */
+  TypeEnumerator d_elementTypeEnumerator;
+  /** the current set returned by the set enumerator */
+  Node d_currentBag;
+  /** the first value returned by the element type enumerator*/
+  Node d_element;
+}; /* class BagEnumerator */
+
+}  // namespace bags
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__BAGS__TYPE_ENUMERATOR_H */
\ No newline at end of file
diff --git a/src/theory/bags/theory_bags_type_rules.h b/src/theory/bags/theory_bags_type_rules.h
new file mode 100644
index 000000000..fc5a19348
--- /dev/null
+++ b/src/theory/bags/theory_bags_type_rules.h
@@ -0,0 +1,255 @@
+/*********************                                                        */
+/*! \file theory_bags_type_rules.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Mudathir Mohamed
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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 Bags theory type rules.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__BAGS__THEORY_BAGS_TYPE_RULES_H
+#define CVC4__THEORY__BAGS__THEORY_BAGS_TYPE_RULES_H
+
+#include "theory/bags/normal_form.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bags {
+
+struct BinaryOperatorTypeRule
+{
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+  {
+    Assert(n.getKind() == kind::UNION_MAX || n.getKind() == kind::UNION_DISJOINT
+           || n.getKind() == kind::INTERSECTION_MIN
+           || n.getKind() == kind::DIFFERENCE_SUBTRACT
+           || n.getKind() == kind::DIFFERENCE_REMOVE);
+    TypeNode bagType = n[0].getType(check);
+    if (check)
+    {
+      if (!bagType.isBag())
+      {
+        throw TypeCheckingExceptionPrivate(
+            n, "operator expects a bag, first argument is not");
+      }
+      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");
+        }
+      }
+    }
+    return bagType;
+  }
+
+  static bool computeIsConst(NodeManager* nodeManager, TNode n)
+  {
+    // only UNION_DISJOINT has a const rule in kinds.
+    // Other binary operators do not have const rules in kinds
+    Assert(n.getKind() == kind::UNION_DISJOINT);
+    return NormalForm::checkNormalConstant(n);
+  }
+}; /* struct BinaryOperatorTypeRule */
+
+struct IsIncludedTypeRule
+{
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+  {
+    Assert(n.getKind() == kind::BAG_IS_INCLUDED);
+    TypeNode bagType = n[0].getType(check);
+    if (check)
+    {
+      if (!bagType.isBag())
+      {
+        throw TypeCheckingExceptionPrivate(
+            n, "BAG_IS_INCLUDED operating on non-bag");
+      }
+      TypeNode secondBagType = n[1].getType(check);
+      if (secondBagType != bagType)
+      {
+        if (!bagType.isComparableTo(secondBagType))
+        {
+          throw TypeCheckingExceptionPrivate(
+              n, "BAG_IS_INCLUDED operating on bags of different types");
+        }
+      }
+    }
+    return nodeManager->booleanType();
+  }
+}; /* struct IsIncludedTypeRule */
+
+struct CountTypeRule
+{
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+  {
+    Assert(n.getKind() == kind::BAG_COUNT);
+    TypeNode bagType = n[1].getType(check);
+    if (check)
+    {
+      if (!bagType.isBag())
+      {
+        throw TypeCheckingExceptionPrivate(
+            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()))
+      {
+        std::stringstream ss;
+        ss << "member operating on bags of different types:\n"
+           << "child type:  " << elementType << "\n"
+           << "not subtype: " << bagType.getBagElementType() << "\n"
+           << "in term : " << n;
+        throw TypeCheckingExceptionPrivate(n, ss.str());
+      }
+    }
+    return nodeManager->integerType();
+  }
+}; /* struct CountTypeRule */
+
+struct MkBagTypeRule
+{
+  static TypeNode computeType(NodeManager* nm, TNode n, bool check)
+  {
+    Assert(n.getKind() == kind::MK_BAG);
+    if (check)
+    {
+      if (n.getNumChildren() != 2)
+      {
+        std::stringstream ss;
+        ss << "operands in term " << n << " are " << n.getNumChildren()
+           << ", but MK_BAG expects 2 operands.";
+        throw TypeCheckingExceptionPrivate(n, ss.str());
+      }
+      TypeNode type1 = n[1].getType(check);
+      if (!type1.isInteger())
+      {
+        std::stringstream ss;
+        ss << "MK_BAG expects an integer for " << n[1] << ". Found" << type1;
+        throw TypeCheckingExceptionPrivate(n, ss.str());
+      }
+    }
+
+    return nm->mkBagType(n[0].getType(check));
+  }
+
+  static bool computeIsConst(NodeManager* nodeManager, TNode n)
+  {
+    Assert(n.getKind() == kind::MK_BAG);
+    // for a bag to be a constant, both the element and its multiplicity should
+    // be constants, and the multiplicity should be > 0.
+    return n[0].isConst() && n[1].isConst()
+           && n[1].getConst<Rational>().sgn() == 1;
+  }
+}; /* struct MkBagTypeRule */
+
+struct IsSingletonTypeRule
+{
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+  {
+    Assert(n.getKind() == kind::BAG_IS_SINGLETON);
+    TypeNode bagType = n[0].getType(check);
+    if (check)
+    {
+      if (!bagType.isBag())
+      {
+        throw TypeCheckingExceptionPrivate(
+            n, "BAG_IS_SINGLETON operator expects a bag, a non-bag is found");
+      }
+    }
+    return nodeManager->booleanType();
+  }
+}; /* struct IsMkBagTypeRule */
+
+struct EmptyBagTypeRule
+{
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+  {
+    Assert(n.getKind() == kind::EMPTYBAG);
+    EmptyBag emptyBag = n.getConst<EmptyBag>();
+    return emptyBag.getType();
+  }
+}; /* struct EmptyBagTypeRule */
+
+struct CardTypeRule
+{
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+  {
+    Assert(n.getKind() == kind::BAG_CARD);
+    TypeNode bagType = n[0].getType(check);
+    if (check)
+    {
+      if (!bagType.isBag())
+      {
+        throw TypeCheckingExceptionPrivate(
+            n, "cardinality operates on a bag, non-bag object found");
+      }
+    }
+    return nodeManager->integerType();
+  }
+}; /* struct CardTypeRule */
+
+struct ChooseTypeRule
+{
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+  {
+    Assert(n.getKind() == kind::BAG_CHOOSE);
+    TypeNode bagType = n[0].getType(check);
+    if (check)
+    {
+      if (!bagType.isBag())
+      {
+        throw TypeCheckingExceptionPrivate(
+            n, "CHOOSE operator expects a bag, a non-bag is found");
+      }
+    }
+    return bagType.getBagElementType();
+  }
+}; /* struct ChooseTypeRule */
+
+struct BagsProperties
+{
+  static Cardinality computeCardinality(TypeNode type)
+  {
+    return Cardinality::UNKNOWN_CARD;
+  }
+
+  static bool isWellFounded(TypeNode type) { return type[0].isWellFounded(); }
+
+  static Node mkGroundTerm(TypeNode type)
+  {
+    Assert(type.isBag());
+    return NodeManager::currentNM()->mkConst(EmptyBag(type));
+  }
+}; /* struct BagsProperties */
+
+}  // namespace bags
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__BAGS__THEORY_BAGS_TYPE_RULES_H */
diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp
index 4bbbdc322..73cd920d2 100644
--- a/src/theory/logic_info.cpp
+++ b/src/theory/logic_info.cpp
@@ -338,6 +338,11 @@ std::string LogicInfo::getLogicString() const {
         ss << "FS";
         ++seen;
       }
+      if (d_theories[THEORY_BAGS])
+      {
+        ss << "FB";
+        ++seen;
+      }
       if(seen != d_sharingTheories) {
         Unhandled()
             << "can't extract a logic string from LogicInfo; at least one "
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 2d32b34d4..a425441fd 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -82,6 +82,7 @@ namespace theory {
   CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_DATATYPES) \
   CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_SEP)       \
   CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_SETS)      \
+  CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_BAGS)      \
   CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_STRINGS)   \
   CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_QUANTIFIERS)
 
diff --git a/src/theory/theory_id.cpp b/src/theory/theory_id.cpp
index 5c11c340a..31b864e7f 100644
--- a/src/theory/theory_id.cpp
+++ b/src/theory/theory_id.cpp
@@ -43,6 +43,7 @@ std::ostream& operator<<(std::ostream& out, TheoryId theoryId)
     case THEORY_SAT_SOLVER: out << "THEORY_SAT_SOLVER"; break;
     case THEORY_SEP: out << "THEORY_SEP"; break;
     case THEORY_SETS: out << "THEORY_SETS"; break;
+    case THEORY_BAGS: out << "THEORY_BAGS"; break;
     case THEORY_STRINGS: out << "THEORY_STRINGS"; break;
     case THEORY_QUANTIFIERS: out << "THEORY_QUANTIFIERS"; break;
 
@@ -65,6 +66,7 @@ std::string getStatsPrefix(TheoryId theoryId)
     case THEORY_DATATYPES: return "theory::datatypes"; break;
     case THEORY_SEP: return "theory::sep"; break;
     case THEORY_SETS: return "theory::sets"; break;
+    case THEORY_BAGS: return "theory::bags"; break;
     case THEORY_STRINGS: return "theory::strings"; break;
     case THEORY_QUANTIFIERS: return "theory::quantifiers"; break;
 
diff --git a/src/theory/theory_id.h b/src/theory/theory_id.h
index 60e005cf7..e0dfaa507 100644
--- a/src/theory/theory_id.h
+++ b/src/theory/theory_id.h
@@ -42,6 +42,7 @@ enum TheoryId
   THEORY_DATATYPES,
   THEORY_SEP,
   THEORY_SETS,
+  THEORY_BAGS,
   THEORY_STRINGS,
   THEORY_QUANTIFIERS,