Class: Z3::Solver

Inherits:
Object
  • Object
show all
Defined in:
lib/z3/solver.rb

Instance Attribute Summary collapse

Instance Method Summary collapse

Constructor Details

#initialize ⇒ Solver

Returns a new instance of Solver.



4
5
6
7
 
# File 'lib/z3/solver.rb', line 4

def initialize
  @_solver = LowLevel.mk_solver
  LowLevel.solver_inc_ref(self)
end

Instance Attribute Details

#_solver ⇒ Object (readonly)

Returns the value of attribute _solver.



3
4
5
 
# File 'lib/z3/solver.rb', line 3

def _solver
  @_solver
end

Instance Method Details

#assert(ast) ⇒ Object 



21
22
23
 
# File 'lib/z3/solver.rb', line 21

def assert(ast)
  LowLevel.solver_assert(self, ast)
end

#assertions ⇒ Object 



35
36
37
38
 
# File 'lib/z3/solver.rb', line 35

def assertions
  _ast_vector = LowLevel.solver_get_assertions(self)
  LowLevel.unpack_ast_vector(_ast_vector)
end

#check ⇒ Object 



25
26
27
 
# File 'lib/z3/solver.rb', line 25

def check
  check_sat_results(LowLevel.solver_check(self))
end

#model ⇒ Object 



29
30
31
32
33
 
# File 'lib/z3/solver.rb', line 29

def model
  Z3::Model.new(
    LowLevel.solver_get_model(self)
  )
end

#pop(n = 1) ⇒ Object 



13
14
15
 
# File 'lib/z3/solver.rb', line 13

def pop(n=1)
  LowLevel.solver_pop(self, n)
end

#prove!(ast) ⇒ Object 



45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
 
# File 'lib/z3/solver.rb', line 45

def prove!(ast)
  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 ⇒ Object 



9
10
11
 
# File 'lib/z3/solver.rb', line 9

def push
  LowLevel.solver_push(self)
end

#reset ⇒ Object 



17
18
19
 
# File 'lib/z3/solver.rb', line 17

def reset
  LowLevel.solver_reset(self)
end

#statistics ⇒ Object 



40
41
42
43
 
# File 'lib/z3/solver.rb', line 40

def statistics
  _stats = LowLevel::solver_get_statistics(self)
  LowLevel.unpack_statistics(_stats)
end