Introduce template classes for simple type rules (#2835)

This commit introduces two template classes `SimpleTypeRule` and
`SimpleTypeRuleVar` to help define simple type rules without writing
lots of redundant code. The main advantages of this approach are:

- Less code
- More consistent error reporting
- Easier to extend type checking with other functionality (e.g. getting
the type of a symbol)

2 files changed, 28 insertions, 122 deletions

diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds
index 95d1aa9c1..409534050 100644
--- a/src/theory/arith/kinds
+++ b/src/theory/arith/kinds
@@ -94,40 +94,40 @@ typerule POW ::CVC4::theory::arith::ArithOperatorTypeRule
 
 typerule CONST_RATIONAL ::CVC4::theory::arith::ArithConstantTypeRule
 
-typerule LT ::CVC4::theory::arith::ArithPredicateTypeRule
-typerule LEQ ::CVC4::theory::arith::ArithPredicateTypeRule
-typerule GT ::CVC4::theory::arith::ArithPredicateTypeRule
-typerule GEQ ::CVC4::theory::arith::ArithPredicateTypeRule
+typerule LT "SimpleTypeRule<RBool, AReal, AReal>"
+typerule LEQ "SimpleTypeRule<RBool, AReal, AReal>"
+typerule GT "SimpleTypeRule<RBool, AReal, AReal>"
+typerule GEQ "SimpleTypeRule<RBool, AReal, AReal>"
 
 typerule TO_REAL ::CVC4::theory::arith::ArithOperatorTypeRule
 typerule TO_INTEGER ::CVC4::theory::arith::ArithOperatorTypeRule
-typerule IS_INTEGER ::CVC4::theory::arith::ArithUnaryPredicateTypeRule
+typerule IS_INTEGER "SimpleTypeRule<RBool, AReal>"
 
-typerule ABS ::CVC4::theory::arith::IntOperatorTypeRule
-typerule INTS_DIVISION ::CVC4::theory::arith::IntOperatorTypeRule
-typerule INTS_MODULUS ::CVC4::theory::arith::IntOperatorTypeRule
-typerule DIVISIBLE ::CVC4::theory::arith::IntUnaryPredicateTypeRule
-typerule DIVISIBLE_OP ::CVC4::theory::arith::DivisibleOpTypeRule
+typerule ABS "SimpleTypeRule<RInteger, AInteger>"
+typerule INTS_DIVISION "SimpleTypeRule<RInteger, AInteger, AInteger>"
+typerule INTS_MODULUS "SimpleTypeRule<RInteger, AInteger, AInteger>"
+typerule DIVISIBLE "SimpleTypeRule<RBool, AInteger>"
+typerule DIVISIBLE_OP "SimpleTypeRule<RBuiltinOperator>"
 
 typerule DIVISION_TOTAL ::CVC4::theory::arith::ArithOperatorTypeRule
-typerule INTS_DIVISION_TOTAL ::CVC4::theory::arith::IntOperatorTypeRule
-typerule INTS_MODULUS_TOTAL ::CVC4::theory::arith::IntOperatorTypeRule
-
-typerule EXPONENTIAL ::CVC4::theory::arith::RealOperatorTypeRule
-typerule SINE ::CVC4::theory::arith::RealOperatorTypeRule
-typerule COSINE ::CVC4::theory::arith::RealOperatorTypeRule
-typerule TANGENT ::CVC4::theory::arith::RealOperatorTypeRule
-typerule COSECANT ::CVC4::theory::arith::RealOperatorTypeRule
-typerule SECANT ::CVC4::theory::arith::RealOperatorTypeRule
-typerule COTANGENT ::CVC4::theory::arith::RealOperatorTypeRule
-typerule ARCSINE ::CVC4::theory::arith::RealOperatorTypeRule
-typerule ARCCOSINE ::CVC4::theory::arith::RealOperatorTypeRule
-typerule ARCTANGENT ::CVC4::theory::arith::RealOperatorTypeRule
-typerule ARCCOSECANT ::CVC4::theory::arith::RealOperatorTypeRule
-typerule ARCSECANT ::CVC4::theory::arith::RealOperatorTypeRule
-typerule ARCCOTANGENT ::CVC4::theory::arith::RealOperatorTypeRule
-
-typerule SQRT ::CVC4::theory::arith::RealOperatorTypeRule
+typerule INTS_DIVISION_TOTAL "SimpleTypeRule<RInteger, AInteger, AInteger>"
+typerule INTS_MODULUS_TOTAL "SimpleTypeRule<RInteger, AInteger, AInteger>"
+
+typerule EXPONENTIAL "SimpleTypeRule<RReal, AReal>"
+typerule SINE "SimpleTypeRule<RReal, AReal>"
+typerule COSINE "SimpleTypeRule<RReal, AReal>"
+typerule TANGENT "SimpleTypeRule<RReal, AReal>"
+typerule COSECANT "SimpleTypeRule<RReal, AReal>"
+typerule SECANT "SimpleTypeRule<RReal, AReal>"
+typerule COTANGENT "SimpleTypeRule<RReal, AReal>"
+typerule ARCSINE "SimpleTypeRule<RReal, AReal>"
+typerule ARCCOSINE "SimpleTypeRule<RReal, AReal>"
+typerule ARCTANGENT "SimpleTypeRule<RReal, AReal>"
+typerule ARCCOSECANT "SimpleTypeRule<RReal, AReal>"
+typerule ARCSECANT "SimpleTypeRule<RReal, AReal>"
+typerule ARCCOTANGENT "SimpleTypeRule<RReal, AReal>"
+
+typerule SQRT "SimpleTypeRule<RReal, AReal>"
 
 nullaryoperator PI "pi"
 
diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h
index c32b612e2..8b587c0fb 100644
--- a/src/theory/arith/theory_arith_type_rules.h
+++ b/src/theory/arith/theory_arith_type_rules.h
@@ -73,88 +73,6 @@ public:
   }
 };/* class ArithOperatorTypeRule */
 
-class IntOperatorTypeRule {
-public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    TNode::iterator child_it = n.begin();
-    TNode::iterator child_it_end = n.end();
-    if(check) {
-      for(; child_it != child_it_end; ++child_it) {
-        TypeNode childType = (*child_it).getType(check);
-        if (!childType.isInteger()) {
-          throw TypeCheckingExceptionPrivate(n, "expecting an integer subterm");
-        }
-      }
-    }
-    return nodeManager->integerType();
-  }
-};/* class IntOperatorTypeRule */
-
-class RealOperatorTypeRule {
-public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    TNode::iterator child_it = n.begin();
-    TNode::iterator child_it_end = n.end();
-    if(check) {
-      for(; child_it != child_it_end; ++child_it) {
-        TypeNode childType = (*child_it).getType(check);
-        if (!childType.isReal()) {
-          throw TypeCheckingExceptionPrivate(n, "expecting a real subterm");
-        }
-      }
-    }
-    return nodeManager->realType();
-  }
-};/* class RealOperatorTypeRule */
-
-class ArithPredicateTypeRule {
-public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    if( check ) {
-      TypeNode lhsType = n[0].getType(check);
-      if (!lhsType.isReal()) {
-        throw TypeCheckingExceptionPrivate(n, "expecting an arithmetic term on the left-hand-side");
-      }
-      TypeNode rhsType = n[1].getType(check);
-      if (!rhsType.isReal()) {
-        throw TypeCheckingExceptionPrivate(n, "expecting an arithmetic term on the right-hand-side");
-      }
-    }
-    return nodeManager->booleanType();
-  }
-};/* class ArithPredicateTypeRule */
-
-class ArithUnaryPredicateTypeRule {
-public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    if( check ) {
-      TypeNode t = n[0].getType(check);
-      if (!t.isReal()) {
-        throw TypeCheckingExceptionPrivate(n, "expecting an arithmetic term");
-      }
-    }
-    return nodeManager->booleanType();
-  }
-};/* class ArithUnaryPredicateTypeRule */
-
-class IntUnaryPredicateTypeRule {
-public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    if( check ) {
-      TypeNode t = n[0].getType(check);
-      if (!t.isInteger()) {
-        throw TypeCheckingExceptionPrivate(n, "expecting an integer term");
-      }
-    }
-    return nodeManager->booleanType();
-  }
-};/* class IntUnaryPredicateTypeRule */
-
 class RealNullaryOperatorTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
@@ -169,18 +87,6 @@ public:
   }
 };/* class RealNullaryOperatorTypeRule */
 
-class DivisibleOpTypeRule
-{
- public:
-  inline static TypeNode computeType(NodeManager* nodeManager,
-                                     TNode n,
-                                     bool check)
-  {
-    Assert(n.getKind() == kind::DIVISIBLE_OP);
-    return nodeManager->builtinOperatorType();
-  }
-}; /* class DivisibleOpTypeRule */
-
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */