Class: Z3::Optimize

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

Instance Attribute Summary collapse

Instance Method Summary collapse

Constructor Details

#initialize ⇒ Optimize

Returns a new instance of Optimize.



5
6
7
8
9
 
# File 'lib/z3/optimize.rb', line 5

def initialize
  @_optimize = LowLevel.mk_optimize
  LowLevel.optimize_inc_ref(self)
  reset_model!
end

Instance Attribute Details

#_optimize ⇒ Object (readonly)

Returns the value of attribute _optimize.



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

def _optimize
  @_optimize
end

Instance Method Details

#assert(ast) ⇒ Object 



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

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

#assert_soft(ast) ⇒ Object 



26
27
28
29
 
# File 'lib/z3/optimize.rb', line 26

def assert_soft(ast)
  reset_model!
  LowLevel.optimize_assert_soft(self, ast)
end

#assertions ⇒ Object 



68
69
70
71
 
# 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) ⇒ Object 



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



103
104
105
 
# File 'lib/z3/optimize.rb', line 103

def maximize(ast)
  LowLevel.optimize_maximize(self, ast)
end

#minimize(ast) ⇒ Object 



107
108
109
 
# File 'lib/z3/optimize.rb', line 107

def minimize(ast)
  LowLevel.optimize_minimize(self, ast)
end

#model ⇒ Object 



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



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

def pop
  reset_model!
  LowLevel.optimize_pop(self)
end

#prove!(ast) ⇒ Object 



78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
 
# 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 ⇒ Object 



11
12
13
14
 
# File 'lib/z3/optimize.rb', line 11

def push
  reset_model!
  LowLevel.optimize_push(self)
end

#reason_unknown ⇒ Object 



99
100
101
 
# File 'lib/z3/optimize.rb', line 99

def reason_unknown
  LowLevel.optimize_get_reason_unknown(self)
end

#satisfiable? ⇒ Boolean

Returns:

  • (Boolean) 


38
39
40
41
42
43
44
45
46
47
 
# 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 ⇒ Object 



73
74
75
76
 
# File 'lib/z3/optimize.rb', line 73

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

#unsatisfiable? ⇒ Boolean

Returns:

  • (Boolean) 


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