class ADSL::DS::DSEither
Attributes
is_trues[R]
resolution_link[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