class Z3::Optimize

# File lib/z3/optimize.rb, line 7
def initialize(params = {})
  @_optimize = LowLevel.mk_optimize
  inc_ref! :optimize, @_optimize
  reset_model!
  # Skipped for the common no-parameters case, as #set_params has to build
  # the parameter descriptions to check against
  set_params(params) unless params == {}
end

# File lib/z3/optimize.rb, line 40
def assert(ast)
  reset_model!
  LowLevel.optimize_assert(self, ast)
end

# File lib/z3/optimize.rb, line 47
def assert_and_track(ast, tracker)
  reset_model!
  LowLevel.optimize_assert_and_track(self, ast, tracker)
end

# File lib/z3/optimize.rb, line 52
def assert_soft(ast, weight = "1", id = nil)
  reset_model!
  LowLevel.optimize_assert_soft(self, ast, weight, id)
end

# File lib/z3/optimize.rb, line 94
def assertions
  _ast_vector = LowLevel.optimize_get_assertions(self)
  LowLevel.unpack_ast_vector(_ast_vector)
end

# File lib/z3/optimize.rb, line 57
def check(*args)
  reset_model!
  result = check_sat_results(LowLevel.optimize_check(self, args))
  @has_model = true if result == :sat
  result
end

# File lib/z3/optimize.rb, line 111
def help
  LowLevel.optimize_get_help(self)
end

# File lib/z3/optimize.rb, line 144
def maximize(ast)
  reset_model!
  LowLevel.optimize_maximize(self, ast)
end

# File lib/z3/optimize.rb, line 149
def minimize(ast)
  reset_model!
  LowLevel.optimize_minimize(self, ast)
end

# File lib/z3/optimize.rb, line 86
def model
  if @has_model
    @model ||= Z3::Model.new(LowLevel.optimize_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/optimize.rb, line 17
def param_descrs
  ParamDescrs.new(LowLevel.optimize_get_param_descrs(self))
end

# File lib/z3/optimize.rb, line 35
def pop
  reset_model!
  LowLevel.optimize_pop(self)
end

# File lib/z3/optimize.rb, line 119
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/optimize.rb, line 30
def push
  reset_model!
  LowLevel.optimize_push(self)
end

# File lib/z3/optimize.rb, line 140
def reason_unknown
  LowLevel.optimize_get_reason_unknown(self)
end

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

# File lib/z3/optimize.rb, line 24
def set_params(params)
  params = Params.new(params, param_descrs) unless params.is_a?(Params)
  LowLevel.optimize_set_params(self, params)
  self
end

# File lib/z3/optimize.rb, line 106
def statistics
  _stats = LowLevel::optimize_get_statistics(self)
  LowLevel.unpack_statistics(_stats)
end

# File lib/z3/optimize.rb, line 115
def to_s
  LowLevel.optimize_to_string(self)
end

# File lib/z3/optimize.rb, line 101
def unsat_core
  _ast_vector = LowLevel.optimize_get_unsat_core(self)
  LowLevel.unpack_ast_vector(_ast_vector)
end

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