Class: Z3::AST

Inherits:
Object
  • Object
show all
Defined in:
lib/z3/ast.rb

Direct Known Subclasses

Expr, FuncDecl, Sort

Instance Attribute Summary collapse

Instance Method Summary collapse

Constructor Details

#initialize(_ast) ⇒ AST

Returns a new instance of AST.

Raises:



4
5
6
7
 
# 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

Instance Attribute Details

#_ast ⇒ Object (readonly)

Returns the value of attribute _ast.



3
4
5
 
# File 'lib/z3/ast.rb', line 3

def _ast
  @_ast
end

Instance Method Details

#arguments ⇒ Object

Raises:



28
29
30
31
32
33
34
35
 
# 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 ⇒ Object 



9
10
11
12
13
14
15
16
17
18
19
20
21
 
# 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) ⇒ Boolean

Returns:

  • (Boolean) 


49
50
51
 
# File 'lib/z3/ast.rb', line 49

def eql?(other)
  self.class == other.class and self._ast == other._ast
end

#func_decl ⇒ Object

Raises:



23
24
25
26
 
# 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 ⇒ Object 



53
54
55
 
# File 'lib/z3/ast.rb', line 53

def hash
  _ast.address
end

#sexpr ⇒ Object 



41
42
43
 
# File 'lib/z3/ast.rb', line 41

def sexpr
  LowLevel.ast_to_string(self)
end

#simplify ⇒ Object 



45
46
47
 
# File 'lib/z3/ast.rb', line 45

def simplify
  sort.new(LowLevel.simplify(self))
end

#to_s ⇒ Object 



37
38
39
 
# File 'lib/z3/ast.rb', line 37

def to_s
  Printer.new.format(self)
end