class ADSL::DS::DSFlatForEach

Public Instance Methods

create_iteration_formulae(translation) click to toggle source
# File lib/adsl/spass/spass_ds_extensions.rb, line 579
def create_iteration_formulae(translation)
  context = translation.context
  translation.reserve_names context.p_names, :o, :c1, :c2 do |ps, o, c1, c2|
    ps_without_last = ps.first(ps.length - 1)
    translation.create_formula _for_all(ps, o, _implies(
      @context.type_pred(ps),
      _equiv(@pre_state[ps_without_last, o], @pre_iteration_state[ps, o])
    ))
    translation.create_formula _for_all(ps_without_last, o, _if_then_else(
      _not(_exists(ps.last, @context.type_pred(ps))),
      _equiv(@pre_state[ps_without_last, o], @post_state[ps_without_last, o]),
      _implies(
        @context.parent.type_pred(ps_without_last),
        _equiv(
          @post_state[ps_without_last, o],
          _or(
            _and(
              @pre_state[ps_without_last, o],
              _for_all(ps.last, _implies(
                @context.type_pred(ps),
                @post_iteration_state[ps, o]
              ))
            ),
            _and(
              _not(@pre_state[ps_without_last, o]),
              _exists(ps.last, @post_iteration_state[ps, o])
            )
          )
        )
      )
    ))
  end
end
prepare(translation) click to toggle source
# File lib/adsl/spass/spass_ds_extensions.rb, line 575
def prepare(translation)
  prepare_with_context(translation, true)
end