Sep: Move implementation of type rules to cpp. (#6402)

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index b86e5987707566d3a9dd6d43093b79cc308d86db..81e598f2bafde017374f330a41abafe7349561ea 100644 (file)
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -892,6 +892,7 @@ libcvc4_add_sources(
   theory/sep/theory_sep.h
   theory/sep/theory_sep_rewriter.cpp
   theory/sep/theory_sep_rewriter.h
+  theory/sep/theory_sep_type_rules.cpp
   theory/sep/theory_sep_type_rules.h
   theory/sets/cardinality_extension.cpp
   theory/sets/cardinality_extension.h

diff --git a/src/theory/sep/theory_sep_type_rules.cpp b/src/theory/sep/theory_sep_type_rules.cpp
new file mode 100644 (file)
index 0000000..28dfa5c
--- /dev/null
+++ b/src/theory/sep/theory_sep_type_rules.cpp
@@ -0,0 +1,120 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Tim King, Mathias Preiner
+ *
+ * This file is part of the cvc5 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.
+ * ****************************************************************************
+ *
+ * Typing and cardinality rules for the theory of sep.
+ */
+
+#include "theory/sep/theory_sep_type_rules.h"
+
+namespace cvc5 {
+namespace theory {
+namespace sep {
+
+TypeNode SepEmpTypeRule::computeType(NodeManager* nodeManager,
+                                     TNode n,
+                                     bool check)
+{
+  Assert(n.getKind() == kind::SEP_EMP);
+  return nodeManager->booleanType();
+}
+
+TypeNode SepPtoTypeRule::computeType(NodeManager* nodeManager,
+                                     TNode n,
+                                     bool check)
+{
+  Assert(n.getKind() == kind::SEP_PTO);
+  if (check)
+  {
+    TypeNode refType = n[0].getType(check);
+    TypeNode ptType = n[1].getType(check);
+  }
+  return nodeManager->booleanType();
+}
+
+TypeNode SepStarTypeRule::computeType(NodeManager* nodeManager,
+                                      TNode n,
+                                      bool check)
+{
+  TypeNode btype = nodeManager->booleanType();
+  Assert(n.getKind() == kind::SEP_STAR);
+  if (check)
+  {
+    for (unsigned i = 0; i < n.getNumChildren(); i++)
+    {
+      TypeNode ctype = n[i].getType(check);
+      if (ctype != btype)
+      {
+        throw TypeCheckingExceptionPrivate(n,
+                                           "child of sep star is not Boolean");
+      }
+    }
+  }
+  return btype;
+}
+
+TypeNode SepWandTypeRule::computeType(NodeManager* nodeManager,
+                                      TNode n,
+                                      bool check)
+{
+  TypeNode btype = nodeManager->booleanType();
+  Assert(n.getKind() == kind::SEP_WAND);
+  if (check)
+  {
+    for (unsigned i = 0; i < n.getNumChildren(); i++)
+    {
+      TypeNode ctype = n[i].getType(check);
+      if (ctype != btype)
+      {
+        throw TypeCheckingExceptionPrivate(
+            n, "child of sep magic wand is not Boolean");
+      }
+    }
+  }
+  return btype;
+}
+
+TypeNode SepLabelTypeRule::computeType(NodeManager* nodeManager,
+                                       TNode n,
+                                       bool check)
+{
+  TypeNode btype = nodeManager->booleanType();
+  Assert(n.getKind() == kind::SEP_LABEL);
+  if (check)
+  {
+    TypeNode ctype = n[0].getType(check);
+    if (ctype != btype)
+    {
+      throw TypeCheckingExceptionPrivate(n,
+                                         "child of sep label is not Boolean");
+    }
+    TypeNode stype = n[1].getType(check);
+    if (!stype.isSet())
+    {
+      throw TypeCheckingExceptionPrivate(n, "label of sep label is not a set");
+    }
+  }
+  return btype;
+}
+
+TypeNode SepNilTypeRule::computeType(NodeManager* nodeManager,
+                                     TNode n,
+                                     bool check)
+{
+  Assert(n.getKind() == kind::SEP_NIL);
+  Assert(check);
+  TypeNode type = n.getType();
+  return type;
+}
+
+}  // namespace sep
+}  // namespace theory
+}  // namespace cvc5

diff --git a/src/theory/sep/theory_sep_type_rules.h b/src/theory/sep/theory_sep_type_rules.h
index 676cb8d9dc5c4a5bdcf33ef77d1475ae507db161..f437ba2d7a734906e6042cc8e0ea741beb8c55f2 100644 (file)
--- a/src/theory/sep/theory_sep_type_rules.h
+++ b/src/theory/sep/theory_sep_type_rules.h
@@ -18,93 +18,43 @@
 #ifndef CVC5__THEORY__SEP__THEORY_SEP_TYPE_RULES_H
 #define CVC5__THEORY__SEP__THEORY_SEP_TYPE_RULES_H
 
+#include "expr/node.h"
+#include "expr/type_node.h"
+
 namespace cvc5 {
 namespace theory {
 namespace sep {
 
-class SepEmpTypeRule {
-public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    Assert(n.getKind() == kind::SEP_EMP);
-    return nodeManager->booleanType();
-  }
+class SepEmpTypeRule
+{
+ public:
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
-struct SepPtoTypeRule {
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    Assert(n.getKind() == kind::SEP_PTO);
-    if( check ) {
-      TypeNode refType = n[0].getType(check);
-      TypeNode ptType = n[1].getType(check);
-    }
-    return nodeManager->booleanType();
-  }
-};/* struct SepSelectTypeRule */
+struct SepPtoTypeRule
+{
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
+};
 
-struct SepStarTypeRule {
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    TypeNode btype = nodeManager->booleanType();
-    Assert(n.getKind() == kind::SEP_STAR);
-    if( check ){
-      for( unsigned i=0; i<n.getNumChildren(); i++ ){
-        TypeNode ctype = n[i].getType( check );
-        if( ctype!=btype ){
-          throw TypeCheckingExceptionPrivate(n, "child of sep star is not Boolean");
-        }
-      }
-    }
-    return btype;
-  }
-};/* struct SepStarTypeRule */
+struct SepStarTypeRule
+{
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
+};
 
-struct SepWandTypeRule {
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    TypeNode btype = nodeManager->booleanType();
-    Assert(n.getKind() == kind::SEP_WAND);
-    if( check ){
-      for( unsigned i=0; i<n.getNumChildren(); i++ ){
-        TypeNode ctype = n[i].getType( check );
-        if( ctype!=btype ){
-          throw TypeCheckingExceptionPrivate(n, "child of sep magic wand is not Boolean");
-        }
-      }
-    }
-    return btype;
-  }
-};/* struct SepWandTypeRule */
+struct SepWandTypeRule
+{
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
+};
 
-struct SepLabelTypeRule {
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    TypeNode btype = nodeManager->booleanType();
-    Assert(n.getKind() == kind::SEP_LABEL);
-    if( check ){
-      TypeNode ctype = n[0].getType( check );
-      if( ctype!=btype ){
-        throw TypeCheckingExceptionPrivate(n, "child of sep label is not Boolean");
-      }
-      TypeNode stype = n[1].getType( check );
-      if( !stype.isSet() ){
-        throw TypeCheckingExceptionPrivate(n, "label of sep label is not a set");
-      }
-    }
-    return btype;
-  }
-};/* struct SepLabelTypeRule */
+struct SepLabelTypeRule
+{
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
+};
 
-struct SepNilTypeRule {
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    Assert(n.getKind() == kind::SEP_NIL);
-    Assert(check);
-    TypeNode type = n.getType();
-    return type;
-  }
-};/* struct SepLabelTypeRule */
+struct SepNilTypeRule
+{
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
+};
 
 }  // namespace sep
 }  // namespace theory