sig
  val mk_sort : Z3.context -> Z3.Sort.sort
  val mk_const : Z3.context -> Z3.Symbol.symbol -> Z3.Expr.expr
  val mk_const_s : Z3.context -> string -> Z3.Expr.expr
  val mk_true : Z3.context -> Z3.Expr.expr
  val mk_false : Z3.context -> Z3.Expr.expr
  val mk_val : Z3.context -> bool -> Z3.Expr.expr
  val mk_not : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_ite :
    Z3.context ->
    Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_iff : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_implies : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_xor : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_and : Z3.context -> Z3.Expr.expr list -> Z3.Expr.expr
  val mk_or : Z3.context -> Z3.Expr.expr list -> Z3.Expr.expr
  val mk_eq : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_distinct : Z3.context -> Z3.Expr.expr list -> Z3.Expr.expr
  val get_bool_value : Z3.Expr.expr -> Z3enums.lbool
  val is_bool : Z3.Expr.expr -> bool
  val is_true : Z3.Expr.expr -> bool
  val is_false : Z3.Expr.expr -> bool
  val is_eq : Z3.Expr.expr -> bool
  val is_distinct : Z3.Expr.expr -> bool
  val is_ite : Z3.Expr.expr -> bool
  val is_and : Z3.Expr.expr -> bool
  val is_or : Z3.Expr.expr -> bool
  val is_iff : Z3.Expr.expr -> bool
  val is_xor : Z3.Expr.expr -> bool
  val is_not : Z3.Expr.expr -> bool
  val is_implies : Z3.Expr.expr -> bool
end