sig
  module Cnstrnt :
    sig
      type t = Unconstrained | Real of Dom.t | Bitvector of int
      val mk_real : Dom.t -> Var.Cnstrnt.t
      val mk_bitvector : int -> Var.Cnstrnt.t
      val pp : Var.Cnstrnt.t Pretty.printer
      exception Empty
      val sub : Var.Cnstrnt.t -> Var.Cnstrnt.t -> bool
      val inter : Var.Cnstrnt.t -> Var.Cnstrnt.t -> Var.Cnstrnt.t
    end
  type t
  val name_of : Var.t -> Name.t
  val cnstrnt_of : Var.t -> Var.Cnstrnt.t
  val dom_of : Var.t -> Dom.t
  val width_of : Var.t -> int
  val cmp : Var.t -> Var.t -> int
  val ( <<< ) : Var.t -> Var.t -> bool
  val mk_external : Name.t -> Var.Cnstrnt.t -> Var.t
  val mk_const : Th.t -> int -> Var.Cnstrnt.t -> Var.t
  val mk_rename : Name.t -> int -> Var.Cnstrnt.t -> Var.t
  type slack = Zero | Nonneg of Dom.t
  val nonneg : Dom.t -> Var.slack
  val mk_slack : int -> Var.slack -> Var.t
  val mk_fresh : Th.t -> int -> Var.Cnstrnt.t -> Var.t
  val is_var : Var.t -> bool
  val is_rename : Var.t -> bool
  val is_slack : Var.slack -> Var.t -> bool
  val is_zero_slack : Var.t -> bool
  val is_nonneg_slack : Var.t -> bool
  val is_const : Var.t -> bool
  val is_fresh : Th.t -> Var.t -> bool
  val is_some_fresh : Var.t -> bool
  val is_internal : Var.t -> bool
  val is_real : Var.t -> bool
  val is_int : Var.t -> bool
  val d_external : Var.t -> Name.t * Var.Cnstrnt.t
  val pretty : bool Pervasives.ref
  val pp : Var.t Pretty.printer
end