module Bv: sig end
Operation on function symbols of the
bitvector theory
Th.bv.
- Constructors
mk_const b, mk_conc n m, mk_sub n i j
for representing Const(b), Conc(n, m), and Sub(n, i, j), respectively.
get f returns the function symbol in Th.bv represented by f,
or raises Not_found. - The test
is_const f (is_conc f, is_sub f) succeeds iff f
represents some Const(b) (Conc(n, m), Sub(n, i, j)).
d_conc f (d_const f, d_sub f) yields b ((n, m), (n, i, j))
if f represents Const(b) (Conc(n, m), Sub(n, i, j)); otherwise
Not_found is raised.pp p fmt (op, al) pretty-prints the appliation of op to the
argument list al depending on the value of Pretty.flag. See
also Pretty.apply. It assumes applications to Const(.) to be
nullary, applications to Conc(.,.) are binary, and Sub(.,.,.)
is unary. - The width associated with each bitvector function symbol
op is
returned by width op. For constant bitvector symbols, this width
is defined by the length of the associated bitvector of type Bitv.t,
the width of Conc(n, m) is n + m, and the width of Sub(n, i, j)
is j - i + 1, namely the width of the extracted sub-bitvector.
val get : Sym.t -> Sym.bv
val mk_const : Bitv.t -> Sym.t
val mk_conc : int -> int -> Sym.t
val mk_sub : int -> int -> int -> Sym.t
val is : Sym.t -> bool
val is_const : Sym.t -> bool
val is_conc : Sym.t -> bool
val is_sub : Sym.t -> bool
val d_const : Sym.t -> Bitv.t
val d_conc : Sym.t -> int * int
val d_sub : Sym.t -> int * int * int
val width : Sym.bv -> int
val pp : 'a Pretty.printer -> (Sym.bv * 'a list) Pretty.printer