class Z3::StringSort

Z3 internally represents String as Seq(Char), so StringSort == SeqSort.new(CharSort.new)

Public Class Methods

Source

# File lib/z3/sort/string_sort.rb, line 4
def initialize
  super LowLevel.mk_string_sort
end

Calls superclass method Z3::Sort::new

new (_ast)

Source

# File lib/z3/sort/sort.rb, line 3
def initialize(_ast)
  super(_ast)
  raise Z3::Exception, "Sorts must have AST kind sort" unless ast_kind == :sort
end

Calls superclass method Z3::Sort::new

Public Instance Methods

element_sort ()

Source

# File lib/z3/sort/string_sort.rb, line 8
def element_sort
  CharSort.new
end

expr_class ()

Source

# File lib/z3/sort/string_sort.rb, line 12
def expr_class
  StringExpr
end

from_code (int)

Source

# File lib/z3/sort/string_sort.rb, line 40
def from_code(int)
  new(LowLevel.mk_string_from_code(IntSort.new.cast(int)))
end

The one character string for a code point, or “” if it isn’t one. StringExpr#to_code is this backwards.

from_const (val)

Source

# File lib/z3/sort/string_sort.rb, line 18
def from_const(val)
  raise cant_convert(val) unless val.is_a?(String)
  raise Z3::Exception, "String is not valid #{val.encoding}" unless val.valid_encoding?
  val.each_codepoint do |code_point|
    next if code_point <= CharSort::MAX_CODE_POINT
    raise Z3::Exception, "Character 0x#{code_point.to_s(16).upcase} is outside Z3's alphabet (0 to 0x#{CharSort::MAX_CODE_POINT.to_s(16).upcase})"
  end
  new(LowLevel.mk_string(val))
end

A Z3 string is a sequence of code points, so a Ruby String converts character by character, not byte by byte - which means it has to be valid in its own encoding

from_int (int)

Source

# File lib/z3/sort/string_sort.rb, line 34
def from_int(int)
  new(LowLevel.mk_int_to_str(IntSort.new.cast(int)))
end

The decimal digits of a nonnegative Int. SMT-LIB says a negative number has no string form at all, and Z3 answers “” for one rather than “-1”.

from_signed_bv (bv)

Source

# File lib/z3/sort/string_sort.rb, line 50
def from_signed_bv(bv)
  new(LowLevel.mk_sbv_to_str(expect_bitvec(bv)))
end

from_unsigned_bv (bv)

Source

# File lib/z3/sort/string_sort.rb, line 46
def from_unsigned_bv(bv)
  new(LowLevel.mk_ubv_to_str(expect_bitvec(bv)))
end

Decimal digits again, but of a Bitvec read either way - the same eight bits give “253” unsigned and “-3” signed