sig
  val bitv2nat : Bitv.t -> int
  val nat2bitv : int -> int -> Bitv.t
  val width : Term.t -> int option
  val d_const : Term.t -> Bitv.t
  val mk_const : Bitv.t -> Term.t
  val mk_eps : unit -> Term.t
  val mk_one : int -> Term.t
  val mk_zero : int -> Term.t
  val mk_conc : int -> int -> Term.t -> Term.t -> Term.t
  val mk_sub : int -> int -> int -> Term.t -> Term.t
  val is_interp : Term.t -> bool
  val is_const : Bitv.t -> Term.t -> bool
  val is_zero : Term.t -> bool
  val is_one : Term.t -> bool
  val is_diseq : Term.t -> Term.t -> bool
  val sigma : Sym.bv -> Term.t list -> Term.t
  val iter : (Term.t -> unit) -> Term.t -> unit
  val fold : (Term.t -> 'a -> 'a) -> Term.t -> 'a -> 'a
  val map : (Term.t -> Term.t) -> Term.t -> Term.t
  val apply : Term.Equal.t -> Term.t -> Term.t
  val solve : Term.t * Term.t -> (Term.t * Term.t) list
end