Class: Z3::Optimize

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

Instance Attribute Summary collapse

Instance Method Summary collapse

Methods included from ReferenceCounted

finalizer

Constructor Details

#initialize(params = {}) ⇒ Optimize

Returns a new instance of Optimize.



7
8
9
10
11
12
13
14
 
# File 'lib/z3/optimize.rb', line 7

def initialize(params = {})
  @_optimize = LowLevel.mk_optimize
  inc_ref! :optimize, @_optimize
  reset_model!
  # Skipped for the common no-parameters case, as #set_params has to build
  # the parameter descriptions to check against
  set_params(params) unless params == {}
end

Instance Attribute Details

#_optimize ⇒ Object (readonly)

Returns the value of attribute _optimize.



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

def _optimize
  @_optimize
end

Instance Method Details

#assert(ast) ⇒ Object 



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

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

#assert_and_track(ast, tracker) ⇒ Object

tracker is a Bool const standing in for ast, and it's what shows up in #unsat_core if the solver blames this assertion



47
48
49
50
 
# File 'lib/z3/optimize.rb', line 47

def assert_and_track(ast, tracker)
  reset_model!
  LowLevel.optimize_assert_and_track(self, ast, tracker)
end

#assert_soft(ast, weight = "1", id = nil) ⇒ Object 



52
53
54
55
 
# File 'lib/z3/optimize.rb', line 52

def assert_soft(ast, weight = "1", id = nil)
  reset_model!
  LowLevel.optimize_assert_soft(self, ast, weight, id)
end

#assertions ⇒ Object 



94
95
96
97
 
# File 'lib/z3/optimize.rb', line 94

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

#check(*args) ⇒ Object 



57
58
59
60
61
62
 
# File 'lib/z3/optimize.rb', line 57

def check(*args)
  reset_model!
  result = check_sat_results(LowLevel.optimize_check(self, args))
  @has_model = true if result == :sat
  result
end

#help ⇒ Object 



111
112
113
 
# File 'lib/z3/optimize.rb', line 111

def help
  LowLevel.optimize_get_help(self)
end

#maximize(ast) ⇒ Object 



144
145
146
147
 
# File 'lib/z3/optimize.rb', line 144

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

#minimize(ast) ⇒ Object 



149
150
151
152
 
# File 'lib/z3/optimize.rb', line 149

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

#model ⇒ Object 



86
87
88
89
90
91
92
 
# File 'lib/z3/optimize.rb', line 86

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

#param_descrs ⇒ Object

Optimize takes far fewer parameters than Solver does



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

def param_descrs
  ParamDescrs.new(LowLevel.optimize_get_param_descrs(self))
end

#pop ⇒ Object 



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

def pop
  reset_model!
  LowLevel.optimize_pop(self)
end

#prove!(ast) ⇒ Object 



119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
 
# File 'lib/z3/optimize.rb', line 119

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 



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

def push
  reset_model!
  LowLevel.optimize_push(self)
end

#reason_unknown ⇒ Object 



140
141
142
 
# File 'lib/z3/optimize.rb', line 140

def reason_unknown
  LowLevel.optimize_get_reason_unknown(self)
end

#satisfiable? ⇒ Boolean

Returns:

  • (Boolean) 


64
65
66
67
68
69
70
71
72
73
 
# File 'lib/z3/optimize.rb', line 64

def satisfiable?
  case check
  when :sat
    true
  when :unsat
    false
  else
    raise Z3::Exception, "Satisfiability unknown"
  end
end

#set_params(params) ⇒ Object

Parameters accumulate - setting one twice overrides it, but parameters set by earlier calls stay. Pass a Params if you want to skip the name and type checks, a Hash if you don't.



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

def set_params(params)
  params = Params.new(params, param_descrs) unless params.is_a?(Params)
  LowLevel.optimize_set_params(self, params)
  self
end

#statistics ⇒ Object 



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

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

#to_s ⇒ Object 



115
116
117
 
# File 'lib/z3/optimize.rb', line 115

def to_s
  LowLevel.optimize_to_string(self)
end

#unsat_core ⇒ Object

Only the trackers passed to #assert_and_track can ever show up here, plainly asserted formulas are never blamed



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

def unsat_core
  _ast_vector = LowLevel.optimize_get_unsat_core(self)
  LowLevel.unpack_ast_vector(_ast_vector)
end

#unsatisfiable? ⇒ Boolean

Returns:

  • (Boolean) 


75
76
77
78
79
80
81
82
83
84
 
# File 'lib/z3/optimize.rb', line 75

def unsatisfiable?
  case check
  when :unsat
    true
  when :sat
    false
  else
    raise Z3::Exception, "Satisfiability unknown"
  end
end