Module Katbv_lib.Bitstring

Type

type t = (Base.int, Base.unit) Base.Hashtbl.t

the type of a bit string. AF: the table H represents a bitvector v where v_i=1 iff (i, ()) is in H. Note that bit strings are interpreted left to right as highest bit to lowest bit. So the string 110 is the binary representation of 6 and (100)_0 = 0 whereas (100)_2 = 1

include Ppx_sexp_conv_lib.Sexpable.S with type Bitstring.t := t
val t_of_sexp : Sexplib0__.Sexp.t -> t
val sexp_of_t : t -> Sexplib0__.Sexp.t
include Base.Comparator.S with type Bitstring.t := t
type comparator_witness
val comparator : (t, comparator_witness) Base.Comparator.comparator

Constructors

val zero : t

the zero bit string

val of_bool_list : Base.bool Base.list -> t

of_bool_list lst bv is the bit string v where v_i=1 iff lst_i=true

val of_int_list : Base.int Base.list -> t

of_int_list lst bv the bit string v where v_i=1 iff i is in lst

val of_binary : Base.string -> t

of_binary s is the bit string v where v_i=1 iff s_i="1"

val of_ternary : Base.string -> t * t

of_ternary s is the pair (z, n) where z_i=1 iff s_i="0" and n_i=1 iff s_i="1"

Basic Operations

val max : t -> Base.int Base.option

max v is Some i where i is the maximum of {j:v_j=1}

val min : t -> Base.int Base.option

min v is Some i where i is the minimum of {j:v_j=1}

val (**) : t -> t -> t

v**v' is bitwise multiplication of v and v'

val (++) : t -> t -> t

v++v' is bitwise OR of v and v'

val (--) : t -> t -> t

v -- v' is v'' where v''_i=0 if v'_i=1 and otherwise v''_i=v_i

val xor : t -> t -> t

xor v v' is the bitwise xor of v and v'

val is_zero : t -> Base.bool

is_zero v is true iff v=0

val equal : t -> t -> Base.bool

equal v v' is true iff v=v'

val nth : t -> Base.int -> Base.bool

nth v i is true iff v_i=1

KAT+B! functions

val lower_bound : Base.string -> t -> Katbb_lib.Ast.bexp

lower_bound s a is KAT+B! Boolean expression that is satisfied by s:=v iff v>=a where s is the variable name

val upper_bound : Base.string -> t -> Katbb_lib.Ast.bexp

upper_bound s b is KAT+B! Boolean expression that is satisfied by s:=v iff v<=b where s is the variable name

val build_term_list : t -> t -> (Base.bool -> Base.int -> 'a) -> 'a Base.list

build_term_list z n h is a list with elements h false i for all i such that z_i=1 and elements h true i for all i such that n_i=1

Rendering

val to_string : t -> Base.string