class Z3::Params

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.

Attributes

_params [R]

descrs [R]

Public Class Methods

new (values = {}, descrs = nil)

Source

# 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

Public Instance Methods

[]= (name, value)

Source

# 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 ()

Source

# File lib/z3/params.rb, line 38
def to_s
  LowLevel.params_to_string(self)
end