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.



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

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 



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

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

#assert_soft(ast) ⇒ Object 



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

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

#assertions ⇒ Object 



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

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

#check ⇒ Object 



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

def check
  reset_model!
  result = check_sat_results(LowLevel.optimize_check(self))
  @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 



59
60
61
62
63
64
65
 
# File 'lib/z3/optimize.rb', line 59

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 



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

def pop
  reset_model!
  LowLevel.optimize_pop(self)
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/optimize.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/optimize.rb', line 10

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) 


37
38
39
40
41
42
43
44
45
46
 
# File 'lib/z3/optimize.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/optimize.rb', line 72

def statistics
  _stats = LowLevel::optimize_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/optimize.rb', line 48

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