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