Module Z3.Boolean

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