Class: Z3::ArithExpr

Inherits:
Expr show all
Defined in:
lib/z3/expr/arith_expr.rb

Direct Known Subclasses

IntExpr, RealExpr

Instance Attribute Summary

Attributes inherited from Expr

#sort

Attributes inherited from AST

#_ast

Class Method Summary collapse

Instance Method Summary collapse

Methods inherited from Expr

#!=, #==, Add, And, Distinct, Eq, Ge, Gt, Le, Lt, Mul, Or, Sub, Xor, coerce_to_same_sort, #initialize, #inspect, new_from_pointer, sort_for_const

Methods inherited from AST

#arguments, #ast_kind, #eql?, #func_decl, #hash, #initialize, #sexpr, #simplify, #to_s

Constructor Details

This class inherits a constructor from Z3::Expr

Class Method Details

.coerce_to_same_arith_sort(*args) ⇒ Object

Raises:



73
74
75
76
77
 
# 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

.Div(a, b) ⇒ Object 



79
80
81
82
 
# 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) ⇒ Object 



84
85
86
87
88
 
# 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

Instance Method Details

#*(other) ⇒ Object 



11
12
13
 
# File 'lib/z3/expr/arith_expr.rb', line 11

def *(other)
  Expr.Mul(self, other)
end

#**(other) ⇒ Object 



19
20
21
 
# File 'lib/z3/expr/arith_expr.rb', line 19

def **(other)
  ArithExpr.Power(self, other)
end

#+(other) ⇒ Object 



3
4
5
 
# File 'lib/z3/expr/arith_expr.rb', line 3

def +(other)
  Expr.Add(self, other)
end

#-(other) ⇒ Object 



7
8
9
 
# File 'lib/z3/expr/arith_expr.rb', line 7

def -(other)
  Expr.Sub(self, other)
end

#-@ ⇒ Object 



39
40
41
 
# File 'lib/z3/expr/arith_expr.rb', line 39

def -@
  sort.new(LowLevel.mk_unary_minus(self))
end

#/(other) ⇒ Object 



15
16
17
 
# File 'lib/z3/expr/arith_expr.rb', line 15

def /(other)
  ArithExpr.Div(self, other)
end

#<(other) ⇒ Object 



35
36
37
 
# File 'lib/z3/expr/arith_expr.rb', line 35

def <(other)
  Expr.Lt(self, other)
end

#<=(other) ⇒ Object 



31
32
33
 
# File 'lib/z3/expr/arith_expr.rb', line 31

def <=(other)
  Expr.Le(self, other)
end

#>(other) ⇒ Object 



23
24
25
 
# File 'lib/z3/expr/arith_expr.rb', line 23

def >(other)
  Expr.Gt(self, other)
end

#>=(other) ⇒ Object 



27
28
29
 
# File 'lib/z3/expr/arith_expr.rb', line 27

def >=(other)
  Expr.Ge(self, other)
end

#abs ⇒ Object 



59
60
61
 
# File 'lib/z3/expr/arith_expr.rb', line 59

def abs
  (self < 0).ite(-self, self)
end

#coerce(other) ⇒ Object

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



66
67
68
69
70
 
# 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? ⇒ Boolean

Returns:

  • (Boolean) 


55
56
57
 
# File 'lib/z3/expr/arith_expr.rb', line 55

def negative?
  self < 0
end

#nonzero? ⇒ Boolean

Returns:

  • (Boolean) 


47
48
49
 
# File 'lib/z3/expr/arith_expr.rb', line 47

def nonzero?
  self != 0
end

#positive? ⇒ Boolean

Returns:

  • (Boolean) 


51
52
53
 
# File 'lib/z3/expr/arith_expr.rb', line 51

def positive?
  self > 0
end

#zero? ⇒ Boolean

Returns:

  • (Boolean) 


43
44
45
 
# File 'lib/z3/expr/arith_expr.rb', line 43

def zero?
  self == 0
end