From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Tue, 13 Apr 2021 01:33:55 +0000 (-0700)
Subject: Bags: Move more implementation of type rule from header to .cpp. (#6336)
X-Git-Tag: cvc5-1.0.0~1920
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d5023d8b814b177651d4bb8d09b5818c90fbc7f0;p=cvc5.git

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 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