class Z3::BoolExpr

# File lib/z3/expr/bool_expr.rb, line 81
def AtLeast(args, k)
  args = cardinality_args(args, k)
  BoolSort.new.new(LowLevel.mk_atleast(args, k))
end

# File lib/z3/expr/bool_expr.rb, line 75
def AtMost(args, k)
  args = cardinality_args(args, k)
  BoolSort.new.new(LowLevel.mk_atmost(args, k))
end

# File lib/z3/expr/bool_expr.rb, line 87
def Exactly(args, k)
  args = cardinality_args(args, k)
  BoolSort.new.new(LowLevel.mk_pbeq(args, [1] * args.size, k))
end

# File lib/z3/expr/bool_expr.rb, line 68
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 63
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 58
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 52
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 38
def to_b
  value = BOOL_VALUES[LowLevel.get_bool_value(self)]
  return value unless value.nil?
  value = BOOL_VALUES[LowLevel.get_bool_value(simplify)]
  raise Z3::Exception, "Can't convert expression #{to_s} into Boolean" if value.nil?
  value
end