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, 7 insertions, 91 deletions

diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds
index fe451603b..f9caf119a 100644
--- a/src/theory/bv/kinds
+++ b/src/theory/bv/kinds
@@ -222,19 +222,19 @@ typerule BITVECTOR_EAGER_ATOM ::CVC4::theory::bv::BitVectorEagerAtomTypeRule
 
 ### type rules for parameterized operator kinds -------------------------------
 
-typerule BITVECTOR_BITOF_OP ::CVC4::theory::bv::BitVectorBitOfOpTypeRule
+typerule BITVECTOR_BITOF_OP "SimpleTypeRule<RBuiltinOperator>"
 typerule BITVECTOR_BITOF ::CVC4::theory::bv::BitVectorBitOfTypeRule
-typerule BITVECTOR_EXTRACT_OP ::CVC4::theory::bv::BitVectorExtractOpTypeRule
+typerule BITVECTOR_EXTRACT_OP "SimpleTypeRule<RBuiltinOperator>"
 typerule BITVECTOR_EXTRACT ::CVC4::theory::bv::BitVectorExtractTypeRule
-typerule BITVECTOR_REPEAT_OP ::CVC4::theory::bv::BitVectorRepeatOpTypeRule
+typerule BITVECTOR_REPEAT_OP "SimpleTypeRule<RBuiltinOperator>"
 typerule BITVECTOR_REPEAT ::CVC4::theory::bv::BitVectorRepeatTypeRule
-typerule BITVECTOR_ROTATE_LEFT_OP ::CVC4::theory::bv::BitVectorRotateLeftOpTypeRule
+typerule BITVECTOR_ROTATE_LEFT_OP "SimpleTypeRule<RBuiltinOperator>"
 typerule BITVECTOR_ROTATE_LEFT ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_ROTATE_RIGHT_OP ::CVC4::theory::bv::BitVectorRotateRightOpTypeRule
+typerule BITVECTOR_ROTATE_RIGHT_OP "SimpleTypeRule<RBuiltinOperator>"
 typerule BITVECTOR_ROTATE_RIGHT ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_SIGN_EXTEND_OP ::CVC4::theory::bv::BitVectorSignExtendOpTypeRule
+typerule BITVECTOR_SIGN_EXTEND_OP "SimpleTypeRule<RBuiltinOperator>"
 typerule BITVECTOR_SIGN_EXTEND ::CVC4::theory::bv::BitVectorExtendTypeRule
-typerule BITVECTOR_ZERO_EXTEND_OP ::CVC4::theory::bv::BitVectorZeroExtendOpTypeRule
+typerule BITVECTOR_ZERO_EXTEND_OP "SimpleTypeRule<RBuiltinOperator>"
 typerule BITVECTOR_ZERO_EXTEND ::CVC4::theory::bv::BitVectorExtendTypeRule
 typerule INT_TO_BITVECTOR_OP ::CVC4::theory::bv::IntToBitVectorOpTypeRule
 typerule INT_TO_BITVECTOR ::CVC4::theory::bv::BitVectorConversionTypeRule
diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h
index 64d04a37e..e56f752af 100644
--- a/src/theory/bv/theory_bv_type_rules.h
+++ b/src/theory/bv/theory_bv_type_rules.h
@@ -224,18 +224,6 @@ class BitVectorITETypeRule
 /* parameterized operator kinds                                               */
 /* -------------------------------------------------------------------------- */
 
-class BitVectorBitOfOpTypeRule
-{
- public:
-  inline static TypeNode computeType(NodeManager* nodeManager,
-                                     TNode n,
-                                     bool check)
-  {
-    Assert(n.getKind() == kind::BITVECTOR_BITOF_OP);
-    return nodeManager->builtinOperatorType();
-  }
-}; /* class BitVectorBitOfOpTypeRule */
-
 class BitVectorBitOfTypeRule
 {
  public:
@@ -262,18 +250,6 @@ class BitVectorBitOfTypeRule
   }
 }; /* class BitVectorBitOfTypeRule */
 
-class BitVectorExtractOpTypeRule
-{
- public:
-  inline static TypeNode computeType(NodeManager* nodeManager,
-                                     TNode n,
-                                     bool check)
-  {
-    Assert(n.getKind() == kind::BITVECTOR_EXTRACT_OP);
-    return nodeManager->builtinOperatorType();
-  }
-}; /* class BitVectorExtractOpTypeRule */
-
 class BitVectorExtractTypeRule
 {
  public:
@@ -309,18 +285,6 @@ class BitVectorExtractTypeRule
   }
 }; /* class BitVectorExtractTypeRule */
 
-class BitVectorRepeatOpTypeRule
-{
- public:
-  inline static TypeNode computeType(NodeManager* nodeManager,
-                                     TNode n,
-                                     bool check)
-  {
-    Assert(n.getKind() == kind::BITVECTOR_REPEAT_OP);
-    return nodeManager->builtinOperatorType();
-  }
-}; /* class BitVectorRepeatOpTypeRule */
-
 class BitVectorRepeatTypeRule
 {
  public:
@@ -341,54 +305,6 @@ class BitVectorRepeatTypeRule
   }
 }; /* class BitVectorRepeatTypeRule */
 
-class BitVectorRotateLeftOpTypeRule
-{
- public:
-  inline static TypeNode computeType(NodeManager* nodeManager,
-                                     TNode n,
-                                     bool check)
-  {
-    Assert(n.getKind() == kind::BITVECTOR_ROTATE_LEFT_OP);
-    return nodeManager->builtinOperatorType();
-  }
-}; /* class BitVectorRotateLeftOpTypeRule */
-
-class BitVectorRotateRightOpTypeRule
-{
- public:
-  inline static TypeNode computeType(NodeManager* nodeManager,
-                                     TNode n,
-                                     bool check)
-  {
-    Assert(n.getKind() == kind::BITVECTOR_ROTATE_RIGHT_OP);
-    return nodeManager->builtinOperatorType();
-  }
-}; /* class BitVectorRotateRightOpTypeRule */
-
-class BitVectorSignExtendOpTypeRule
-{
- public:
-  inline static TypeNode computeType(NodeManager* nodeManager,
-                                     TNode n,
-                                     bool check)
-  {
-    Assert(n.getKind() == kind::BITVECTOR_SIGN_EXTEND_OP);
-    return nodeManager->builtinOperatorType();
-  }
-}; /* class BitVectorSignExtendOpTypeRule */
-
-class BitVectorZeroExtendOpTypeRule
-{
- public:
-  inline static TypeNode computeType(NodeManager* nodeManager,
-                                     TNode n,
-                                     bool check)
-  {
-    Assert(n.getKind() == kind::BITVECTOR_ZERO_EXTEND_OP);
-    return nodeManager->builtinOperatorType();
-  }
-}; /* class BitVectorZeroExtendOpTypeRule */
-
 class BitVectorExtendTypeRule
 {
  public: