class

Z3::StringSort

Inherits Reference < Object

Z3 represents a String as a Seq(Char), so this is the very same sort as SeqSort.new(CharSort) - which is why that hands back StringSort

Class methods

[](expr : StringExpr)
Source
[](value : String)

A Z3 string is a sequence of code points, so a Crystal String converts character by character, not byte by byte - which means it has to be valid UTF-8

Source
cast(value) : StringExpr
Source
element_sort
Source
from_ast(ast : LibZ3::Ast) : StringExpr
Source
from_code(int : IntExpr | Int)

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

Source
from_int(int : IntExpr | Int)

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".

Source
from_signed_bv(bv : BitvecExpr)
Source
from_unsigned_bv(bv : BitvecExpr)

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

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