class Z3::FuncDecl

Public Class Methods

new(_ast) click to toggle source
Calls superclass method Z3::AST::new
# 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
new(_ast) click to toggle 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() click to toggle source
# File lib/z3/func_decl.rb, line 12
def arity
  LowLevel.get_arity(self)
end
domain(i) click to toggle 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() click to toggle source
# File lib/z3/func_decl.rb, line 35
def inspect
  "Z3::FuncDecl<#{name}/#{arity}>"
end
name() click to toggle source
# File lib/z3/func_decl.rb, line 8
def name
  LowLevel.get_symbol_string(LowLevel.get_decl_name(self))
end
range() click to toggle source
# File lib/z3/func_decl.rb, line 22
def range
  Sort.from_pointer(LowLevel::get_range(self))
end
to_s() click to toggle source

def ast_parameter(i)

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

end

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