class Z3::CharSort

Defined in:

z3/char_sort.cr

Constant Summary

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 Method Summary

Class Method Detail

def self.[](expr : CharExpr) #

[View source]
def self.[](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.


[View source]
def self.[](code_point : Int) #

[View source]
def self.cast(value) : CharExpr #

[View source]
def self.from_ast(ast : LibZ3::Ast) : CharExpr #

[View source]
def self.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.


[View source]
def self.to_s(io) #

[View source]
def self.to_unsafe #

[View source]
def self.var(name : String) #

[View source]