diff options
| author | Liana Hadarean <lianahady@gmail.com> | 2012-04-04 02:02:06 +0000 |
|---|---|---|
| committer | Liana Hadarean <lianahady@gmail.com> | 2012-04-04 02:02:06 +0000 |
| commit | 52d6dc20c61007a5c066590aa1fd0b95ed3c2527 (patch) | |
| tree | 040efec36cde7775b5c19eb43fcdd60cbeb61f9e /src/theory/bv/kinds | |
| parent | 4fa8c7d1a0654e7780fd485c51463c06b34379b5 (diff) | |
* added propagation as lemmas to TheoryBV:
* modified BVMinisat to work incrementally
* added more bv regressions
Diffstat (limited to 'src/theory/bv/kinds')
| -rw-r--r-- | src/theory/bv/kinds | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds index 36d25de2a..6ef2cb0a9 100644 --- a/src/theory/bv/kinds +++ b/src/theory/bv/kinds @@ -28,16 +28,16 @@ constant CONST_BITVECTOR \ "a fixed-width bit-vector constant" operator BITVECTOR_CONCAT 2: "bit-vector concatenation" -operator BITVECTOR_AND 2 "bitwise and" -operator BITVECTOR_OR 2 "bitwise or" -operator BITVECTOR_XOR 2 "bitwise xor" +operator BITVECTOR_AND 2: "bitwise and" +operator BITVECTOR_OR 2: "bitwise or" +operator BITVECTOR_XOR 2: "bitwise xor" operator BITVECTOR_NOT 1 "bitwise not" operator BITVECTOR_NAND 2 "bitwise nand" operator BITVECTOR_NOR 2 "bitwise nor" operator BITVECTOR_XNOR 2 "bitwise xnor" operator BITVECTOR_COMP 2 "equality comparison (returns one bit)" -operator BITVECTOR_MULT 2 "bit-vector multiplication" -operator BITVECTOR_PLUS 2 "bit-vector addition" +operator BITVECTOR_MULT 2: "bit-vector multiplication" +operator BITVECTOR_PLUS 2: "bit-vector addition" operator BITVECTOR_SUB 2 "bit-vector subtraction" operator BITVECTOR_NEG 1 "bit-vector unary negation" operator BITVECTOR_UDIV 2 "bit-vector unsigned division, truncating towards 0 (undefined if divisor is 0)" |