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
8
 
# File 'lib/z3/solver.rb', line 4

def initialize
  @_solver = LowLevel.mk_solver
  LowLevel.solver_inc_ref(self)
  reset_model!
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 



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

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

#assertions ⇒ Object 



53
54
55
56
 
# File 'lib/z3/solver.rb', line 53

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

#check ⇒ Object 



30
31
32
33
34
35
 
# 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 ⇒ Object 



45
46
47
48
49
50
51
 
# File 'lib/z3/solver.rb', line 45

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) ⇒ Object 



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

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

#prove!(ast) ⇒ Object 



63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
 
# File 'lib/z3/solver.rb', line 63

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 ⇒ Object 



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

def push
  reset_model!
  LowLevel.solver_push(self)
end

#reset ⇒ Object 



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

def reset
  reset_model!
  LowLevel.solver_reset(self)
end

#satisfiable? ⇒ Boolean

Returns:

  • (Boolean) 


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

def satisfiable?
  check == :sat
end

#statistics ⇒ Object 



58
59
60
61
 
# File 'lib/z3/solver.rb', line 58

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

#unsatisfiable? ⇒ Boolean

Returns:

  • (Boolean) 


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

def unsatisfiable?
  check == :unsat
end