From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Tue, 20 Apr 2021 22:33:39 +0000 (-0700)
Subject: Quantifiers: Move implementation of type rules to cpp. (#6404)
X-Git-Tag: cvc5-1.0.0~1876
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9cb7212d58d42cf1433dc086d305f1a202c3771b;p=cvc5.git

Quantifiers: Move implementation of type rules to cpp. (#6404)
---

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index c24ab31ec..b86e59877 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -877,6 +877,7 @@ libcvc4_add_sources(
   theory/quantifiers/term_util.h
   theory/quantifiers/theory_quantifiers.cpp
   theory/quantifiers/theory_quantifiers.h
+  theory/quantifiers/theory_quantifiers_type_rules.cpp
   theory/quantifiers/theory_quantifiers_type_rules.h
   theory/quantifiers_engine.cpp
   theory/quantifiers_engine.h
diff --git a/src/theory/quantifiers/theory_quantifiers_type_rules.cpp b/src/theory/quantifiers/theory_quantifiers_type_rules.cpp
new file mode 100644
index 000000000..6fb377a56
--- /dev/null
+++ b/src/theory/quantifiers/theory_quantifiers_type_rules.cpp
@@ -0,0 +1,137 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Morgan Deters, Tim King
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Theory of quantifiers.
+ */
+
+#include "theory/quantifiers/theory_quantifiers_type_rules.h"
+
+namespace cvc5 {
+namespace theory {
+namespace quantifiers {
+
+TypeNode QuantifierTypeRule::computeType(NodeManager* nodeManager,
+                                         TNode n,
+                                         bool check)
+{
+  Debug("typecheck-q") << "type check for fa " << n << std::endl;
+  Assert((n.getKind() == kind::FORALL || n.getKind() == kind::EXISTS)
+         && n.getNumChildren() > 0);
+  if (check)
+  {
+    if (n[0].getType(check) != nodeManager->boundVarListType())
+    {
+      throw TypeCheckingExceptionPrivate(
+          n, "first argument of quantifier is not bound var list");
+    }
+    if (n[1].getType(check) != nodeManager->booleanType())
+    {
+      throw TypeCheckingExceptionPrivate(n,
+                                         "body of quantifier is not boolean");
+    }
+    if (n.getNumChildren() == 3)
+    {
+      if (n[2].getType(check) != nodeManager->instPatternListType())
+      {
+        throw TypeCheckingExceptionPrivate(
+            n,
+            "third argument of quantifier is not instantiation "
+            "pattern list");
+      }
+      for (const Node& p : n[2])
+      {
+        if (p.getKind() == kind::INST_POOL
+            && p.getNumChildren() != n[0].getNumChildren())
+        {
+          throw TypeCheckingExceptionPrivate(
+              n,
+              "expected number of arguments to pool to be the same as the "
+              "number of bound variables of the quantified formula");
+        }
+      }
+    }
+  }
+  return nodeManager->booleanType();
+}
+
+TypeNode QuantifierBoundVarListTypeRule::computeType(NodeManager* nodeManager,
+                                                     TNode n,
+                                                     bool check)
+{
+  Assert(n.getKind() == kind::BOUND_VAR_LIST);
+  if (check)
+  {
+    for (int i = 0; i < (int)n.getNumChildren(); i++)
+    {
+      if (n[i].getKind() != kind::BOUND_VARIABLE)
+      {
+        throw TypeCheckingExceptionPrivate(
+            n, "argument of bound var list is not bound variable");
+      }
+    }
+  }
+  return nodeManager->boundVarListType();
+}
+
+TypeNode QuantifierInstPatternTypeRule::computeType(NodeManager* nodeManager,
+                                                    TNode n,
+                                                    bool check)
+{
+  Assert(n.getKind() == kind::INST_PATTERN);
+  if (check)
+  {
+    TypeNode tn = n[0].getType(check);
+    // this check catches the common mistake writing :pattern (f x) instead of
+    // :pattern ((f x))
+    if (n[0].isVar() && n[0].getKind() != kind::BOUND_VARIABLE
+        && tn.isFunction())
+    {
+      throw TypeCheckingExceptionPrivate(
+          n[0], "Pattern must be a list of fully-applied terms.");
+    }
+  }
+  return nodeManager->instPatternType();
+}
+
+TypeNode QuantifierAnnotationTypeRule::computeType(NodeManager* nodeManager,
+                                                   TNode n,
+                                                   bool check)
+{
+  return nodeManager->instPatternType();
+}
+
+TypeNode QuantifierInstPatternListTypeRule::computeType(
+    NodeManager* nodeManager, TNode n, bool check)
+{
+  Assert(n.getKind() == kind::INST_PATTERN_LIST);
+  if (check)
+  {
+    for (const Node& nc : n)
+    {
+      Kind k = nc.getKind();
+      if (k != kind::INST_PATTERN && k != kind::INST_NO_PATTERN
+          && k != kind::INST_ATTRIBUTE && k != kind::INST_POOL
+          && k != kind::INST_ADD_TO_POOL && k != kind::SKOLEM_ADD_TO_POOL)
+      {
+        throw TypeCheckingExceptionPrivate(
+            n,
+            "argument of inst pattern list is not a legal quantifiers "
+            "annotation");
+      }
+    }
+  }
+  return nodeManager->instPatternListType();
+}
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/theory_quantifiers_type_rules.h b/src/theory/quantifiers/theory_quantifiers_type_rules.h
index 7783c65d6..80d7b0e03 100644
--- a/src/theory/quantifiers/theory_quantifiers_type_rules.h
+++ b/src/theory/quantifiers/theory_quantifiers_type_rules.h
@@ -27,106 +27,28 @@ namespace quantifiers {
 
 struct QuantifierTypeRule
 {
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    Debug("typecheck-q") << "type check for fa " << n << std::endl;
-    Assert((n.getKind() == kind::FORALL || n.getKind() == kind::EXISTS)
-           && n.getNumChildren() > 0);
-    if( check ){
-      if( n[ 0 ].getType(check)!=nodeManager->boundVarListType() ){
-        throw TypeCheckingExceptionPrivate(
-            n, "first argument of quantifier is not bound var list");
-      }
-      if( n[ 1 ].getType(check)!=nodeManager->booleanType() ){
-        throw TypeCheckingExceptionPrivate(n,
-                                           "body of quantifier is not boolean");
-      }
-      if (n.getNumChildren() == 3)
-      {
-        if (n[2].getType(check) != nodeManager->instPatternListType())
-        {
-          throw TypeCheckingExceptionPrivate(
-              n,
-              "third argument of quantifier is not instantiation "
-              "pattern list");
-        }
-        for (const Node& p : n[2])
-        {
-          if (p.getKind() == kind::INST_POOL
-              && p.getNumChildren() != n[0].getNumChildren())
-          {
-            throw TypeCheckingExceptionPrivate(
-                n,
-                "expected number of arguments to pool to be the same as the "
-                "number of bound variables of the quantified formula");
-          }
-        }
-      }
-    }
-    return nodeManager->booleanType();
-  }
-}; /* struct QuantifierTypeRule */
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
+};
 
-struct QuantifierBoundVarListTypeRule {
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    Assert(n.getKind() == kind::BOUND_VAR_LIST);
-    if( check ){
-      for( int i=0; i<(int)n.getNumChildren(); i++ ){
-        if( n[i].getKind()!=kind::BOUND_VARIABLE ){
-          throw TypeCheckingExceptionPrivate(n, "argument of bound var list is not bound variable");
-        }
-      }
-    }
-    return nodeManager->boundVarListType();
-  }
-};/* struct QuantifierBoundVarListTypeRule */
+struct QuantifierBoundVarListTypeRule
+{
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
+};
 
-struct QuantifierInstPatternTypeRule {
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    Assert(n.getKind() == kind::INST_PATTERN);
-    if( check ){
-      TypeNode tn = n[0].getType(check);
-      // this check catches the common mistake writing :pattern (f x) instead of :pattern ((f x))
-      if( n[0].isVar() && n[0].getKind()!=kind::BOUND_VARIABLE && tn.isFunction() ){
-        throw TypeCheckingExceptionPrivate(n[0], "Pattern must be a list of fully-applied terms.");
-      }
-    }
-    return nodeManager->instPatternType();
-  }
-};/* struct QuantifierInstPatternTypeRule */
+struct QuantifierInstPatternTypeRule
+{
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
+};
 
 struct QuantifierAnnotationTypeRule
 {
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    return nodeManager->instPatternType();
-  }
-}; /* struct QuantifierAnnotationTypeRule */
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
+};
 
-struct QuantifierInstPatternListTypeRule {
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    Assert(n.getKind() == kind::INST_PATTERN_LIST);
-    if( check ){
-      for (const Node& nc : n)
-      {
-        Kind k = nc.getKind();
-        if (k != kind::INST_PATTERN && k != kind::INST_NO_PATTERN
-            && k != kind::INST_ATTRIBUTE && k != kind::INST_POOL
-            && k != kind::INST_ADD_TO_POOL && k != kind::SKOLEM_ADD_TO_POOL)
-        {
-          throw TypeCheckingExceptionPrivate(
-              n,
-              "argument of inst pattern list is not a legal quantifiers "
-              "annotation");
-        }
-      }
-    }
-    return nodeManager->instPatternListType();
-  }
-};/* struct QuantifierInstPatternListTypeRule */
+struct QuantifierInstPatternListTypeRule
+{
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
+};
 
 }  // namespace quantifiers
 }  // namespace theory