class

Z3::BoolExpr

Inherits Reference < Object

Constructors

new(expr : LibZ3::Ast)

Instance methods

!=(other)

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.

&(other)

==(other)

Returns false (other can only be a Value here).

^(other)

|(other)

~

const?

iff(other)

implies(other)

inspect(io)

ite(a : BoolExpr | Bool, b : BoolExpr | Bool) : BoolExpr

ite(a : BitvecExpr, b : BitvecExpr | Int) : BitvecExpr

Both branches have to be the same sort, and a Bitvec's sort includes its size, so the sizes have to match too - sort[] is what says so

ite(a : Int, b : BitvecExpr) : BitvecExpr

ite(a : IntExpr | Int, b : IntExpr | Int) : IntExpr

ite(a : Int | Float64 | BigRational, b : RealExpr) : RealExpr

ite(a : RealExpr, b : RealExpr | Int | Float64 | BigRational) : RealExpr

ite(a : Char, b : CharExpr) : CharExpr

ite(a : CharExpr, b : CharExpr | Char) : CharExpr

ite(a : String, b : StringExpr) : StringExpr

ite(a : StringExpr, b : StringExpr | String) : StringExpr

ite(a : Array, b : SeqExpr) : SeqExpr

ite(a : SeqExpr, b : SeqExpr | Array) : SeqExpr

Both branches have to be the same sort, and a Seq's sort includes its element sort, so sort[] is what says so

ite(a : Float64 | Int, b : FloatExpr) : FloatExpr

ite(a : FloatExpr, b : FloatExpr | Float64 | Int) : FloatExpr

Both branches have to be the same sort, and a Float's sort is its two bit counts, so sort[] is what says so

ite(a : RoundingModeExpr, b : RoundingModeExpr) : RoundingModeExpr

same_term?(other : AnyExpr)

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.

simplify

sort

to_b

to_s(io)

to_unsafe

value

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