class
Z3::CharExpr
- Z3::CharExpr
- Reference
- Object
Defined in:
z3/char_expr.crConstructors
Instance Method Summary
-
#!=(other)
Returns
trueif this object is not equal to other. - #<(other)
-
#<=(other)
Z3 only gives us
char.<=, and the order is total, so the other three are that one turned around and negated -
#==(other)
Returns
false(other can only be aValuehere). - #>(other)
- #>=(other)
-
#const?
A Char literal is an application of an indexed decl rather than a numeral, so the code point is easiest to get at by asking Z3 to simplify
char.to_int - #digit?
- #inspect(io)
-
#same_term?(other : AnyExpr)
Whether this is the same term as
other. - #simplify
- #sort
-
#to_bv
Z3's alphabet stops at 0x2FFFF, which is why 18 bits is always enough
- #to_c : Char
- #to_i
- #to_s(io)
- #to_unsafe : LibZ3::Ast
-
#value : Char
Every sort which can hand back a Crystal object spells it #value
Constructor Detail
Instance Method Detail
Returns true if this object is not equal to other.
By default this method is implemented as !(self == other)
so there's no need to override this unless there's a more efficient
way to do it.
Z3 only gives us char.<=, and the order is total, so the other three are that
one turned around and negated
Returns false (other can only be a Value here).
A Char literal is an application of an indexed decl rather than a numeral, so
the code point is easiest to get at by asking Z3 to simplify char.to_int
Whether this is the same term as other. Z3 hash-conses its expressions, so
this is structural equality - Z3.int("a") + 1 built twice is one term. It is
a named method rather than #== because #== builds a Z3 expression instead of
answering a Crystal Bool - see the Limitations section of the README.