class Z3::AST

Attributes

_ast[R]

Private Class Methods

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

arguments() click to toggle source
# 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
ast_kind() click to toggle source
# 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
eql?(other) click to toggle source
# File lib/z3/ast.rb, line 49
def eql?(other)
  self.class == other.class and self._ast == other._ast
end
func_decl() click to toggle source
# 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
hash() click to toggle source
# File lib/z3/ast.rb, line 53
def hash
  _ast.address
end
sexpr() click to toggle source
# File lib/z3/ast.rb, line 41
def sexpr
  LowLevel.ast_to_string(self)
end
simplify() click to toggle source
# File lib/z3/ast.rb, line 45
def simplify
  sort.new(LowLevel.simplify(self))
end
to_s() click to toggle source
# File lib/z3/ast.rb, line 37
def to_s
  Printer.new.format(self)
end