class Z3::AST

# File lib/z3/ast.rb, line 28
def arguments
  raise Z3::Exception, "Only app ASTs can have arguments" unless ast_kind == :app
  num = LowLevel::get_app_num_args(self)
  (0...num).map do |i|
    _ast = LowLevel::get_app_arg(self, i)
    Expr.new_from_pointer(_ast)
  end
end

# File lib/z3/ast.rb, line 9
def ast_kind
  ast_kind_lookup = {
    0 => :numeral,
    1 => :app,
    2 => :var,
    3 => :quantifier,
    4 => :sort,
    5 => :func_decl,
    1000 => :unknown,
  }
  kind_id = LowLevel.get_ast_kind(self)
  ast_kind_lookup[kind_id] or raise Z3::Exception, "Unknown AST kind #{kind_id}"
end

# File lib/z3/ast.rb, line 49
def eql?(other)
  self.class == other.class and self._ast == other._ast
end

# File lib/z3/ast.rb, line 23
def func_decl
  raise Z3::Exception, "Only app ASTs can have func decls" unless ast_kind == :app
  FuncDecl.new(LowLevel::get_app_decl(self))
end

# File lib/z3/ast.rb, line 53
def hash
  _ast.address
end

# File lib/z3/ast.rb, line 41
def sexpr
  LowLevel.ast_to_string(self)
end

# File lib/z3/ast.rb, line 45
def simplify
  sort.new(LowLevel.simplify(self))
end

# File lib/z3/ast.rb, line 37
def to_s
  Printer.new.format(self)
end