Bags: Move more implementation of type rule from header to .cpp. (#6336)

2 files changed, 14 insertions, 7 deletions

diff --git a/src/theory/bags/theory_bags_type_rules.cpp b/src/theory/bags/theory_bags_type_rules.cpp
index 66117d64a..133059cd0 100644
--- a/src/theory/bags/theory_bags_type_rules.cpp
+++ b/src/theory/bags/theory_bags_type_rules.cpp
@@ -278,6 +278,17 @@ TypeNode ToSetTypeRule::computeType(NodeManager* nodeManager,
   TypeNode setType = nodeManager->mkSetType(elementType);
   return setType;
 }
+
+bool BagsProperties::isWellFounded(TypeNode type)
+{
+  return type[0].isWellFounded();
+}
+
+Node BagsProperties::mkGroundTerm(TypeNode type)
+{
+  Assert(type.isBag());
+  return NodeManager::currentNM()->mkConst(EmptyBag(type));
+}
 }  // namespace bags
 }  // namespace theory
 }  // namespace cvc5
diff --git a/src/theory/bags/theory_bags_type_rules.h b/src/theory/bags/theory_bags_type_rules.h
index 06cc74e2a..4e4fe0716 100644
--- a/src/theory/bags/theory_bags_type_rules.h
+++ b/src/theory/bags/theory_bags_type_rules.h
@@ -19,11 +19,11 @@
 #define CVC5__THEORY__BAGS__THEORY_BAGS_TYPE_RULES_H
 
 #include "expr/node.h"
-#include "expr/type_node.h"
 
 namespace cvc5 {
 
 class NodeManager;
+class TypeNode;
 
 namespace theory {
 namespace bags {
@@ -130,13 +130,9 @@ struct BagsProperties
     return Cardinality::INTEGERS;
   }
 
-  static bool isWellFounded(TypeNode type) { return type[0].isWellFounded(); }
+  static bool isWellFounded(TypeNode type);
 
-  static Node mkGroundTerm(TypeNode type)
-  {
-    Assert(type.isBag());
-    return NodeManager::currentNM()->mkConst(EmptyBag(type));
-  }
+  static Node mkGroundTerm(TypeNode type);
 }; /* struct BagsProperties */
 
 }  // namespace bags