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