class Z3::BoolExpr
Public Class Methods
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
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
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
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
Source
# File lib/z3/expr/bool_expr.rb, line 23 def iff(other) BoolExpr.Iff(self, other) end
Source
# File lib/z3/expr/bool_expr.rb, line 27 def implies(other) BoolExpr.Implies(self, other) end
Source
# File lib/z3/expr/bool_expr.rb, line 31 def ite(a, b) BoolExpr.IfThenElse(self, a, b) end
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