diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-12-20 13:44:51 -0800 |
---|---|---|
committer | Aina Niemetz <aina.niemetz@gmail.com> | 2018-12-20 15:42:40 -0800 |
commit | c4a4923bf72d81ea273edb4c94836f0714452ac3 (patch) | |
tree | d251a891943e1abaf246fb2db035b7af41a39d6f /src/theory/bv | |
parent | 6b46621c4076ace3b0703e29fbdadca04f7635cb (diff) |
Add missing type rules for parameterized operator kinds. (#2766)
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/kinds | 16 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_type_rules.h | 72 |
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, |