class Z3::Goal

# File lib/z3/goal.rb, line 90
def from_pointer(_goal)
  goal = allocate
  goal.send(:initialize, _goal)
  goal
end

# File lib/z3/goal.rb, line 7
def initialize(_goal)
  @_goal = _goal
  inc_ref! :goal, _goal
end

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

# File lib/z3/goal.rb, line 12
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 70
def convert_model(model)
  raise Z3::Exception, "Model required" unless model.is_a?(Model)
  Model.new(LowLevel.goal_convert_model(self, model))
end

# File lib/z3/goal.rb, line 42
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 47
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 21
def depth
  LowLevel.goal_depth(self)
end

# File lib/z3/goal.rb, line 60
def each
  return to_enum(:each) unless block_given?
  size.times { |i| yield formula(i) }
  self
end

# File lib/z3/goal.rb, line 52
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 37
def inconsistent?
  # Does it convert bool or do we need to ?
  LowLevel.goal_inconsistent(self)
end

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

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

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

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

# File lib/z3/goal.rb, line 79
def to_dimacs(include_names=true)
  LowLevel.goal_to_dimacs_string(self, include_names)
end

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