class ADSL::DS::DSEither

Attributes

is_trues[R]

Public Instance Methods

migrate_state_spass(translation) click to toggle source
# File lib/adsl/spass/spass_ds_extensions.rb, line 404
def migrate_state_spass(translation)
  post_state = translation.create_state :post_either
  prev_state = translation.prev_state
  context = translation.context

  pre_states = []
  post_states = []
  @blocks.length.times do |i|
    pre_states << translation.create_state(:pre_of_either)
  end
  translation.create_formula FOL::ForAll.new(:r, FOL::Implies.new(
    translation.is_either_resolution[:r],
    FOL::OneOf.new(is_trues.map{ |pred| pred[:r] })
  ))

  translation.reserve_names context.p_names, :resolution, :o do |ps, resolution, o|
    translation.create_formula FOL::ForAll.new(ps, FOL::Implies.new(
      translation.context.type_pred(ps),
      FOL::Exists.new(resolution, FOL::And.new(
        @resolution_link[ps, resolution],
        FOL::And.new((0..@blocks.length-1).map { |i|
          FOL::Equiv.new(is_trues[i][resolution], FOL::ForAll.new(o, FOL::Equiv.new(prev_state[ps, o], pre_states[i][ps, o])))
        })
      ))
    ))
  end

  @blocks.length.times do |i|
    translation.prev_state = pre_states[i]
    @blocks[i].migrate_state_spass translation
    post_states << translation.prev_state
  end
    
  translation.reserve_names context.p_names, :resolution, :o do |ps, resolution, o|
    translation.create_formula FOL::ForAll.new(ps, FOL::Implies.new(
      translation.context.type_pred(ps),
      FOL::Exists.new(resolution, FOL::And.new(
        @resolution_link[ps, resolution],
        FOL::And.new((0..@blocks.length-1).map { |i|
          FOL::Equiv.new(is_trues[i][resolution], FOL::ForAll.new(o, FOL::Equiv.new(post_state[ps, o], post_states[i][ps, o])))
        })
      ))
    ))
  end
  
  translation.prev_state = post_state
end
prepare(translation) click to toggle source
# File lib/adsl/spass/spass_ds_extensions.rb, line 385
def prepare(translation)
  context = translation.context
  @resolution_link = translation.create_predicate :resolution_link, context.level+1
  translation.reserve_names context.p_names, :r do |ps, r|
    translation.gen_formula_for_unique_arg(@resolution_link, (0..ps.length-1), ps.length)
    translation.create_formula _for_all(ps, r, _implies(@resolution_link[ps, r], _and(
      translation.context.type_pred(ps),
      translation.is_either_resolution[r]
    )))
  end
  @is_trues = []
  @blocks.length.times do |i|
    is_trues << translation.create_predicate("either_resolution_#{i}_is_true", 1)
  end
  @blocks.each do |block|
    block.prepare(translation)
  end
end