package libsail

  1. Overview
  2. Docs
package libsail
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module AbsBitvector.Dom

type bvset =
  1. | Top
  2. | Bvs of (Big_int_Z.big_int, Bit.Three.ubit list) Gmap.gmap Specif.coq_sig
val bvset_rect : 'a1 -> ((Big_int_Z.big_int, Bit.Three.ubit list) Gmap.gmap Specif.coq_sig -> 'a1) -> bvset -> 'a1
val bvset_rec : 'a1 -> ((Big_int_Z.big_int, Bit.Three.ubit list) Gmap.gmap Specif.coq_sig -> 'a1) -> bvset -> 'a1
val to_bv_list : bvset -> Bit.Three.ubit list list option
type t = bvset
val top : bvset
val bot : t
val join_aux : (Big_int_Z.big_int, Bit.Three.ubit list) Gmap.gmap -> (Big_int_Z.big_int, Bit.Three.ubit list) Gmap.gmap -> (Big_int_Z.big_int, Bit.Three.ubit list) Gmap.gmap
val join : t -> t -> t
val meet_aux : (Big_int_Z.big_int, Bit.Three.ubit list) Gmap.gmap -> (Big_int_Z.big_int, Bit.Three.ubit list) Gmap.gmap -> (Big_int_Z.big_int, Bit.Three.ubit list) Gmap.gmap
val meet : t -> t -> t
val leb_aux : (Big_int_Z.big_int, Bit.Three.ubit list) Gmap.gmap -> (Big_int_Z.big_int, Bit.Three.ubit list) Gmap.gmap -> bool
val leb : t -> t -> bool
val unknown_bit : bvset
val zwbv : bvset
val abst : Definitions.bvn -> bvset
val lift_bitwise_gmap : (Bit.Three.ubit -> Bit.Three.ubit -> Bit.Three.ubit) -> (Big_int_Z.big_int, Bit.Three.ubit list) Gmap.gmap -> (Big_int_Z.big_int, Bit.Three.ubit list) Gmap.gmap -> (Big_int_Z.big_int, Bit.Three.ubit list) Gmap.gmap
val lift_bitwise : (Bit.Three.ubit -> Bit.Three.ubit -> Bit.Three.ubit) -> bvset -> bvset -> bvset
val coq_and : bvset -> bvset -> bvset
val coq_or : bvset -> bvset -> bvset
val xor : bvset -> bvset -> bvset
val not_gmap : (Big_int_Z.big_int, Bit.Three.ubit list) Gmap.gmap -> (Big_int_Z.big_int, Bit.Three.ubit list) Gmap.gmap
val not : bvset -> bvset
val add_gmap : (Big_int_Z.big_int, Bit.Three.ubit list) Gmap.gmap -> (Big_int_Z.big_int, Bit.Three.ubit list) Gmap.gmap -> (Big_int_Z.big_int, Bit.Three.ubit list) Gmap.gmap
val add : bvset -> bvset -> bvset
val append_insert : Bit.Three.ubit list -> Bit.Three.ubit list option -> Bit.Three.ubit list option
val append_gmap : (Big_int_Z.big_int, Bit.Three.ubit list) Gmap.gmap -> (Big_int_Z.big_int, Bit.Three.ubit list) Gmap.gmap -> (Big_int_Z.big_int, Bit.Three.ubit list) Gmap.gmap
val append : bvset -> bvset -> bvset
val one_bits : Big_int_Z.big_int -> Bit.Three.ubit list
val negate_gmap : (Big_int_Z.big_int, Bit.Three.ubit list) Gmap.gmap -> (Big_int_Z.big_int, Bit.Three.ubit list) Gmap.gmap
val negate : bvset -> bvset
val sub : bvset -> bvset -> bvset
val slice_bits : Bit.Three.ubit list -> Big_int_Z.big_int -> Big_int_Z.big_int -> Bit.Three.ubit list
val slice_gmap : (Big_int_Z.big_int, Bit.Three.ubit list) Gmap.gmap -> Big_int_Z.big_int -> Big_int_Z.big_int -> (Big_int_Z.big_int, Bit.Three.ubit list) Gmap.gmap
val slice : bvset -> Big_int_Z.big_int -> Big_int_Z.big_int -> bvset