Add missing type rules for parameterized operator kinds. (#2766)

6 files changed, 122 insertions, 5 deletions

diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds
index 3073d0078..95d1aa9c1 100644
--- a/src/theory/arith/kinds
+++ b/src/theory/arith/kinds
@@ -107,6 +107,7 @@ 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 DIVISION_TOTAL ::CVC4::theory::arith::ArithOperatorTypeRule
 typerule INTS_DIVISION_TOTAL ::CVC4::theory::arith::IntOperatorTypeRule
diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h
index 2e998010c..bde1730a2 100644
--- a/src/theory/arith/theory_arith_type_rules.h
+++ b/src/theory/arith/theory_arith_type_rules.h
@@ -169,6 +169,18 @@ 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 */
diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds
index 66ee02c63..612e530ee 100644
--- a/src/theory/bv/kinds
+++ b/src/theory/bv/kinds
@@ -165,8 +165,6 @@ typerule BITVECTOR_SMOD ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
 typerule BITVECTOR_SHL ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
 typerule BITVECTOR_LSHR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
 typerule BITVECTOR_ASHR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_ROTATE_LEFT ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_ROTATE_RIGHT ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
 
 typerule BITVECTOR_ULT ::CVC4::theory::bv::BitVectorPredicateTypeRule
 typerule BITVECTOR_ULE ::CVC4::theory::bv::BitVectorPredicateTypeRule
@@ -185,6 +183,7 @@ typerule BITVECTOR_ITE ::CVC4::theory::bv::BitVectorITETypeRule
 typerule BITVECTOR_REDOR ::CVC4::theory::bv::BitVectorUnaryPredicateTypeRule
 typerule BITVECTOR_REDAND ::CVC4::theory::bv::BitVectorUnaryPredicateTypeRule
 
+typerule BITVECTOR_CONCAT ::CVC4::theory::bv::BitVectorConcatTypeRule
 
 typerule BITVECTOR_EAGER_ATOM ::CVC4::theory::bv::BitVectorEagerAtomTypeRule
 typerule BITVECTOR_ACKERMANNIZE_UDIV ::CVC4::theory::bv::BitVectorAckermanizationUdivTypeRule
@@ -192,11 +191,18 @@ typerule BITVECTOR_ACKERMANNIZE_UREM ::CVC4::theory::bv::BitVectorAckermanizatio
 
 typerule BITVECTOR_EXTRACT_OP ::CVC4::theory::bv::BitVectorExtractOpTypeRule
 typerule BITVECTOR_EXTRACT ::CVC4::theory::bv::BitVectorExtractTypeRule
-typerule BITVECTOR_BITOF   ::CVC4::theory::bv::BitVectorBitOfTypeRule
-typerule BITVECTOR_CONCAT ::CVC4::theory::bv::BitVectorConcatTypeRule
+typerule BITVECTOR_BITOF_OP ::CVC4::theory::bv::BitVectorBitOfOpTypeRule
+typerule BITVECTOR_BITOF ::CVC4::theory::bv::BitVectorBitOfTypeRule
+typerule BITVECTOR_REPEAT_OP ::CVC4::theory::bv::BitVectorRepeatOpTypeRule
 typerule BITVECTOR_REPEAT ::CVC4::theory::bv::BitVectorRepeatTypeRule
-typerule BITVECTOR_ZERO_EXTEND ::CVC4::theory::bv::BitVectorExtendTypeRule
+typerule BITVECTOR_ROTATE_LEFT_OP ::CVC4::theory::bv::BitVectorRotateLeftOpTypeRule
+typerule BITVECTOR_ROTATE_LEFT ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_ROTATE_RIGHT_OP ::CVC4::theory::bv::BitVectorRotateRightOpTypeRule
+typerule BITVECTOR_ROTATE_RIGHT ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_SIGN_EXTEND_OP ::CVC4::theory::bv::BitVectorSignExtendOpTypeRule
 typerule BITVECTOR_SIGN_EXTEND ::CVC4::theory::bv::BitVectorExtendTypeRule
+typerule BITVECTOR_ZERO_EXTEND_OP ::CVC4::theory::bv::BitVectorZeroExtendOpTypeRule
+typerule BITVECTOR_ZERO_EXTEND ::CVC4::theory::bv::BitVectorExtendTypeRule
 
 typerule BITVECTOR_TO_NAT ::CVC4::theory::bv::BitVectorConversionTypeRule
 typerule INT_TO_BITVECTOR_OP ::CVC4::theory::bv::IntToBitVectorOpTypeRule
diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h
index 817099752..3460a980b 100644
--- a/src/theory/bv/theory_bv_type_rules.h
+++ b/src/theory/bv/theory_bv_type_rules.h
@@ -58,6 +58,18 @@ class BitVectorBitOfTypeRule {
   }
 }; /* class BitVectorBitOfTypeRule */
 
+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 BitVectorBVPredTypeRule {
  public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
@@ -251,6 +263,18 @@ class BitVectorConcatTypeRule {
   }
 }; /* class BitVectorConcatTypeRule */
 
+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:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
@@ -267,6 +291,30 @@ class BitVectorRepeatTypeRule {
   }
 }; /* class BitVectorRepeatTypeRule */
 
+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 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 BitVectorExtendTypeRule {
  public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
@@ -286,6 +334,30 @@ class BitVectorExtendTypeRule {
   }
 }; /* class BitVectorExtendTypeRule */
 
+class BitVectorRotateLeftOpTypeRule
+{
+ public:
+  inline static TypeNode computeType(NodeManager* nodeManager,
+                                     TNode n,
+                                     bool check)
+  {
+    Assert(n.getKind() == kind::BITVECTOR_ROTATE_LEFT);
+    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);
+    return nodeManager->builtinOperatorType();
+  }
+}; /* class BitVectorRotateRightOpTypeRule */
+
 class BitVectorConversionTypeRule {
  public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds
index b83e9616a..a0b00bcb0 100644
--- a/src/theory/datatypes/kinds
+++ b/src/theory/datatypes/kinds
@@ -91,6 +91,7 @@ constant TUPLE_UPDATE_OP \
         "util/tuple.h" \
         "operator for a tuple update; payload is an instance of the CVC4::TupleUpdate class"
 parameterized TUPLE_UPDATE TUPLE_UPDATE_OP 2 "tuple update; first parameter is a TUPLE_UPDATE_OP (which references an index), second is the tuple, third is the element to store in the tuple at the given index"
+typerule TUPLE_UPDATE_OP ::CVC4::theory::datatypes::TupleUpdateOpTypeRule
 typerule TUPLE_UPDATE ::CVC4::theory::datatypes::TupleUpdateTypeRule
 
 constant RECORD_UPDATE_OP \
@@ -99,6 +100,7 @@ constant RECORD_UPDATE_OP \
         "expr/record.h" \
         "operator for a record update; payload is an instance CVC4::RecordUpdate class"
 parameterized RECORD_UPDATE RECORD_UPDATE_OP 2 "record update; first parameter is a RECORD_UPDATE_OP (which references a field), second is a record term to update, third is the element to store in the record in the given field"
+typerule RECORD_UPDATE_OP ::CVC4::theory::datatypes::RecordUpdateOpTypeRule
 typerule RECORD_UPDATE ::CVC4::theory::datatypes::RecordUpdateTypeRule
 
 
diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h
index 140ebe158..8a5849010 100644
--- a/src/theory/datatypes/theory_datatypes_type_rules.h
+++ b/src/theory/datatypes/theory_datatypes_type_rules.h
@@ -273,6 +273,18 @@ struct TupleUpdateTypeRule {
   }
 }; /* struct TupleUpdateTypeRule */
 
+class TupleUpdateOpTypeRule
+{
+ public:
+  inline static TypeNode computeType(NodeManager* nodeManager,
+                                     TNode n,
+                                     bool check)
+  {
+    Assert(n.getKind() == kind::TUPLE_UPDATE_OP);
+    return nodeManager->builtinOperatorType();
+  }
+}; /* class TupleUpdateOpTypeRule */
+
 struct RecordUpdateTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
                                      bool check) {
@@ -298,6 +310,18 @@ struct RecordUpdateTypeRule {
   }
 }; /* struct RecordUpdateTypeRule */
 
+class RecordUpdateOpTypeRule
+{
+ public:
+  inline static TypeNode computeType(NodeManager* nodeManager,
+                                     TNode n,
+                                     bool check)
+  {
+    Assert(n.getKind() == kind::RECORD_UPDATE_OP);
+    return nodeManager->builtinOperatorType();
+  }
+}; /* class RecordUpdateOpTypeRule */
+
 class DtSizeTypeRule {
  public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n,