class

Z3::CharSort

Inherits Reference < Object

Constants

MAX_CODE_POINT = 196607

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

Class methods

[](expr : CharExpr)
Source
[](c : Char)

Crystal has a Char type, so unlike Ruby's z3 gem there is no need to read a one character String as a character. A code point works too, since that is what a Z3 Char is.

Source
[](code_point : Int)
Source
cast(value) : CharExpr
Source
from_ast(ast : LibZ3::Ast) : CharExpr
Source
from_bv(bv : BitvecExpr)

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

Source
to_s(io)
Source
to_unsafe
Source
var(name : String)
Source