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