Class: ADSL::Verification::FormulaBuilder

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

Overview

forward declaration

Instance Attribute Summary collapse

Instance Method Summary collapse

Methods included from 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 Utils

#classname_for_classname, #infer_classname_from_varname, #t

Constructor Details

#initialize(component = nil) ⇒ FormulaBuilder

Returns a new instance of FormulaBuilder.



152
153
154
155
 
# File 'lib/adsl/verification/formula_generators.rb', line 152

def initialize(component = nil)
  @adsl_stack = []
  @adsl_stack << component unless component.nil?
end

Instance Attribute Details

#adsl_stack ⇒ Object (readonly)

Returns the value of attribute adsl_stack.



150
151
152
 
# File 'lib/adsl/verification/formula_generators.rb', line 150

def adsl_stack
  @adsl_stack
end

Instance Method Details

#adsl_ast ⇒ Object 



202
203
204
205
206
207
208
 
# File 'lib/adsl/verification/formula_generators.rb', line 202

def adsl_ast
  elements = gather_adsl_asts
  if elements.length != 1
    raise "Invalid formula/operator stack state [#{ elements.map{ |e| e.respond_to?(:to_adsl) ? e.to_adsl : e }.join(', ') }]"
  end
  elements.first
end

#gather_adsl_asts ⇒ Object 



182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
 
# File 'lib/adsl/verification/formula_generators.rb', line 182

def gather_adsl_asts
  elements = @adsl_stack.clone
  handle_unary_operator elements, :not do |formula|
    ASTNot.new(:subformula => formula)
  end
  handle_binary_operator elements, :and do |formula1, formula2|
    ASTAnd.new(:subformulae => [formula1, formula2])
  end
  handle_binary_operator elements, :or do |formula1, formula2|
    ASTOr.new(:subformulae => [formula1, formula2])
  end
  handle_binary_operator elements, :implies do |formula1, formula2|
    ASTImplies.new(:subformula1 => formula1, :subformula2 => formula2)
  end
  handle_binary_operator elements, :equiv do |formula1, formula2|
    ASTEquiv.new(:subformula1 => formula1, :subformula2 => formula2)
  end
  elements 
end

#handle_binary_operator(elements, operator) ⇒ Object 



168
169
170
171
172
173
174
175
176
177
178
179
180
 
# File 'lib/adsl/verification/formula_generators.rb', line 168

def handle_binary_operator(elements, operator)
  until (index = elements.find_index(operator)).nil?
    raise "Binary operator `#{operator}' not infix-called" if index == 0 or index == elements.length-1
    args = [elements[index-1], elements[index+1]]
    args.each do |arg|
      raise "`#{arg}', used by operator `#{operator}', is not a formula" unless arg.is_a? ASTNode
    end
    result = yield *args
    elements.delete_at index - 1
    elements.delete_at index - 1
    elements[index - 1] = result
  end
end

#handle_unary_operator(elements, operator) ⇒ Object 



157
158
159
160
161
162
163
164
165
166
 
# File 'lib/adsl/verification/formula_generators.rb', line 157

def handle_unary_operator(elements, operator)
  until (index = elements.find_index(operator)).nil?
    raise "Unary operator `#{operator}' not prefix-called" if index == elements.length-1
    arg = elements[index+1]
    raise "`#{arg}', used by operator `#{operator}', is not a formula" unless arg.is_a? ASTNode
    result = yield arg
    elements.delete_at index
    elements[index] = result
  end
end