Class: Z3::Params

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

Overview

A set of parameters for a Solver, Optimize, or Tactic.

Z3 has no way to read parameters back, so this only ever accumulates - setting the same name twice overrides it, and there's no way to unset one.

If descrs is given, names and types are checked against it as they're set. Solver and Optimize always pass theirs, because Z3 itself only notices a bad parameter in the middle of solving, and then all it says is Z3_EXCEPTION.

Instance Attribute Summary collapse

Instance Method Summary collapse

Methods included from ReferenceCounted

finalizer

Constructor Details

#initialize(values = {}, descrs = nil) ⇒ Params

Returns a new instance of Params.



14
15
16
17
18
19
20
21
 
# File 'lib/z3/params.rb', line 14

def initialize(values = {}, descrs = nil)
  @_params = LowLevel.mk_params
  inc_ref! :params, @_params
  @descrs = descrs
  values.each do |name, value|
    self[name] = value
  end
end

Instance Attribute Details

#_params ⇒ Object (readonly)

Returns the value of attribute _params.



13
14
15
 
# File 'lib/z3/params.rb', line 13

def _params
  @_params
end

#descrs ⇒ Object (readonly)

Returns the value of attribute descrs.



13
14
15
 
# File 'lib/z3/params.rb', line 13

def descrs
  @descrs
end

Instance Method Details

#[]=(name, value) ⇒ Object 



23
24
25
26
27
28
29
30
31
32
33
34
35
36
 
# File 'lib/z3/params.rb', line 23

def []=(name, value)
  sym = LowLevel.mk_string_symbol(name.to_s)
  case kind_for(name, value)
  when :uint
    LowLevel.params_set_uint(self, sym, value)
  when :bool
    LowLevel.params_set_bool(self, sym, value)
  when :double
    LowLevel.params_set_double(self, sym, value.to_f)
  when :symbol
    LowLevel.params_set_symbol(self, sym, LowLevel.mk_string_symbol(value.to_s))
  end
  value
end

#to_s ⇒ Object 



38
39
40
 
# File 'lib/z3/params.rb', line 38

def to_s
  LowLevel.params_to_string(self)
end