Z3::CharExpr

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.

Z3's alphabet stops at 0x2FFFF, which is why 18 bits is always enough

The code point, as a Z3 Int - CharSort['a'].to_i is the term char.to_int('a'), not the Crystal Integer 97. #value is the one which hands back a Crystal object.

Every sort which can hand back a Crystal object spells it #value