Module AltErgoLib.Bitv

val src : Logs.src
type 'a alpha_term = {
  1. bv : 'a;
  2. sz : int;
}
val pp_alpha_term : 'a Fmt.t -> 'a alpha_term Fmt.t
type 'a signed = {
  1. value : 'a;
  2. negated : bool;
}

The 'a signed type represents possibly negated values of type 'a. It is used for bvnot at the leaves (Other and Ext below).

type 'a simple_term_aux =
  1. | Cte of Z.t
  2. | Other of 'a signed
  3. | Ext of 'a signed * int * int * int
type 'a simple_term = 'a simple_term_aux alpha_term
type 'a abstract = 'a simple_term list
val extract : int -> int -> int -> 'a abstract -> 'a abstract

extract size i j x extracts i..j from a composition of size size.

An element of size sz at the head of the composition contains the bits size - 1 .. size - sz inclusive.

val zero_extend : int -> 'a abstract -> 'a abstract

zero_extract sz bv adds sz zeros to the front (high bits) of bv.

val lognot : 'a abstract -> 'a abstract
val to_Z_opt : 'a abstract -> Z.t option

to_Z_opt r evaluates r to an integer if possible.

val int2bv_const : int -> Z.t -> 'a abstract

int2bv_const n z evaluates z as a constant n-bits bitvector.

If z is out of the 0 .. 2^n range, only the first n bits of z in binary representation are considered, i.e. int2bv_const n z is always equal to int2bv_const n (erem z (1 lsl n)).

module type ALIEN = sig ... end
module Shostak (X : ALIEN) : Sig.SHOSTAK with type r = X.r and type t = X.r abstract