Class: Z3::FuncDecl

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

Constant Summary collapse

PARAMETER_KINDS =

Decl parameters are the _-part of an indexed decl like (_ map or), (_ extract 7 0), (_ zero_extend 8). They have nothing to do with the domain, so they're not counted by #arity.

{
  0 => :int,
  1 => :double,
  2 => :rational,
  3 => :symbol,
  4 => :sort,
  5 => :ast,
  6 => :func_decl,
  7 => :internal,
  8 => :zstring,
}

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

#func_decl_parameter(i) ⇒ Object

Raises:



51
52
53
54
 
# File 'lib/z3/func_decl.rb', line 51

def func_decl_parameter(i)
  raise Z3::Exception, "Parameter #{i} is a #{parameter_kind(i)}, not a func decl" unless parameter_kind(i) == :func_decl
  FuncDecl.new(LowLevel.get_decl_func_decl_parameter(self, i))
end

#inspect ⇒ Object 



60
61
62
 
# File 'lib/z3/func_decl.rb', line 60

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

#num_parameters ⇒ Object 



41
42
43
 
# File 'lib/z3/func_decl.rb', line 41

def num_parameters
  LowLevel.get_decl_num_parameters(self)
end

#parameter_kind(i) ⇒ Object

Raises:



45
46
47
48
49
 
# File 'lib/z3/func_decl.rb', line 45

def parameter_kind(i)
  raise Z3::Exception, "Trying to access parameter #{i} but decl has #{num_parameters} parameters" if i < 0 or i >= num_parameters
  k = LowLevel.get_decl_parameter_kind(self, i)
  PARAMETER_KINDS.fetch(k) { raise Z3::Exception, "Unknown decl parameter kind #{k}" }
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 



56
57
58
 
# File 'lib/z3/func_decl.rb', line 56

def to_s
  name
end