class Z3::Solver

# File lib/z3/solver.rb, line 4
def initialize
  @_solver = LowLevel.mk_solver
  LowLevel.solver_inc_ref(self)
  reset_model!
end

# File lib/z3/solver.rb, line 25
def assert(ast)
  reset_model!
  LowLevel.solver_assert(self, ast)
end

# File lib/z3/solver.rb, line 67
def assertions
  _ast_vector = LowLevel.solver_get_assertions(self)
  LowLevel.unpack_ast_vector(_ast_vector)
end

# File lib/z3/solver.rb, line 30
def check
  reset_model!
  result = check_sat_results(LowLevel.solver_check(self))
  @has_model = true if result == :sat
  result
end

# File lib/z3/solver.rb, line 59
def model
  if @has_model
    @model ||= Z3::Model.new(LowLevel.solver_get_model(self))
  else
    raise Z3::Exception, "You need to check that it's satisfiable before asking for the model"
  end
end

# File lib/z3/solver.rb, line 15
def pop(n=1)
  reset_model!
  LowLevel.solver_pop(self, n)
end

# File lib/z3/solver.rb, line 77
def prove!(ast)
  @has_model = false
  push
  assert(~ast)
  case check
  when :sat
    puts "Counterexample exists"
    model.each do |n,v|
      puts "* #{n} = #{v}"
    end
  when :unknown
    puts "Unknown"
  when :unsat
    puts "Proven"
  else
    raise "Wrong SAT result #{r}"
  end
ensure
  pop
end

# File lib/z3/solver.rb, line 10
def push
  reset_model!
  LowLevel.solver_push(self)
end

# File lib/z3/solver.rb, line 20
def reset
  reset_model!
  LowLevel.solver_reset(self)
end

# File lib/z3/solver.rb, line 37
def satisfiable?
  case check
  when :sat
    true
  when :unsat
    false
  else
    raise Z3::Exception, "Satisfiability unknown"
  end
end

# File lib/z3/solver.rb, line 72
def statistics
  _stats = LowLevel::solver_get_statistics(self)
  LowLevel.unpack_statistics(_stats)
end

# File lib/z3/solver.rb, line 48
def unsatisfiable?
  case check
  when :unsat
    true
  when :sat
    false
  else
    raise Z3::Exception, "Satisfiability unknown"
  end
end