class Z3::EnumSort

An enumeration - a sort whose values are a fixed, finite list of names, and nothing else. Values are Symbols, and every enum has its own: ‘Color` and `Squirrel` are different values of different sorts, and Z3 refuses to compare them.

Attributes

name [R]

values [R]

Public Class Methods

from_pointer (_sort)

Source

# File lib/z3/sort/enum_sort.rb, line 68
def from_pointer(_sort)
  name = Sort.name_from_pointer(_sort)
  registry[name] ||= build(_sort, name, values_from_pointer(_sort, name))
end

Takes a raw sort pointer, as Sort.from_pointer needs it before there’s any Sort object. Rebuilds rather than redeclares, so it works for a sort Z3 handed us - out of a model, or parsed from a file - and not just for ones this process declared.

new (_sort, name, values)

Source

# File lib/z3/sort/enum_sort.rb, line 11
def initialize(_sort, name, values)
  @name = name
  @values = values
  super(_sort)
end

Both ways in already have the sort in hand - ::new declares it, ::from_pointer gets it back from Z3 - so this only ever wraps one

Calls superclass method

new (name, values)

Source

# File lib/z3/sort/enum_sort.rb, line 47
def new(name, values)
  name = normalize_name(name)
  values = normalize_values(values)
  already_declared = registry[name]
  if already_declared
    unless already_declared.values == values
      raise Z3::Exception, "Enum sort #{name} is already declared, with values #{already_declared.values.inspect}"
    end
    return already_declared
  end
  _sort = LowLevel.mk_enumeration_sort(
    LowLevel.mk_symbol(name),
    values.map { |value| LowLevel.mk_symbol(value) },
  )
  registry[name] = build(_sort, name, values)
end

Every other named sort can be rebuilt just by calling its maker again, since Z3 hash-conses them. Enumerations are the one exception - declaring the same name twice is an error rather than the sort you already had - so they’re memoized by name here, and asking for the same one twice gives it back.

Public Instance Methods

[] (value)

Source

# File lib/z3/sort/enum_sort.rb, line 28
def [](value)
  i = values.index(value.to_sym) if value.is_a?(Symbol) or value.is_a?(String)
  raise cant_convert(value) unless i
  new(LowLevel.mk_app(constructors[i], []))
end

constructors ()

Source

# File lib/z3/sort/enum_sort.rb, line 24
def constructors
  @constructors ||= values.size.times.map { |i| FuncDecl.new(LowLevel.get_datatype_sort_constructor(self, i)) }
end

The nullary constructor behind each value, in declaration order. Memoized because [] and EnumExpr#value both go through it, and sorts are memoized too, so there’s exactly one of these per enum.

expr_class ()

Source

# File lib/z3/sort/enum_sort.rb, line 17
def expr_class
  EnumExpr
end

from_const (value)

Source

# File lib/z3/sort/enum_sort.rb, line 34
def from_const(value)
  self[value]
end

inspect ()

Source

# File lib/z3/sort/enum_sort.rb, line 38
def inspect
  "EnumSort(#{name}, #{values.inspect})"
end