class Z3::Goal

# File lib/z3/goal.rb, line 4
def initialize(_goal)
  @_goal = _goal
end

# File lib/z3/goal.rb, line 59
def new(models=false, unsat_cores=false, proofs=false)
  super LowLevel.mk_goal(!!models, !!unsat_cores, !!proofs)
end

# File lib/z3/goal.rb, line 8
def assert(ast)
  raise Z3::Exception, "AST required" unless ast.is_a?(AST)
  LowLevel.goal_assert(self, ast)
end

# File lib/z3/goal.rb, line 38
def decided_sat?
  # Does it convert bool or do we need to ?
  LowLevel.goal_is_decided_sat(self)
end

# File lib/z3/goal.rb, line 43
def decided_unsat?
  # Does it convert bool or do we need to ?
  LowLevel.goal_is_decided_unsat(self)
end

# File lib/z3/goal.rb, line 17
def depth
  LowLevel.goal_depth(self)
end

# File lib/z3/goal.rb, line 48
def formula(num)
  raise Z3::Exception, "Out of range" unless num.between?(0, size-1)
  # We should probably deal with out of bounds here
  Expr.new_from_pointer(LowLevel.goal_formula(self, num))
end

# File lib/z3/goal.rb, line 33
def inconsistent?
  # Does it convert bool or do we need to ?
  LowLevel.goal_inconsistent(self)
end

# File lib/z3/goal.rb, line 25
def num_exprs
  LowLevel.goal_num_exprs(self)
end

# File lib/z3/goal.rb, line 29
def precision
  LowLevel.goal_precision(self)
end

# File lib/z3/goal.rb, line 13
def reset
  LowLevel.goal_reset(self)
end

# File lib/z3/goal.rb, line 21
def size
  LowLevel.goal_size(self)
end

# File lib/z3/goal.rb, line 54
def to_s
  LowLevel.goal_to_string(self)
end