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, #coerce, coerce_to_same_arith_sort

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, #func_decl, #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:



26
27
28
29
30
 
# File 'lib/z3/expr/int_expr.rb', line 26

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 



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

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 



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

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

#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 



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

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

#to_i ⇒ Object 



11
12
13
14
15
16
17
18
19
20
21
22
 
# File 'lib/z3/expr/int_expr.rb', line 11

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