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