class Z3::StringSort

• Z3::StringSort
• Reference
• Object

Overview

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

Defined in:

z3/string_sort.cr

Class Method Summary

• .[](expr : StringExpr)
• .[](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

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

  The one character string for a code point, or "" if it isn't one.

• .from_int(int : IntExpr | Int)

  The decimal digits of a nonnegative Int.

• .from_signed_bv(bv : BitvecExpr)
• .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

• .to_s(io)
• .to_unsafe
• .var(name : String)

Class Method Detail