class Z3::Solver
Attributes
_solver[R]
Public Class Methods
new()
click to toggle source
# File lib/z3/solver.rb, line 4 def initialize @_solver = LowLevel.mk_solver LowLevel.solver_inc_ref(self) reset_model! end
Public Instance Methods
assert(ast)
click to toggle source
# File lib/z3/solver.rb, line 25 def assert(ast) reset_model! LowLevel.solver_assert(self, ast) end
assertions()
click to toggle source
# File lib/z3/solver.rb, line 67 def assertions _ast_vector = LowLevel.solver_get_assertions(self) LowLevel.unpack_ast_vector(_ast_vector) end
check()
click to toggle source
# 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
model()
click to toggle source
# 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
pop(n=1)
click to toggle source
# File lib/z3/solver.rb, line 15 def pop(n=1) reset_model! LowLevel.solver_pop(self, n) end
prove!(ast)
click to toggle source
# 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
push()
click to toggle source
# File lib/z3/solver.rb, line 10 def push reset_model! LowLevel.solver_push(self) end
reset()
click to toggle source
# File lib/z3/solver.rb, line 20 def reset reset_model! LowLevel.solver_reset(self) end
satisfiable?()
click to toggle source
# 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
statistics()
click to toggle source
# File lib/z3/solver.rb, line 72 def statistics _stats = LowLevel::solver_get_statistics(self) LowLevel.unpack_statistics(_stats) end
unsatisfiable?()
click to toggle source
# 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
Private Instance Methods
check_sat_results(r)
click to toggle source
# File lib/z3/solver.rb, line 105 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/solver.rb, line 100 def reset_model! @has_model = false @model = nil end