class Z3::ParamDescrs

Which parameters a Solver, Optimize, or Tactic accepts, and what type each of them is.

Z3 validates parameters against these, but only once it starts solving, and it reports failures as a bare Z3_EXCEPTION. Params checks names and types against this upfront so a typo fails where it was made.

Constants

KINDS: Z3_param_kind. :other is for parameters Z3 has no specific type for, :invalid means there is no such parameter at all.

Attributes

_param_descrs [R]

Public Class Methods

new (_param_descrs)

Source

# File lib/z3/param_descrs.rb, line 23
def initialize(_param_descrs)
  @_param_descrs = _param_descrs
  inc_ref! :param_descrs, _param_descrs
end

Public Instance Methods

include? (name)

Source

# File lib/z3/param_descrs.rb, line 43
def include?(name)
  kind(name) != :invalid
end

inspect ()

Source

# File lib/z3/param_descrs.rb, line 51
def inspect
  "Z3::ParamDescrs<#{size} parameters>"
end

kind (name)

Source

# File lib/z3/param_descrs.rb, line 38
def kind(name)
  k = LowLevel.param_descrs_get_kind(self, LowLevel.mk_string_symbol(name.to_s))
  KINDS.fetch(k) { raise Z3::Exception, "Unknown parameter kind #{k}" }
end

names ()

Source

# File lib/z3/param_descrs.rb, line 32
def names
  (0...size).map do |i|
    LowLevel.get_symbol_string(LowLevel.param_descrs_get_name(self, i))
  end
end

size ()

Source

# File lib/z3/param_descrs.rb, line 28
def size
  LowLevel.param_descrs_size(self)
end

to_s ()

Source

# File lib/z3/param_descrs.rb, line 47
def to_s
  LowLevel.param_descrs_to_string(self)
end