Method: Z3::Expr.And

Defined in:
lib/z3/expr/expr.rb

.And(*args) ⇒ Object 



108
109
110
111
112
113
114
115
116
117
118
119
120
 
# File 'lib/z3/expr/expr.rb', line 108

def And(*args)
  args = coerce_to_same_sort(*args)
  case args[0]
  when BoolExpr
    BoolSort.new.new(Z3::LowLevel.mk_and(args))
  when BitvecExpr
    args.inject do |a, b|
      a.sort.new(Z3::LowLevel.mk_bvand(a, b))
    end
  else
    raise Z3::Exception, "Can't perform logic operations on #{args[0].sort} exprs, only Bool and Bitvec"
  end
end