From c4a4923bf72d81ea273edb4c94836f0714452ac3 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Thu, 20 Dec 2018 13:44:51 -0800 Subject: [PATCH] Add missing type rules for parameterized operator kinds. (#2766) --- src/theory/arith/kinds | 1 + src/theory/arith/theory_arith_type_rules.h | 12 ++++ src/theory/bv/kinds | 16 +++-- src/theory/bv/theory_bv_type_rules.h | 72 +++++++++++++++++++ src/theory/datatypes/kinds | 2 + .../datatypes/theory_datatypes_type_rules.h | 24 +++++++ 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, -- 2.30.2