class Z3::ArithExpr

Public Class Methods

Div(a,b) click to toggle source
# File lib/z3/expr/arith_expr.rb, line 79
def Div(a,b)
  a, b = coerce_to_same_arith_sort(a, b)
  a.sort.new(LowLevel.mk_div(a, b))
end
Power(a, b) click to toggle source
# File lib/z3/expr/arith_expr.rb, line 84
def Power(a, b)
  # Wait, is this even legitimate that it's I**I and R**R?
  a, b = coerce_to_same_arith_sort(a, b)
  a.sort.new(LowLevel.mk_power(a, b))
end
coerce_to_same_arith_sort(*args) click to toggle source
# File lib/z3/expr/arith_expr.rb, line 73
def coerce_to_same_arith_sort(*args)
  args = coerce_to_same_sort(*args)
  raise Z3::Exception, "Int or Real value expected" unless args[0].is_a?(IntExpr) or args[0].is_a?(RealExpr)
  args
end

Public Instance Methods

*(other) click to toggle source
# File lib/z3/expr/arith_expr.rb, line 11
def *(other)
  Expr.Mul(self, other)
end
**(other) click to toggle source
# File lib/z3/expr/arith_expr.rb, line 19
def **(other)
  ArithExpr.Power(self, other)
end
+(other) click to toggle source
# File lib/z3/expr/arith_expr.rb, line 3
def +(other)
  Expr.Add(self, other)
end
-(other) click to toggle source
# File lib/z3/expr/arith_expr.rb, line 7
def -(other)
  Expr.Sub(self, other)
end
-@() click to toggle source
# File lib/z3/expr/arith_expr.rb, line 39
def -@
  sort.new(LowLevel.mk_unary_minus(self))
end
/(other) click to toggle source
# File lib/z3/expr/arith_expr.rb, line 15
def /(other)
  ArithExpr.Div(self, other)
end
<(other) click to toggle source
# File lib/z3/expr/arith_expr.rb, line 35
def <(other)
  Expr.Lt(self, other)
end
<=(other) click to toggle source
# File lib/z3/expr/arith_expr.rb, line 31
def <=(other)
  Expr.Le(self, other)
end
>(other) click to toggle source
# File lib/z3/expr/arith_expr.rb, line 23
def >(other)
  Expr.Gt(self, other)
end
>=(other) click to toggle source
# File lib/z3/expr/arith_expr.rb, line 27
def >=(other)
  Expr.Ge(self, other)
end
abs() click to toggle source
# File lib/z3/expr/arith_expr.rb, line 59
def abs
  (self < 0).ite(-self, self)
end
coerce(other) click to toggle source

Recast so 1 + x:Float is: (+ 1.0 x) not: (+ (to_real 1) x)

# File lib/z3/expr/arith_expr.rb, line 66
def coerce(other)
  other_sort = Expr.sort_for_const(other)
  max_sort = [sort, other_sort].max
  [max_sort.from_const(other), max_sort.from_value(self)]
end
negative?() click to toggle source
# File lib/z3/expr/arith_expr.rb, line 55
def negative?
  self < 0
end
nonzero?() click to toggle source
# File lib/z3/expr/arith_expr.rb, line 47
def nonzero?
  self != 0
end
positive?() click to toggle source
# File lib/z3/expr/arith_expr.rb, line 51
def positive?
  self > 0
end
zero?() click to toggle source
# File lib/z3/expr/arith_expr.rb, line 43
def zero?
  self == 0
end