class Z3::SeqSort

Attributes

Public Class Methods

Source

# File lib/z3/sort/seq_sort.rb, line 5
def self.new(element_sort)
  return StringSort.new if element_sort == CharSort.new
  super
end

Z3 has no String sort of its own, String is just Seq(Char) - so Seq(Char) has to come back as a StringSort, or we’d have two Ruby classes for one Z3 sort

Calls superclass method

new (element_sort)

Source

# File lib/z3/sort/seq_sort.rb, line 11
def initialize(element_sort)
  @element_sort = element_sort
  super LowLevel.mk_seq_sort(element_sort)
end

Calls superclass method

Public Instance Methods

expr_class ()

Source

# File lib/z3/sort/seq_sort.rb, line 16
def expr_class
  SeqExpr
end

from_const (val)

Source

# File lib/z3/sort/seq_sort.rb, line 22
def from_const(val)
  raise cant_convert(val) unless val.is_a?(Array)
  units = val.map { |v| new(LowLevel.mk_seq_unit(element_sort.cast(v))) }
  case units.size
  when 0
    new(LowLevel.mk_seq_empty(self))
  when 1
    units[0]
  else
    new(LowLevel.mk_seq_concat(units))
  end
end

Z3 has no sequence literals, a sequence value is a concatenation of one element sequences - and it rejects a concatenation of fewer than two of them

inspect ()

Source

# File lib/z3/sort/seq_sort.rb, line 39
def inspect
  "SeqSort(#{element_sort})"
end

to_s ()

Source

# File lib/z3/sort/seq_sort.rb, line 35
def to_s
  "Seq(#{element_sort})"
end