Method: Z3::Expr.Sub

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

.Sub(*args) ⇒ Object 



167
168
169
170
171
172
173
174
175
176
177
178
179
 
# File 'lib/z3/expr/expr.rb', line 167

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