Bool: Move implementation of type rules to cpp. (#6420)

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 95fa90fe35e6d3ef9c345f3b12711d554cbaa87a..c03c2d591b0c32a7f3d1f952a6350ab34c7c0a9e 100644 (file)
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -498,6 +498,7 @@ libcvc5_add_sources(
   theory/booleans/theory_bool.h
   theory/booleans/theory_bool_rewriter.cpp
   theory/booleans/theory_bool_rewriter.h
+  theory/booleans/theory_bool_type_rules.cpp
   theory/booleans/theory_bool_type_rules.h
   theory/booleans/type_enumerator.h
   theory/builtin/proof_checker.cpp

diff --git a/src/theory/arrays/theory_arrays_type_rules.cpp b/src/theory/arrays/theory_arrays_type_rules.cpp
index e0c27419fef390df49e8e5587c76afacd1f7ef28..04a2f1a742da47eb48e4d711de5abbe88d45f3df 100644 (file)
--- a/src/theory/arrays/theory_arrays_type_rules.cpp
+++ b/src/theory/arrays/theory_arrays_type_rules.cpp
@@ -15,7 +15,8 @@
 
 #include "theory/arrays/theory_arrays_type_rules.h"
 
-#include "theory/arrays/theory_arrays_rewriter.h"  // for array-constant attributes
+// for array-constant attributes
+#include "theory/arrays/theory_arrays_rewriter.h"
 #include "theory/type_enumerator.h"
 
 namespace cvc5 {

diff --git a/src/theory/booleans/theory_bool_type_rules.cpp b/src/theory/booleans/theory_bool_type_rules.cpp
new file mode 100644 (file)
index 0000000..11210a8
--- /dev/null
+++ b/src/theory/booleans/theory_bool_type_rules.cpp
@@ -0,0 +1,76 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Dejan Jovanovic, Morgan Deters, Christopher L. Conway
+ *
+ * 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 boolean.
+ */
+
+#include "theory/booleans/theory_bool_type_rules.h"
+
+#include <sstream>
+
+namespace cvc5 {
+namespace theory {
+namespace boolean {
+
+TypeNode BooleanTypeRule::computeType(NodeManager* nodeManager,
+                                      TNode n,
+                                      bool check)
+{
+  TypeNode booleanType = nodeManager->booleanType();
+  if (check)
+  {
+    for (const auto& child : n)
+    {
+      if (!child.getType(check).isBoolean())
+      {
+        Debug("pb") << "failed type checking: " << child << std::endl;
+        Debug("pb") << "  integer: " << child.getType(check).isInteger()
+                    << std::endl;
+        Debug("pb") << "  real: " << child.getType(check).isReal() << std::endl;
+        throw TypeCheckingExceptionPrivate(n,
+                                           "expecting a Boolean subexpression");
+      }
+    }
+  }
+  return booleanType;
+}
+
+TypeNode IteTypeRule::computeType(NodeManager* nodeManager, TNode n, bool check)
+{
+  TypeNode thenType = n[1].getType(check);
+  TypeNode elseType = n[2].getType(check);
+  TypeNode iteType = TypeNode::leastCommonTypeNode(thenType, elseType);
+  if (check)
+  {
+    TypeNode booleanType = nodeManager->booleanType();
+    if (n[0].getType(check) != booleanType)
+    {
+      throw TypeCheckingExceptionPrivate(n, "condition of ITE is not Boolean");
+    }
+    if (iteType.isNull())
+    {
+      std::stringstream ss;
+      ss << "Both branches of the ITE must be a subtype of a common type."
+         << std::endl
+         << "then branch: " << n[1] << std::endl
+         << "its type   : " << thenType << std::endl
+         << "else branch: " << n[2] << std::endl
+         << "its type   : " << elseType << std::endl;
+      throw TypeCheckingExceptionPrivate(n, ss.str());
+    }
+  }
+  return iteType;
+}
+
+}  // namespace boolean
+}  // namespace theory
+}  // namespace cvc5

diff --git a/src/theory/booleans/theory_bool_type_rules.h b/src/theory/booleans/theory_bool_type_rules.h
index 6c9aea0ae7ebb6e5ac9a9a03033f013f0c26621b..6d8eb0a6def7b83aeb75e63038403a1afdb9655c 100644 (file)
--- a/src/theory/booleans/theory_bool_type_rules.h
+++ b/src/theory/booleans/theory_bool_type_rules.h
@@ -10,9 +10,7 @@
  * directory for licensing information.
  * ****************************************************************************
  *
- * [[ Add brief comments here ]]
- *
- * [[ Add file-specific comments here ]]
+ * Typing and cardinality rules for the theory of boolean.
  */
 
 #include "cvc5_private.h"
@@ -20,56 +18,24 @@
 #ifndef CVC5__THEORY_BOOL_TYPE_RULES_H
 #define CVC5__THEORY_BOOL_TYPE_RULES_H
 
+#include "expr/node.h"
+#include "expr/type_node.h"
+
 namespace cvc5 {
 namespace theory {
 namespace boolean {
 
-class BooleanTypeRule {
-public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    TypeNode booleanType = nodeManager->booleanType();
-    if( check ) {
-      TNode::iterator child_it = n.begin();
-      TNode::iterator child_it_end = n.end();
-      for(; child_it != child_it_end; ++child_it) {
-        if(!(*child_it).getType(check).isBoolean()) {
-          Debug("pb") << "failed type checking: " << *child_it << std::endl;
-          Debug("pb") << "  integer: " << (*child_it).getType(check).isInteger() << std::endl;
-          Debug("pb") << "  real: " << (*child_it).getType(check).isReal() << std::endl;
-          throw TypeCheckingExceptionPrivate(n, "expecting a Boolean subexpression");
-        }
-      }
-    }
-    return booleanType;
-  }
-};/* class BooleanTypeRule */
+class BooleanTypeRule
+{
+ public:
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
+};
 
-class IteTypeRule {
-public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    TypeNode thenType = n[1].getType(check);
-    TypeNode elseType = n[2].getType(check);
-    TypeNode iteType = TypeNode::leastCommonTypeNode(thenType, elseType);
-    if( check ) {
-      TypeNode booleanType = nodeManager->booleanType();
-      if (n[0].getType(check) != booleanType) {
-        throw TypeCheckingExceptionPrivate(n, "condition of ITE is not Boolean");
-      }
-      if (iteType.isNull()) {
-        std::stringstream ss;
-        ss << "Both branches of the ITE must be a subtype of a common type." << std::endl
-           << "then branch: " << n[1] << std::endl
-           << "its type   : " << thenType << std::endl
-           << "else branch: " << n[2] << std::endl
-           << "its type   : " << elseType << std::endl;
-        throw TypeCheckingExceptionPrivate(n, ss.str());
-      }
-    }
-    return iteType;
-  }
-};/* class IteTypeRule */
+class IteTypeRule
+{
+ public:
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
+};
 
 }  // namespace boolean
 }  // namespace theory