Class: Z3::IntExpr

Inherits:
ArithExpr show all
Defined in:
lib/z3/expr/int_expr.rb

Instance Attribute Summary

Attributes inherited from Expr

#sort

Attributes inherited from AST

#_ast

Class Method Summary collapse

Instance Method Summary collapse

Methods inherited from ArithExpr

#*, #**, #+, #-, #-@, #/, #<, #<=, #>, #>=, Div, Power, #abs, #coerce, coerce_to_same_arith_sort, #negative?, #nonzero?, #positive?, #zero?

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_int_sort(*args) ⇒ Object

Raises:



30
31
32
33
34
 
# File 'lib/z3/expr/int_expr.rb', line 30

def coerce_to_same_int_sort(*args)
  args = coerce_to_same_sort(*args)
  raise Z3::Exception, "Int value expected" unless args[0].is_a?(IntExpr)
  args
end

.Mod(a, b) ⇒ Object 



36
37
38
39
 
# File 'lib/z3/expr/int_expr.rb', line 36

def Mod(a, b)
  a, b = coerce_to_same_int_sort(a, b)
  a.sort.new(LowLevel.mk_mod(a, b))
end

.Rem(a, b) ⇒ Object 



41
42
43
44
 
# File 'lib/z3/expr/int_expr.rb', line 41

def Rem(a, b)
  a, b = coerce_to_same_int_sort(a, b)
  a.sort.new(LowLevel.mk_rem(a, b))
end

Instance Method Details

#%(other) ⇒ Object 



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

def %(other)
  IntExpr.Mod(self, other)
end

#mod(other) ⇒ Object 



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

def mod(other)
  IntExpr.Mod(self, other)
end

#rem(other) ⇒ Object 



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

def rem(other)
  IntExpr.Rem(self, other)
end

#to_i ⇒ Object 



15
16
17
18
19
20
21
22
23
24
25
26
 
# File 'lib/z3/expr/int_expr.rb', line 15

def to_i
  if ast_kind == :numeral
    LowLevel.get_numeral_string(self).to_i
  else
    obj = simplify
    if obj.ast_kind == :numeral
      LowLevel.get_numeral_string(obj).to_i
    else
      raise Z3::Exception, "Can't convert expression #{to_s} to Integer"
    end
  end
end