class Z3::FuncDecl

Public Class Methods

Source

# 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

Calls superclass method

new (_ast)

Source

# File lib/z3/ast.rb, line 4
def initialize(_ast)
  raise Z3::Exception, "AST expected, got #{_ast.class}" unless _ast.is_a?(FFI::Pointer)
  @_ast = _ast
end

Public Instance Methods

arity ()

Source

# File lib/z3/func_decl.rb, line 12
def arity
  LowLevel.get_arity(self)
end

domain (i)

Source

# 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 ()

Source

# File lib/z3/func_decl.rb, line 35
def inspect
  "Z3::FuncDecl<#{name}/#{arity}>"
end

name ()

Source

# File lib/z3/func_decl.rb, line 8
def name
  LowLevel.get_symbol_string(LowLevel.get_decl_name(self))
end

range ()

Source

# File lib/z3/func_decl.rb, line 22
def range
  Sort.from_pointer(LowLevel::get_range(self))
end

to_s ()

Source

# File lib/z3/func_decl.rb, line 31
def to_s
  name
end

def ast_parameter(i)

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

end