diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-09-28 20:18:22 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-09-28 20:18:22 -0700 |
| commit | d06cf394473cbe09c2e1acc333526c41a6dd9687 (patch) | |
| tree | cec81c5557fdcf0e144da5a275471e92063e4e45 /src/theory/bv/kinds | |
| parent | e25f99329c9905c67a565481dcb0d6a4499a7557 (diff) | |
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)
Diffstat (limited to 'src/theory/bv/kinds')
| -rw-r--r-- | src/theory/bv/kinds | 14 |
1 files changed, 7 insertions, 7 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 |