mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 02:15:19 +00:00
adding doc #1132
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
5357864dbe
commit
465ed7d068
|
@ -396,6 +396,33 @@ typedef enum
|
|||
The meaning is given by the equivalence
|
||||
(xor3 l1 l2 l3) <=> (xor (xor l1 l2) l3)
|
||||
|
||||
- Z3_OP_BSMUL_NO_OVFL: a predicate to check that bit-wise signed multiplication does not overflow.
|
||||
Signed multiplication overflows if the operands have the same sign and the result of multiplication
|
||||
does not fit within the available bits. \sa Z3_mk_bvmul_no_overflow.
|
||||
|
||||
- Z3_OP_BUMUL_NO_OVFL: check that bit-wise unsigned multiplication does not overflow.
|
||||
Unsigned multiplication overflows if the result does not fit within the available bits.
|
||||
\sa Z3_mk_bvmul_no_overflow.
|
||||
|
||||
- Z3_OP_BSMUL_NO_UDFL: check that bit-wise signed multiplication does not underflow.
|
||||
Signed multiplication underflows if the operands have opposite signs and the result of multiplication
|
||||
does not fit within the avaialble bits. Z3_mk_bvmul_no_underflow.
|
||||
|
||||
- Z3_OP_BSDIV_I: Binary signed division.
|
||||
It has the same semantics as Z3_OP_BSDIV, but created in a context where the second operand can be assumed to be non-zero.
|
||||
|
||||
- Z3_OP_BUDIV_I: Binary unsigned division.
|
||||
It has the same semantics as Z3_OP_BUDIV, but created in a context where the second operand can be assumed to be non-zero.
|
||||
|
||||
- Z3_OP_BSREM_I: Binary signed remainder.
|
||||
It has the same semantics as Z3_OP_BSREM, but created in a context where the second operand can be assumed to be non-zero.
|
||||
|
||||
- Z3_OP_BUREM_I: Binary unsigned remainder.
|
||||
It has the same semantics as Z3_OP_BUREM, but created in a context where the second operand can be assumed to be non-zero.
|
||||
|
||||
- Z3_OP_BSMOD_I: Binary signed modulus.
|
||||
It has the same semantics as Z3_OP_BSMOND, but created in a context where the second operand can be assumed to be non-zero.
|
||||
|
||||
- Z3_OP_PR_UNDEF: Undef/Null proof object.
|
||||
|
||||
- Z3_OP_PR_TRUE: Proof for the expression 'true'.
|
||||
|
|
Loading…
Reference in a new issue