class
Z3::BoolExpr
- Z3::BoolExpr
- Reference
- Object
Defined in:
z3/bool_expr.crConstructors
Instance Method Summary
-
#!=(other)
Returns
trueif this object is not equal to other. - #&(other)
-
#==(other)
Returns
false(other can only be aValuehere). - #^(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 -
#same_term?(other : AnyExpr)
Whether this is the same term as
other. - #simplify
- #sort
- #to_b : Bool
- #to_s(io)
- #to_unsafe : LibZ3::Ast
-
#value : Bool
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.
Returns false (other can only be a Value here).
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
Both branches have to be the same sort, and a Seq's sort includes its element
sort, so sort[] is what says so
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.