Class: Z3::FuncDecl

Inherits:
AST
  • Object
show all
Defined in:
lib/z3/func_decl.rb

Instance Attribute Summary

Attributes inherited from AST

#_ast

Instance Method Summary collapse

Methods inherited from AST

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

Constructor Details

#initialize(_ast) ⇒ FuncDecl

Returns a new instance of FuncDecl.

Raises:



3
4
5
6
 
# File 'lib/z3/func_decl.rb', line 3

def initialize(_ast)
  super(_ast)
  raise Z3::Exception, "FuncDecls must have AST kind func decl" unless ast_kind == :func_decl
end

Instance Method Details

#arity ⇒ Object 



12
13
14
 
# File 'lib/z3/func_decl.rb', line 12

def arity
  LowLevel.get_arity(self)
end

#domain(i) ⇒ Object

Raises:



16
17
18
19
20
 
# File 'lib/z3/func_decl.rb', line 16

def domain(i)
  a = arity
  raise Z3::Exception, "Trying to access domain #{i} but function arity is #{a}" if i < 0 or i >= a
  Sort.from_pointer(LowLevel::get_domain(self, i))
end

#inspect ⇒ Object 



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

def inspect
  "Z3::FuncDecl<#{name}/#{arity}>"
end

#name ⇒ Object 



8
9
10
 
# File 'lib/z3/func_decl.rb', line 8

def name
  LowLevel.get_symbol_string(LowLevel.get_decl_name(self))
end

#range ⇒ Object 



22
23
24
 
# File 'lib/z3/func_decl.rb', line 22

def range
  Sort.from_pointer(LowLevel::get_range(self))
end

#to_s ⇒ Object

def ast_parameter(i)

# vs arity ?
Z3::Ast.new(LowLevel.get_decl_ast_parameter(self, i))

end



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

def to_s
  name
end