Class: Z3::IntSort

Inherits:
Sort show all
Defined in:
lib/z3/sort/int_sort.rb

Instance Attribute Summary

Attributes inherited from AST

#_ast

Instance Method Summary collapse

Methods inherited from Sort

#<, #<=, #<=>, #==, #>, #>=, #cast, #eql?, from_pointer, #from_value, #hash, #inspect, #new, #to_s, #value_class, #var

Methods inherited from AST

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

Constructor Details

#initialize ⇒ IntSort

Returns a new instance of IntSort.



3
4
5
 
# File 'lib/z3/sort/int_sort.rb', line 3

def initialize
  super LowLevel.mk_int_sort
end

Instance Method Details

#expr_class ⇒ Object 



7
8
9
 
# File 'lib/z3/sort/int_sort.rb', line 7

def expr_class
  IntExpr
end

#from_const(val) ⇒ Object 



11
12
13
14
15
16
17
 
# File 'lib/z3/sort/int_sort.rb', line 11

def from_const(val)
  if val.is_a?(Integer)
    new(LowLevel.mk_numeral(val.to_s, self))
  else
    raise Z3::Exception, "Cannot convert #{val.class} to #{self.class}"
  end
end