Bags: Move implementation of type rules from header to .cpp file. (#6247)

3 files changed, 301 insertions, 225 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 645cf3c79..4e2113c51 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -490,6 +490,7 @@ libcvc4_add_sources(
   theory/bags/theory_bags_type_enumerator.cpp
   theory/bags/theory_bags_type_enumerator.h
   theory/bags/theory_bags_type_rules.h
+  theory/bags/theory_bags_type_rules.cpp
   theory/booleans/circuit_propagator.cpp
   theory/booleans/circuit_propagator.h
   theory/booleans/proof_circuit_propagator.cpp
diff --git a/src/theory/bags/theory_bags_type_rules.cpp b/src/theory/bags/theory_bags_type_rules.cpp
new file mode 100644
index 000000000..5a97155fc
--- /dev/null
+++ b/src/theory/bags/theory_bags_type_rules.cpp
@@ -0,0 +1,282 @@
+/*********************                                                        */
+/*! \file theory_bags_type_rules.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Mudathir Mohamed
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 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 "theory/bags/theory_bags_type_rules.h"
+
+#include <sstream>
+
+#include "base/check.h"
+#include "theory/bags/normal_form.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bags {
+
+TypeNode BinaryOperatorTypeRule::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)
+    {
+      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;
+}
+
+bool BinaryOperatorTypeRule::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::isConstant(n);
+}
+
+TypeNode SubBagTypeRule::computeType(NodeManager* nodeManager,
+                                     TNode n,
+                                     bool check)
+{
+  Assert(n.getKind() == kind::SUBBAG);
+  TypeNode bagType = n[0].getType(check);
+  if (check)
+  {
+    if (!bagType.isBag())
+    {
+      throw TypeCheckingExceptionPrivate(n, "SUBBAG operating on non-bag");
+    }
+    TypeNode secondBagType = n[1].getType(check);
+    if (secondBagType != bagType)
+    {
+      if (!bagType.isComparableTo(secondBagType))
+      {
+        throw TypeCheckingExceptionPrivate(
+            n, "SUBBAG operating on bags of different types");
+      }
+    }
+  }
+  return nodeManager->booleanType();
+}
+
+TypeNode CountTypeRule::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);
+    // 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"
+         << "child type:  " << elementType << "\n"
+         << "not subtype: " << bagType.getBagElementType() << "\n"
+         << "in term : " << n;
+      throw TypeCheckingExceptionPrivate(n, ss.str());
+    }
+  }
+  return nodeManager->integerType();
+}
+
+TypeNode DuplicateRemovalTypeRule::computeType(NodeManager* nodeManager,
+                                               TNode n,
+                                               bool check)
+{
+  Assert(n.getKind() == kind::DUPLICATE_REMOVAL);
+  TypeNode bagType = n[0].getType(check);
+  if (check)
+  {
+    if (!bagType.isBag())
+    {
+      std::stringstream ss;
+      ss << "Applying DUPLICATE_REMOVAL on a non-bag argument in term " << n;
+      throw TypeCheckingExceptionPrivate(n, ss.str());
+    }
+  }
+  return bagType;
+}
+
+TypeNode MkBagTypeRule::computeType(NodeManager* nm, TNode n, bool check)
+{
+  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)
+    {
+      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());
+    }
+
+    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(expectedElementType);
+}
+
+bool MkBagTypeRule::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;
+}
+
+TypeNode IsSingletonTypeRule::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();
+}
+
+TypeNode EmptyBagTypeRule::computeType(NodeManager* nodeManager,
+                                       TNode n,
+                                       bool check)
+{
+  Assert(n.getKind() == kind::EMPTYBAG);
+  EmptyBag emptyBag = n.getConst<EmptyBag>();
+  return emptyBag.getType();
+}
+
+TypeNode CardTypeRule::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();
+}
+
+TypeNode ChooseTypeRule::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();
+}
+
+TypeNode FromSetTypeRule::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;
+}
+
+TypeNode ToSetTypeRule::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;
+}
+}  // namespace bags
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/bags/theory_bags_type_rules.h b/src/theory/bags/theory_bags_type_rules.h
index f55cfcc88..41e1164c2 100644
--- a/src/theory/bags/theory_bags_type_rules.h
+++ b/src/theory/bags/theory_bags_type_rules.h
@@ -17,278 +17,71 @@
 #ifndef CVC4__THEORY__BAGS__THEORY_BAGS_TYPE_RULES_H
 #define CVC4__THEORY__BAGS__THEORY_BAGS_TYPE_RULES_H
 
-#include "theory/bags/normal_form.h"
+#include "expr/node.h"
+#include "expr/type_node.h"
 
 namespace CVC4 {
+
+class NodeManager;
+
 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)
-      {
-        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;
-  }
-
-  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::isConstant(n);
-  }
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
+  static bool computeIsConst(NodeManager* nodeManager, TNode n);
 }; /* struct BinaryOperatorTypeRule */
 
 struct SubBagTypeRule
 {
-  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    Assert(n.getKind() == kind::SUBBAG);
-    TypeNode bagType = n[0].getType(check);
-    if (check)
-    {
-      if (!bagType.isBag())
-      {
-        throw TypeCheckingExceptionPrivate(n, "SUBBAG operating on non-bag");
-      }
-      TypeNode secondBagType = n[1].getType(check);
-      if (secondBagType != bagType)
-      {
-        if (!bagType.isComparableTo(secondBagType))
-        {
-          throw TypeCheckingExceptionPrivate(
-              n, "SUBBAG operating on bags of different types");
-        }
-      }
-    }
-    return nodeManager->booleanType();
-  }
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 }; /* struct SubBagTypeRule */
 
 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);
-      // 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"
-           << "child type:  " << elementType << "\n"
-           << "not subtype: " << bagType.getBagElementType() << "\n"
-           << "in term : " << n;
-        throw TypeCheckingExceptionPrivate(n, ss.str());
-      }
-    }
-    return nodeManager->integerType();
-  }
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 }; /* struct CountTypeRule */
 
 struct DuplicateRemovalTypeRule
 {
-  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    Assert(n.getKind() == kind::DUPLICATE_REMOVAL);
-    TypeNode bagType = n[0].getType(check);
-    if (check)
-    {
-      if (!bagType.isBag())
-      {
-        std::stringstream ss;
-        ss << "Applying DUPLICATE_REMOVAL on a non-bag argument in term " << n;
-        throw TypeCheckingExceptionPrivate(n, ss.str());
-      }
-    }
-    return bagType;
-  }
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 }; /* struct DuplicateRemovalTypeRule */
 
 struct MkBagTypeRule
 {
-  static TypeNode computeType(NodeManager* nm, TNode n, bool check)
-  {
-    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)
-      {
-        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());
-      }
-
-      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(expectedElementType);
-  }
-
-  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;
-  }
+  static TypeNode computeType(NodeManager* nm, TNode n, bool check);
+  static bool computeIsConst(NodeManager* nodeManager, TNode n);
 }; /* 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();
-  }
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 }; /* 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();
-  }
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 }; /* 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();
-  }
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 }; /* 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();
-  }
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 }; /* 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;
-  }
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 }; /* 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;
-  }
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 }; /* struct ToSetTypeRule */
 
 struct BagsProperties