diff options
| author | Liana Hadarean <lianahady@gmail.com> | 2012-11-13 04:49:34 +0000 |
|---|---|---|
| committer | Liana Hadarean <lianahady@gmail.com> | 2012-11-13 04:49:34 +0000 |
| commit | 2cf12a56cb9c5eb539d50a39b2764a292d6fd13f (patch) | |
| tree | 3578ca6339a97e4b85c83d1a9f2219aea569aca7 /src/theory/bv/kinds | |
| parent | 89081ba6a8a62a117cbfef99aa7c8e4bf0bf1b39 (diff) | |
added support for division by zero for bit-vector division operators
Diffstat (limited to 'src/theory/bv/kinds')
| -rw-r--r-- | src/theory/bv/kinds | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds index 9dc2e66bb..2faa12437 100644 --- a/src/theory/bv/kinds +++ b/src/theory/bv/kinds @@ -54,6 +54,10 @@ operator BITVECTOR_UREM 2 "bit-vector unsigned remainder from truncating divisio operator BITVECTOR_SDIV 2 "bit-vector 2's complement signed division" operator BITVECTOR_SREM 2 "bit-vector 2's complement signed remainder (sign follows dividend)" operator BITVECTOR_SMOD 2 "bit-vector 2's complement signed remainder (sign follows divisor)" +# total division kinds +operator BITVECTOR_UDIV_TOTAL 2 "bit-vector total unsigned division, truncating towards 0 (undefined if divisor is 0)" +operator BITVECTOR_UREM_TOTAL 2 "bit-vector total unsigned remainder from truncating division (undefined if divisor is 0)" + operator BITVECTOR_SHL 2 "bit-vector left shift" operator BITVECTOR_LSHR 2 "bit-vector logical shift right" operator BITVECTOR_ASHR 2 "bit-vector arithmetic shift right" @@ -135,6 +139,8 @@ typerule BITVECTOR_NEG ::CVC4::theory::bv::BitVectorFixedWidthTypeRule typerule BITVECTOR_UDIV ::CVC4::theory::bv::BitVectorFixedWidthTypeRule typerule BITVECTOR_UREM ::CVC4::theory::bv::BitVectorFixedWidthTypeRule +typerule BITVECTOR_UDIV_TOTAL ::CVC4::theory::bv::BitVectorFixedWidthTypeRule +typerule BITVECTOR_UREM_TOTAL ::CVC4::theory::bv::BitVectorFixedWidthTypeRule typerule BITVECTOR_SDIV ::CVC4::theory::bv::BitVectorFixedWidthTypeRule typerule BITVECTOR_SREM ::CVC4::theory::bv::BitVectorFixedWidthTypeRule typerule BITVECTOR_SMOD ::CVC4::theory::bv::BitVectorFixedWidthTypeRule |