class Z3::BoolExpr
Public Class Methods
IfThenElse(a, b, c)
click to toggle source
# File lib/z3/expr/bool_expr.rb, line 69 def IfThenElse(a, b, c) a, = coerce_to_same_bool_sort(a) b, c = coerce_to_same_sort(b, c) b.sort.new(LowLevel.mk_ite(a, b, c)) end
Iff(a,b)
click to toggle source
# File lib/z3/expr/bool_expr.rb, line 64 def Iff(a,b) a, b = coerce_to_same_bool_sort(a, b) BoolSort.new.new(LowLevel.mk_iff(a, b)) end
Implies(a,b)
click to toggle source
# File lib/z3/expr/bool_expr.rb, line 59 def Implies(a,b) a, b = coerce_to_same_bool_sort(a, b) BoolSort.new.new(LowLevel.mk_implies(a, b)) end
coerce_to_same_bool_sort(*args)
click to toggle source
# File lib/z3/expr/bool_expr.rb, line 53 def coerce_to_same_bool_sort(*args) args = coerce_to_same_sort(*args) raise Z3::Exception, "Bool value expected" unless args[0].is_a?(BoolExpr) args end
Public Instance Methods
!()
click to toggle source
# File lib/z3/expr/bool_expr.rb, line 7 def ! sort.new(LowLevel.mk_not(self)) end
&(other)
click to toggle source
# File lib/z3/expr/bool_expr.rb, line 11 def &(other) Expr.And(self, other) end
^(other)
click to toggle source
# File lib/z3/expr/bool_expr.rb, line 19 def ^(other) Expr.Xor(self, other) end
iff(other)
click to toggle source
# File lib/z3/expr/bool_expr.rb, line 23 def iff(other) BoolExpr.Iff(self, other) end
implies(other)
click to toggle source
# File lib/z3/expr/bool_expr.rb, line 27 def implies(other) BoolExpr.Implies(self, other) end
ite(a, b)
click to toggle source
# File lib/z3/expr/bool_expr.rb, line 31 def ite(a, b) BoolExpr.IfThenElse(self, a, b) end
to_b()
click to toggle source
# File lib/z3/expr/bool_expr.rb, line 35 def to_b s = to_s if ast_kind == :app and (s == "true" or s == "false") s == "true" else obj = simplify s = obj.to_s if ast_kind == :app and (s == "true" or s == "false") s == "true" else raise Z3::Exception, "Can't convert expression #{to_s} to Boolean" end end end
|(other)
click to toggle source
# File lib/z3/expr/bool_expr.rb, line 15 def |(other) Expr.Or(self, other) end
~()
click to toggle source
# File lib/z3/expr/bool_expr.rb, line 3 def ~ sort.new(LowLevel.mk_not(self)) end