Method: Z3::Expr.Add

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

.Add(*args) ⇒ Object

Raises:



152
153
154
155
156
157
158
159
160
161
162
163
164
165
 
# File 'lib/z3/expr/expr.rb', line 152

def Add(*args)
  raise Z3::Exception if args.empty?
  args = coerce_to_same_sort(*args)
  case args[0]
  when ArithExpr
    args[0].sort.new(LowLevel.mk_add(args))
  when BitvecExpr
    args.inject do |a, b|
      a.sort.new(LowLevel.mk_bvadd(a, b))
    end
  else
    raise Z3::Exception, "Can't perform logic operations on #{args[0].sort} exprs, only Int/Real/Bitvec"
  end
end