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