From d5023d8b814b177651d4bb8d09b5818c90fbc7f0 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Mon, 12 Apr 2021 18:33:55 -0700 Subject: [PATCH] Bags: Move more implementation of type rule from header to .cpp. (#6336) --- src/theory/bags/theory_bags_type_rules.cpp | 11 +++++++++++ src/theory/bags/theory_bags_type_rules.h | 10 +++------- 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 -- 2.30.2