Class: ADSL::Parser::ASTNode

Inherits:
Object
  • Object
show all
Includes:
Verification::FormulaGenerators
Defined in:
lib/adsl/parser/ast_nodes.rb,
lib/adsl/verification/formula_generators.rb

Class Method Summary collapse

Instance Method Summary collapse

Methods included from Verification::FormulaGenerators

#[], #and, #binary_op, #binary_op_with_any_number_of_params, #equiv, #exists, #false, #forall, #handle_quantifier, #implies, #in_formula_builder, #not, #or, #true

Methods included from Verification::Utils

#classname_for_classname, #infer_classname_from_varname, #t

Class Method Details

.is_formula? ⇒ Boolean

Returns:

  • (Boolean) 


28
29
30
 
# File 'lib/adsl/parser/ast_nodes.rb', line 28

def self.is_formula?
  @is_formula
end

.is_objset? ⇒ Boolean

Returns:

  • (Boolean) 


24
25
26
 
# File 'lib/adsl/parser/ast_nodes.rb', line 24

def self.is_objset?
  @is_objset
end

.is_statement? ⇒ Boolean

Returns:

  • (Boolean) 


20
21
22
 
# File 'lib/adsl/parser/ast_nodes.rb', line 20

def self.is_statement?
  @is_statement
end

.node_type(*fields) ⇒ Object 



36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
 
# File 'lib/adsl/parser/ast_nodes.rb', line 36

def self.node_type(*fields)
  options = {}
  if fields.last.is_a? Hash
    options.merge! fields.pop
  end

  if options.include?(:type) and !options.include?(:types)
    options[:types] = [options[:type]]
  end
  if options.include?(:types)
    @is_statement = options[:types].include? :statement
    @is_objset = options[:types].include? :objset
    @is_formula = options[:types].include? :formula
  end

  container_for *fields
  container_for :lineno
end

Instance Method Details

#==(other) ⇒ Object Also known as: eql? 



105
106
107
108
109
110
111
112
113
 
# File 'lib/adsl/parser/ast_nodes.rb', line 105

def ==(other)
  return false unless self.class == other.class
  self.class.container_for_fields.each do |field_name|
    child1 = self.send field_name
    child2 = other.send field_name
    return false unless child1 == child2
  end
  true
end

#adsl_ast ⇒ Object 



55
56
57
 
# File 'lib/adsl/parser/ast_nodes.rb', line 55

def adsl_ast
  self
end

#adsl_ast_size ⇒ Object

used for statistics



135
136
137
138
139
140
141
142
143
144
145
146
147
148
 
# File 'lib/adsl/parser/ast_nodes.rb', line 135

def adsl_ast_size
  sum = 1
  self.class.container_for_fields.each do |field_name|
    field = send field_name
    if field.is_a? Array
      field.flatten.each do |subfield|
        sum += subfield.adsl_ast_size if subfield.respond_to? :adsl_ast_size
      end
    else
      sum += field.adsl_ast_size if field.respond_to? :adsl_ast_size
    end
  end
  sum
end

#block_replace(&block) ⇒ Object 



83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
 
# File 'lib/adsl/parser/ast_nodes.rb', line 83

def block_replace(&block)
  children = self.class.container_for_fields.map{ |field_name| [field_name, send(field_name)] }
  children.each do |name, value|
    new_value = if value.is_a? Array
      value.map do |e|
        new_e = e.block_replace(&block)
        new_e.nil? ? e.dup : new_e
      end
    elsif value.is_a? ASTNode
      new_value = value.block_replace(&block)
      new_value.nil? ? value.dup : new_value
    elsif value.is_a?(Symbol) || value.nil?
      value
    else
      value.dup
    end
    send("#{name}=", new_value) if new_value != value
  end
  new_value = block[self]
  new_value.nil? ? self.dup : new_value
end

#dup ⇒ Object 



70
71
72
73
74
75
76
77
78
79
80
81
 
# File 'lib/adsl/parser/ast_nodes.rb', line 70

def dup
  new_values = {}
  self.class.container_for_fields.each do |field_name|
    value = send field_name
    new_values[field_name] = if value.is_a?(Symbol) || value.nil?
      value
    else
      value.dup
    end
  end
  self.class.new new_values
end

#hash ⇒ Object 



116
117
118
 
# File 'lib/adsl/parser/ast_nodes.rb', line 116

def hash
  [self.class, *self.class.container_for_fields.map{ |field_name| send field_name }].hash
end

#objset_has_side_effects? ⇒ Boolean

Returns:

  • (Boolean) 


32
33
34
 
# File 'lib/adsl/parser/ast_nodes.rb', line 32

def objset_has_side_effects?
  false
end

#optimize ⇒ Object 



59
60
61
62
63
64
65
66
67
68
 
# File 'lib/adsl/parser/ast_nodes.rb', line 59

def optimize
  copy = self.dup
  children = self.class.container_for_fields.map{ |field_name| [field_name, copy.send(field_name)] }
  until children.empty?
    child_name, child = children.pop
    new_value = child.respond_to?(:optimize) ? child.optimize : child.dup
    copy.send "#{child_name}=", new_value unless new_value.equal? child
  end
  copy
end

#preorder_traverse(&block) ⇒ Object 



120
121
122
123
124
125
126
127
128
129
130
131
132
 
# File 'lib/adsl/parser/ast_nodes.rb', line 120

def preorder_traverse(&block)
  self.class.container_for_fields.each do |field_name|
    field = send field_name
    if field.is_a? Array
      field.flatten.each do |subfield|
        subfield.preorder_traverse &block if subfield.respond_to? :preorder_traverse
      end
    else
      field.preorder_traverse &block if field.respond_to? :preorder_traverse
    end
  end
  block[self]
end