mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

update ocaml doc per #2843

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-01-06 20:26:06 -08:00
parent f70696d8e7
commit a432fd71d3
1 changed files with 14 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
src/api/ml/z3.mli
View file

@ -1611,7 +1611,8 @@ sig
It is defined as the floor of [t1/t2] if \c t2 is
different from zero. If [t2] is zero, then the result
is undefined.
is not uniquely specified. It can be set to any value
that satisfies the constraints where unsigned division is used.
The arguments must have the same bit-vector sort. *)
val mk_udiv : context -> Expr.expr -> Expr.expr -> Expr.expr
@ -1623,14 +1624,18 @@ sig
- The \c ceiling of [t1/t2] if \c t2 is different from zero, and [t1*t2 < 0].
If [t2] is zero, then the result is undefined.
If [t2] is zero, then the result is is not uniquely specified.
It can be set to any value that satisfies the constraints
where signed division is used.
The arguments must have the same bit-vector sort. *)
val mk_sdiv : context -> Expr.expr -> Expr.expr -> Expr.expr
(** Unsigned remainder.
It is defined as [t1 - (t1 /u t2) * t2], where [/u] represents unsigned division.
If [t2] is zero, then the result is undefined.
If [t2] is zero, then the result is not uniquely specified.
It can be set to any value that satisfies the constraints
where unsigned remainder is used.
The arguments must have the same bit-vector sort. *)
val mk_urem : context -> Expr.expr -> Expr.expr -> Expr.expr
@ -1639,13 +1644,17 @@ sig
It is defined as [t1 - (t1 /s t2) * t2], where [/s] represents signed division.
The most significant bit (sign) of the result is equal to the most significant bit of \c t1.
If [t2] is zero, then the result is undefined.
If [t2] is zero, then the result is not uniquely specified.
It can be set to any value that satisfies the constraints
where signed remainder is used.
The arguments must have the same bit-vector sort. *)
val mk_srem : context -> Expr.expr -> Expr.expr -> Expr.expr
(** Two's complement signed remainder (sign follows divisor).
If [t2] is zero, then the result is undefined.
If [t2] is zero, then the result is not uniquely specified.
It can be set to any value that satisfies the constraints
where two's complement signed remainder is used.
The arguments must have the same bit-vector sort. *)
val mk_smod : context -> Expr.expr -> Expr.expr -> Expr.expr