class ADSL::Spass::SpassTranslator::ContextCommon

Attributes

level[RW]
parent[RW]

Public Class Methods

get_common_context(c1, c2) click to toggle source
# File lib/adsl/spass/spass_translator.rb, line 69
def self.get_common_context(c1, c2)
  while c1.level > c2.level
    c1 = c1.parent
  end
  while c2.level > c1.level
    c2 = c2.parent
  end
  while c1 != c2
    c1 = c1.parent
    c2 = c2.parent
  end
  return c1
end
new(translation, name, parent) click to toggle source
# File lib/adsl/spass/spass_translator.rb, line 39
def initialize(translation, name, parent)
  @level = parent.nil? ? 0 : parent.level + 1
  @translation = translation
  @parent = parent
  
  unless parent.nil?
    @type_pred = translation.create_predicate(name, @level)
    
    translation.reserve_names @parent.p_names do |ps|
      translation.create_formula FOL::ForAll.new(ps, :c, FOL::Implies.new(
        type_pred(ps, :c), @parent.type_pred(ps)
      ))
    end
    translation.reserve_names @parent.p_names, @parent.p_names, :c do |p1s, p2s, c|
      translation.create_formula FOL::ForAll.new(p1s, p2s, :c, FOL::Implies.new(
        FOL::And.new(type_pred(p1s, c), type_pred(p2s, c)),
        FOL::PairwiseEqual.new(p1s, p2s)
      ))
    end
  end
end

Public Instance Methods

before(c2, c1var, c2var, executed_before) click to toggle source
# File lib/adsl/spass/spass_translator.rb, line 83
def before(c2, c1var, c2var, executed_before)
  c1 = self
  @translation.reserve_names((1..c1.level-1).map{|i| "parent_a#{i}"}) do |context1_names|
    @translation.reserve_names((1..c2.level-1).map{|i| "parent_b#{i}"}) do |context2_names|
      context1_names << c1var
      context2_names << c2var
      common_context = ContextCommon.get_common_context c1, c2
      prereq_formulae = FOL::And.new(c1.type_pred(context1_names), c2.type_pred(context2_names))

      solution = executed_before
      parent_args = context1_names.first(common_context.level)
      parent_args.pop
      while common_context.parent
        c1_name = context1_names[common_context.level-1]
        c2_name = context2_names[common_context.level-1]
        solution = FOL::And.new(
          FOL::Implies.new(common_context.same_level_before_formula(parent_args, c1_name, c2_name), true),
          FOL::Implies.new(common_context.same_level_before_formula(parent_args, c2_name, c1_name), false),
          FOL::Implies.new(
            FOL::Not.new(
              common_context.same_level_before_formula(parent_args, c1_name, c2_name),
              common_context.same_level_before_formula(parent_args, c2_name, c1_name)
            ),
            solution
          )
        )
        common_context = common_context.parent
        parent_args.pop
      end
      solution = FOL::Implies.new(FOL::And.new(prereq_formulae), solution)
      if context1_names.length > 1 or context2_names.length > 1
        solution = FOL::ForAll.new([context1_names[0..-2], context2_names[0..-2]], solution)
      end
      return solution
    end
  end
end
p_names(num = level) click to toggle source
# File lib/adsl/spass/spass_translator.rb, line 65
def p_names(num = level)
  num.times.map{ |i| "p#{i+1}".to_sym }
end
same_level_before_formula(parents, c1, c2) click to toggle source
# File lib/adsl/spass/spass_translator.rb, line 61
def same_level_before_formula(parents, c1, c2)
  raise 'To be implemented'
end
type_pred(*args) click to toggle source
# File lib/adsl/spass/spass_translator.rb, line 35
def type_pred(*args)
  return @level == 0 ? 'true' : @type_pred[*args.flatten]
end