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 



67
68
69
70
 
# File 'lib/z3/solver.rb', line 67

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 



59
60
61
62
63
64
65
 
# 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) ⇒ 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 



77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
 
# 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 ⇒ 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
40
41
42
43
44
45
46
 
# 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 ⇒ Object 



72
73
74
75
 
# File 'lib/z3/solver.rb', line 72

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

#unsatisfiable? ⇒ Boolean

Returns:

  • (Boolean) 


48
49
50
51
52
53
54
55
56
57
 
# 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