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

diff --git a/src/theory/bags/theory_bags_type_rules.cpp b/src/theory/bags/theory_bags_type_rules.cpp
index 66117d64a171bf433c07cc0e307858d81955751e..133059cd066bfb3456bf3f8e94dd45f7c04c4590 100644 (file)
--- 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 06cc74e2ae0959c5c78593430e2b7d6f8947cc62..4e4fe071610ffd948dcd65c1af9740d818cd2c76 100644 (file)
--- 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