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

2 files changed, 83 insertions, 5 deletions

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,