class Z3::AST

Public Class Methods

Source

# File lib/z3/ast.rb, line 63
def self.describe(value)
  case value
  when NilClass, TrueClass, FalseClass, Symbol
    value.inspect
  when Expr
    value.sort
  else
    value.class
  end
end

How a value gets named in an error message. Ruby writes nil / true / false literally and everything else by class - ‘Integer(nil)` says “can’t convert nil into Integer”, not “can’t convert NilClass into Integer” - and an Expr goes by its sort, which is what any mismatch involving one is really about. A Symbol joins the literal group: it’s an enum value, and which one it was is the whole of what went wrong.

Public Instance Methods

arguments ()

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 ()

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)

Source

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

func_decl ()

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 ()

Source

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

sexpr ()

Source

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

simplify ()

Source

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

to_s ()

Source

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