Class: Z3::ParamDescrs

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

Overview

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.

Constant Summary collapse

KINDS =

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

{
  0 => :uint,
  1 => :bool,
  2 => :double,
  3 => :symbol,
  4 => :string,
  5 => :other,
  6 => :invalid,
}

Instance Attribute Summary collapse

Instance Method Summary collapse

Methods included from ReferenceCounted

finalizer

Constructor Details

#initialize(_param_descrs) ⇒ ParamDescrs

Returns a new instance of ParamDescrs.



23
24
25
26
 
# File 'lib/z3/param_descrs.rb', line 23

def initialize(_param_descrs)
  @_param_descrs = _param_descrs
  inc_ref! :param_descrs, _param_descrs
end

Instance Attribute Details

#_param_descrs ⇒ Object (readonly)

Returns the value of attribute _param_descrs.



22
23
24
 
# File 'lib/z3/param_descrs.rb', line 22

def _param_descrs
  @_param_descrs
end

Instance Method Details

#include?(name) ⇒ Boolean

Returns:

  • (Boolean) 


43
44
45
 
# File 'lib/z3/param_descrs.rb', line 43

def include?(name)
  kind(name) != :invalid
end

#inspect ⇒ Object 



51
52
53
 
# File 'lib/z3/param_descrs.rb', line 51

def inspect
  "Z3::ParamDescrs<#{size} parameters>"
end

#kind(name) ⇒ Object 



38
39
40
41
 
# 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 ⇒ Object 



32
33
34
35
36
 
# 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 ⇒ Object 



28
29
30
 
# File 'lib/z3/param_descrs.rb', line 28

def size
  LowLevel.param_descrs_size(self)
end

#to_s ⇒ Object 



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

def to_s
  LowLevel.param_descrs_to_string(self)
end