class Z3::Optimize

Attributes

_optimize[R]

Public Class Methods

new() click to toggle source
# File lib/z3/optimize.rb, line 5
def initialize
  @_optimize = LowLevel.mk_optimize
  LowLevel.optimize_inc_ref(self)
  reset_model!
end

Public Instance Methods

assert(ast) click to toggle source
# File lib/z3/optimize.rb, line 21
def assert(ast)
  reset_model!
  LowLevel.optimize_assert(self, ast)
end
assert_soft(ast, weight = "1", id = nil) click to toggle source
# File lib/z3/optimize.rb, line 26
def assert_soft(ast, weight = "1", id = nil)
  reset_model!
  LowLevel.optimize_assert_soft(self, ast, weight, id)
end
assertions() click to toggle source
# File lib/z3/optimize.rb, line 68
def assertions
  _ast_vector = LowLevel.optimize_get_assertions(self)
  LowLevel.unpack_ast_vector(_ast_vector)
end
check(*args) click to toggle source
# File lib/z3/optimize.rb, line 31
def check(*args)
  reset_model!
  result = check_sat_results(LowLevel.optimize_check(self, args))
  @has_model = true if result == :sat
  result
end
maximize(ast) click to toggle source
# File lib/z3/optimize.rb, line 103
def maximize(ast)
  LowLevel.optimize_maximize(self, ast)
end
minimize(ast) click to toggle source
# File lib/z3/optimize.rb, line 107
def minimize(ast)
  LowLevel.optimize_minimize(self, ast)
end
model() click to toggle source
# File lib/z3/optimize.rb, line 60
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
pop() click to toggle source
# File lib/z3/optimize.rb, line 16
def pop
  reset_model!
  LowLevel.optimize_pop(self)
end
prove!(ast) click to toggle source
# File lib/z3/optimize.rb, line 78
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
push() click to toggle source
# File lib/z3/optimize.rb, line 11
def push
  reset_model!
  LowLevel.optimize_push(self)
end
reason_unknown() click to toggle source
# File lib/z3/optimize.rb, line 99
def reason_unknown
  LowLevel.optimize_get_reason_unknown(self)
end
satisfiable?() click to toggle source
# File lib/z3/optimize.rb, line 38
def satisfiable?
  case check
  when :sat
    true
  when :unsat
    false
  else
    raise Z3::Exception, "Satisfiability unknown"
  end
end
statistics() click to toggle source
# File lib/z3/optimize.rb, line 73
def statistics
  _stats = LowLevel::optimize_get_statistics(self)
  LowLevel.unpack_statistics(_stats)
end
unsatisfiable?() click to toggle source
# File lib/z3/optimize.rb, line 49
def unsatisfiable?
  case check
  when :unsat
    true
  when :sat
    false
  else
    raise Z3::Exception, "Satisfiability unknown"
  end
end

Private Instance Methods

check_sat_results(r) click to toggle source
# File lib/z3/optimize.rb, line 118
def check_sat_results(r)
  {
    -1 => :unsat,
    0 => :unknown,
    1 => :sat,
  }[r] or raise Z3::Exception, "Wrong SAT result #{r}"
end
reset_model!() click to toggle source
# File lib/z3/optimize.rb, line 113
def reset_model!
  @has_model = false
  @model = nil
end