module Cint: sig
.. end
Integer arithmetics
Integer Arithmetic Model
module FunMap: FCMap.Make
(
Lang.Fun
)
val is_cint_map : Ctypes.c_int FunMap.t Pervasives.ref
val to_cint_map : Ctypes.c_int FunMap.t Pervasives.ref
val is_cint : FunMap.key -> Ctypes.c_int
Raises Not_found
if not.
val to_cint : FunMap.key -> Ctypes.c_int
Raises Not_found
if not.
val library : string
val make_fun_int : string -> Ctypes.c_int -> Lang.lfun
val make_pred_int : string -> Ctypes.c_int -> Lang.lfun
val p_is_int : Ctypes.c_int -> Lang.lfun
val f_to_int : Ctypes.c_int -> Lang.lfun
val f_truncate : Lang.lfun
val ac : 'a Qed.Logic.operator
val result : ('a, 'b) Qed.Logic.datatype
val library : string
val balance : Lang.balance
val op_lxor : 'a Qed.Logic.operator
val op_lor : 'a Qed.Logic.operator
val op_land : 'a Qed.Logic.operator
val f_lnot : Lang.lfun
val f_lor : Lang.lfun
val f_land : Lang.lfun
val f_lxor : Lang.lfun
val f_lsl : Lang.lfun
val f_lsr : Lang.lfun
val f_bit : Lang.lfun
val of_real : Ctypes.c_int -> Lang.F.term -> Lang.F.term
val irange : Ctypes.c_int -> Lang.F.term -> Lang.F.pred
val iconvert : Ctypes.c_int -> Lang.F.term -> Lang.F.term
val iconvert_unsigned : Ctypes.c_int -> Lang.F.term -> Lang.F.term
type
model =
val model : model Context.value
val configure : model -> unit
val ibinop : ('a -> 'b -> Lang.F.term) -> Ctypes.c_int -> 'a -> 'b -> Lang.F.term
val iunop : ('a -> Lang.F.term) -> Ctypes.c_int -> 'a -> Lang.F.term
val iopp : Ctypes.c_int -> Lang.F.term -> Lang.F.term
val iadd : Ctypes.c_int -> Lang.F.term -> Lang.F.term -> Lang.F.term
val isub : Ctypes.c_int -> Lang.F.term -> Lang.F.term -> Lang.F.term
val imul : Ctypes.c_int -> Lang.F.term -> Lang.F.term -> Lang.F.term
val idiv : Ctypes.c_int -> Lang.F.term -> Lang.F.term -> Lang.F.term
val imod : Ctypes.c_int -> Lang.F.term -> Lang.F.term -> Lang.F.term
val smp1 : (Lang.F.Z.t -> Lang.F.Z.t) -> Lang.F.term list -> Lang.F.term
val smp2 : Lang.F.Fun.t ->
(Lang.F.Z.t -> Lang.F.Z.t -> Lang.F.Z.t) -> Lang.F.term list -> Lang.F.term
val match_integer : Lang.F.term -> Lang.F.Z.t
val is_to_cint : FunMap.key -> bool
val is_positive_or_null : Lang.F.term -> bool
val is_negative : Lang.F.term -> bool
val match_power2 : Lang.F.term -> Lang.F.term
val match_positive_integer : Lang.F.term -> Lang.F.Z.t
val match_integer_arg1 : Lang.F.term list -> Lang.F.Z.t * Lang.F.term
val match_positive_integer_arg2 : Lang.F.term list -> Lang.F.term * Lang.F.Z.t
: Lang.F.term list -> Lang.F.Z.t * Lang.F.term list
val is_leq : Lang.F.term -> Lang.F.term -> Qed.Logic.maybe
val bitk_positive : Lang.F.term -> Lang.F.term -> Lang.F.term
val smp_bitk_positive : Lang.F.term list -> Lang.F.term
val match_fun : Lang.F.Fun.t -> Lang.F.term -> Lang.F.term list
val match_ufun : Lang.F.Fun.t -> Lang.F.term -> Lang.F.term
: Lang.F.term list -> Lang.F.term * Lang.F.term * Lang.F.term list
val introduction_bit_test_positive : Lang.F.term list -> Lang.F.term -> Lang.F.term
val smp_land : Lang.F.term list -> Lang.F.term
val smp_shift : (Lang.F.Z.t -> Lang.F.Z.t -> Lang.F.Z.t) -> Lang.F.term list -> Lang.F.term
val smp_eq_with_land : Lang.F.term -> Lang.F.term -> Lang.F.term
val smp_eq_with_lor : Lang.F.term -> Lang.F.term -> Lang.F.term
val smp_eq_with_lxor : Lang.F.term -> Lang.F.term -> Lang.F.term
val smp_eq_with_lnot : Lang.F.term -> Lang.F.term -> Lang.F.term
val two_power_k_minus1 : Integer.t -> Integer.t
val smp_eq_with_lsl : Lang.F.term -> Lang.F.term -> Lang.F.term
val smp_eq_with_lsr : Lang.F.term -> Lang.F.term -> Lang.F.term
type
l_builtin = {
|
f : Lang.lfun ; |
|
eq : (Lang.F.term -> Lang.F.term -> Lang.F.term) option ; |
|
smp : Lang.F.term list -> Lang.F.term ; |
}
val install_builtins : unit -> unit
val l_not : Lang.F.term -> Lang.F.term
val l_xor : Lang.F.term -> Lang.F.term -> Lang.F.term
val l_or : Lang.F.term -> Lang.F.term -> Lang.F.term
val l_and : Lang.F.term -> Lang.F.term -> Lang.F.term
val l_lsl : Lang.F.term -> Lang.F.term -> Lang.F.term
val l_lsr : Lang.F.term -> Lang.F.term -> Lang.F.term
val bnot : Ctypes.c_int -> Lang.F.term -> Lang.F.term
val bxor : Ctypes.c_int -> Lang.F.term -> Lang.F.term -> Lang.F.term
val bor : 'a -> Lang.F.term -> Lang.F.term -> Lang.F.term
val band : 'a -> Lang.F.term -> Lang.F.term -> Lang.F.term
val blsl : Ctypes.c_int -> Lang.F.term -> Lang.F.term -> Lang.F.term
val blsr : 'a -> Lang.F.term -> Lang.F.term -> Lang.F.term