class Z3::CharSort

Constants

MAX_CODE_POINT: Z3’s alphabet is Unicode code points 0 to 0x2FFFF, so it stops short of Ruby’s 0x10FFFF. Z3 itself doesn’t check, it just misbehaves.

Public Class Methods

Source

# File lib/z3/sort/char_sort.rb, line 3
def initialize
  super LowLevel.mk_char_sort
end

Calls superclass method

Public Instance Methods

expr_class ()

Source

# File lib/z3/sort/char_sort.rb, line 11
def expr_class
  CharExpr
end

from_bv (bv)

Source

# File lib/z3/sort/char_sort.rb, line 32
def from_bv(bv)
  raise Z3::Exception, "Bitvec(18) expected, got #{AST.describe(bv)}" unless
    bv.is_a?(BitvecExpr) and bv.sort.size == 18
  new(LowLevel.mk_char_from_bv(bv))
end

The other direction of CharExpr#to_bv. Z3 wants the full 18 bits, which is as wide as its alphabet goes.

from_const (val)

Source

# File lib/z3/sort/char_sort.rb, line 17
def from_const(val)
  case val
  when Integer
    raise Z3::Exception, "Char code point must be between 0 and 0x#{MAX_CODE_POINT.to_s(16).upcase}" unless (0..MAX_CODE_POINT).cover?(val)
    new(LowLevel.mk_char(val))
  when String
    raise Z3::Exception, "Only single character strings can be converted to Char" unless val.size == 1
    from_const(val.ord)
  else
    raise cant_convert(val)
  end
end

Ruby has no character type, so a Char can be built either from a code point or from a one character String

to_s ()

Source

# File lib/z3/sort/char_sort.rb, line 38
def to_s
  "Char"
end