class Z3::BoolExpr

# File lib/z3/expr/bool_expr.rb, line 69
def IfThenElse(a, b, c)
  a, = coerce_to_same_bool_sort(a)
  b, c = coerce_to_same_sort(b, c)
  b.sort.new(LowLevel.mk_ite(a, b, c))
end

# File lib/z3/expr/bool_expr.rb, line 64
def Iff(a,b)
  a, b = coerce_to_same_bool_sort(a, b)
  BoolSort.new.new(LowLevel.mk_iff(a, b))
end

# File lib/z3/expr/bool_expr.rb, line 59
def Implies(a,b)
  a, b = coerce_to_same_bool_sort(a, b)
  BoolSort.new.new(LowLevel.mk_implies(a, b))
end

# File lib/z3/expr/bool_expr.rb, line 53
def coerce_to_same_bool_sort(*args)
  args = coerce_to_same_sort(*args)
  raise Z3::Exception, "Bool value expected" unless args[0].is_a?(BoolExpr)
  args
end

# File lib/z3/expr/bool_expr.rb, line 7
def !
  sort.new(LowLevel.mk_not(self))
end

# File lib/z3/expr/bool_expr.rb, line 11
def &(other)
  Expr.And(self, other)
end

# File lib/z3/expr/bool_expr.rb, line 19
def ^(other)
  Expr.Xor(self, other)
end

# File lib/z3/expr/bool_expr.rb, line 15
def |(other)
  Expr.Or(self, other)
end

# File lib/z3/expr/bool_expr.rb, line 3
def ~
  sort.new(LowLevel.mk_not(self))
end

# File lib/z3/expr/bool_expr.rb, line 23
def iff(other)
  BoolExpr.Iff(self, other)
end

# File lib/z3/expr/bool_expr.rb, line 27
def implies(other)
  BoolExpr.Implies(self, other)
end

# File lib/z3/expr/bool_expr.rb, line 31
def ite(a, b)
  BoolExpr.IfThenElse(self, a, b)
end

# File lib/z3/expr/bool_expr.rb, line 35
def to_b
  s = to_s
  if ast_kind == :app and (s == "true" or s == "false")
    s == "true"
  else
    obj = simplify
    s = obj.to_s
    if ast_kind == :app and (s == "true" or s == "false")
      s == "true"
    else
      raise Z3::Exception, "Can't convert expression #{to_s} to Boolean"
    end
  end
end