Arithmetic: Move implementation of type rules to cpp. (#6419)

3 files changed, 184 insertions, 127 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 052e65adb..7d7aca8e8 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -436,6 +436,7 @@ libcvc5_add_sources(
   theory/arith/theory_arith.h
   theory/arith/theory_arith_private.cpp
   theory/arith/theory_arith_private.h
+  theory/arith/theory_arith_type_rules.cpp
   theory/arith/theory_arith_type_rules.h
   theory/arith/type_enumerator.h
   theory/arrays/array_info.cpp
diff --git a/src/theory/arith/theory_arith_type_rules.cpp b/src/theory/arith/theory_arith_type_rules.cpp
new file mode 100644
index 000000000..ba4c7dcb5
--- /dev/null
+++ b/src/theory/arith/theory_arith_type_rules.cpp
@@ -0,0 +1,158 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Gereon Kremer, Dejan Jovanovic
+ *
+ * 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 theory arithmetic.
+ */
+
+#include "theory/arith/theory_arith_type_rules.h"
+
+namespace cvc5 {
+namespace theory {
+namespace arith {
+
+TypeNode ArithConstantTypeRule::computeType(NodeManager* nodeManager,
+                                            TNode n,
+                                            bool check)
+{
+  Assert(n.getKind() == kind::CONST_RATIONAL);
+  if (n.getConst<Rational>().isIntegral())
+  {
+    return nodeManager->integerType();
+  }
+  else
+  {
+    return nodeManager->realType();
+  }
+}
+
+TypeNode ArithOperatorTypeRule::computeType(NodeManager* nodeManager,
+                                            TNode n,
+                                            bool check)
+{
+  TypeNode integerType = nodeManager->integerType();
+  TypeNode realType = nodeManager->realType();
+  TNode::iterator child_it = n.begin();
+  TNode::iterator child_it_end = n.end();
+  bool isInteger = true;
+  Kind k = n.getKind();
+  for (; child_it != child_it_end; ++child_it)
+  {
+    TypeNode childType = (*child_it).getType(check);
+    if (!childType.isInteger())
+    {
+      isInteger = false;
+      if (!check)
+      {  // if we're not checking, nothing left to do
+        break;
+      }
+    }
+    if (check)
+    {
+      if (!childType.isReal())
+      {
+        throw TypeCheckingExceptionPrivate(n,
+                                           "expecting an arithmetic subterm");
+      }
+      if (k == kind::TO_REAL && !childType.isInteger())
+      {
+        throw TypeCheckingExceptionPrivate(n, "expecting an integer subterm");
+      }
+    }
+  }
+  switch (k)
+  {
+    case kind::TO_REAL:
+    case kind::CAST_TO_REAL: return realType;
+    case kind::TO_INTEGER: return integerType;
+    default:
+    {
+      bool isDivision = k == kind::DIVISION || k == kind::DIVISION_TOTAL;
+      return (isInteger && !isDivision ? integerType : realType);
+    }
+  }
+}
+
+TypeNode RealNullaryOperatorTypeRule::computeType(NodeManager* nodeManager,
+                                                  TNode n,
+                                                  bool check)
+{
+  // for nullary operators, we only computeType for check=true, since they are
+  // given TypeAttr() on creation
+  Assert(check);
+  TypeNode realType = n.getType();
+  if (realType != NodeManager::currentNM()->realType())
+  {
+    throw TypeCheckingExceptionPrivate(n, "expecting real type");
+  }
+  return realType;
+}
+
+TypeNode IAndOpTypeRule::computeType(NodeManager* nodeManager,
+                                     TNode n,
+                                     bool check)
+{
+  if (n.getKind() != kind::IAND_OP)
+  {
+    InternalError() << "IAND_OP typerule invoked for IAND_OP kind";
+  }
+  TypeNode iType = nodeManager->integerType();
+  std::vector<TypeNode> argTypes;
+  argTypes.push_back(iType);
+  argTypes.push_back(iType);
+  return nodeManager->mkFunctionType(argTypes, iType);
+}
+
+TypeNode IAndTypeRule::computeType(NodeManager* nodeManager,
+                                   TNode n,
+                                   bool check)
+{
+  if (n.getKind() != kind::IAND)
+  {
+    InternalError() << "IAND typerule invoked for IAND kind";
+  }
+  if (check)
+  {
+    TypeNode arg1 = n[0].getType(check);
+    TypeNode arg2 = n[1].getType(check);
+    if (!arg1.isInteger() || !arg2.isInteger())
+    {
+      throw TypeCheckingExceptionPrivate(n, "expecting integer terms");
+    }
+  }
+  return nodeManager->integerType();
+}
+
+TypeNode IndexedRootPredicateTypeRule::computeType(NodeManager* nodeManager,
+                                                   TNode n,
+                                                   bool check)
+{
+  if (check)
+  {
+    TypeNode t1 = n[0].getType(check);
+    if (!t1.isBoolean())
+    {
+      throw TypeCheckingExceptionPrivate(
+          n, "expecting boolean term as first argument");
+    }
+    TypeNode t2 = n[1].getType(check);
+    if (!t2.isReal())
+    {
+      throw TypeCheckingExceptionPrivate(
+          n, "expecting polynomial as second argument");
+    }
+  }
+  return nodeManager->booleanType();
+}
+
+}  // namespace arith
+}  // namespace theory
+}  // namespace cvc5
diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h
index 2d56a26c7..f7ef64e2d 100644
--- a/src/theory/arith/theory_arith_type_rules.h
+++ b/src/theory/arith/theory_arith_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 theory arithmetic.
  */
 
 #include "cvc5_private.h"
@@ -20,148 +18,48 @@
 #ifndef CVC5__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H
 #define CVC5__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H
 
+#include "expr/node.h"
+#include "expr/type_node.h"
+
 namespace cvc5 {
 namespace theory {
 namespace arith {
 
+class ArithConstantTypeRule
+{
+ public:
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
+};
 
-class ArithConstantTypeRule {
-public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    Assert(n.getKind() == kind::CONST_RATIONAL);
-    if(n.getConst<Rational>().isIntegral()){
-      return nodeManager->integerType();
-    }else{
-      return nodeManager->realType();
-    }
-  }
-};/* class ArithConstantTypeRule */
-
-class ArithOperatorTypeRule {
-public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    TypeNode integerType = nodeManager->integerType();
-    TypeNode realType = nodeManager->realType();
-    TNode::iterator child_it = n.begin();
-    TNode::iterator child_it_end = n.end();
-    bool isInteger = true;
-    Kind k = n.getKind();
-    for(; child_it != child_it_end; ++child_it) {
-      TypeNode childType = (*child_it).getType(check);
-      if (!childType.isInteger()) {
-        isInteger = false;
-        if( !check ) { // if we're not checking, nothing left to do
-          break;
-        }
-      }
-      if( check ) {
-        if(!childType.isReal()) {
-          throw TypeCheckingExceptionPrivate(n, "expecting an arithmetic subterm");
-        }
-        if (k == kind::TO_REAL && !childType.isInteger())
-        {
-          throw TypeCheckingExceptionPrivate(n, "expecting an integer subterm");
-        }
-      }
-    }
-    switch (k)
-    {
-      case kind::TO_REAL:
-      case kind::CAST_TO_REAL: return realType;
-      case kind::TO_INTEGER: return integerType;
-      default:
-      {
-        bool isDivision = k == kind::DIVISION || k == kind::DIVISION_TOTAL;
-        return (isInteger && !isDivision ? integerType : realType);
-      }
-    }
-  }
-};/* class ArithOperatorTypeRule */
+class ArithOperatorTypeRule
+{
+ public:
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
+};
 
-class RealNullaryOperatorTypeRule {
-public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    // for nullary operators, we only computeType for check=true, since they are given TypeAttr() on creation
-    Assert(check);
-    TypeNode realType = n.getType();
-    if(realType!=NodeManager::currentNM()->realType()) {
-      throw TypeCheckingExceptionPrivate(n, "expecting real type");
-    }
-    return realType;
-  }
-};/* class RealNullaryOperatorTypeRule */
+class RealNullaryOperatorTypeRule
+{
+ public:
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
+};
 
 class IAndOpTypeRule
 {
  public:
-  inline static TypeNode computeType(NodeManager* nodeManager,
-                                     TNode n,
-                                     bool check)
-  {
-    if (n.getKind() != kind::IAND_OP)
-    {
-      InternalError() << "IAND_OP typerule invoked for IAND_OP kind";
-    }
-    TypeNode iType = nodeManager->integerType();
-    std::vector<TypeNode> argTypes;
-    argTypes.push_back(iType);
-    argTypes.push_back(iType);
-    return nodeManager->mkFunctionType(argTypes, iType);
-  }
-}; /* class IAndOpTypeRule */
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
+};
 
 class IAndTypeRule
 {
  public:
-  inline static TypeNode computeType(NodeManager* nodeManager,
-                                     TNode n,
-                                     bool check)
-  {
-    if (n.getKind() != kind::IAND)
-    {
-      InternalError() << "IAND typerule invoked for IAND kind";
-    }
-    if (check)
-    {
-      TypeNode arg1 = n[0].getType(check);
-      TypeNode arg2 = n[1].getType(check);
-      if (!arg1.isInteger() || !arg2.isInteger())
-      {
-        throw TypeCheckingExceptionPrivate(n, "expecting integer terms");
-      }
-    }
-    return nodeManager->integerType();
-  }
-}; /* class BitVectorConversionTypeRule */
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
+};
 
 class IndexedRootPredicateTypeRule
 {
  public:
-  inline static TypeNode computeType(NodeManager* nodeManager,
-                                     TNode n,
-                                     bool check)
-  {
-    if (check)
-    {
-      TypeNode t1 = n[0].getType(check);
-      if (!t1.isBoolean())
-      {
-        throw TypeCheckingExceptionPrivate(
-            n, "expecting boolean term as first argument");
-      }
-      TypeNode t2 = n[1].getType(check);
-      if (!t2.isReal())
-      {
-        throw TypeCheckingExceptionPrivate(
-            n, "expecting polynomial as second argument");
-      }
-    }
-    return nodeManager->booleanType();
-  }
-}; /* class IndexedRootPredicateTypeRule */
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
+};
 
 }  // namespace arith
 }  // namespace theory