Class: ADSL::Spass::SpassTranslator::ContextCommon

Inherits:
Object
  • Object
show all
Defined in:
lib/adsl/spass/spass_translator.rb

Direct Known Subclasses

ChainedContext, FlatContext

Instance Attribute Summary collapse

Class Method Summary collapse

Instance Method Summary collapse

Constructor Details

#initialize(translation, name, parent) ⇒ ContextCommon

Returns a new instance of ContextCommon.



39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
 
# 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

Instance Attribute Details

#level ⇒ Object

Returns the value of attribute level.



33
34
35
 
# File 'lib/adsl/spass/spass_translator.rb', line 33

def level
  @level
end

#parent ⇒ Object

Returns the value of attribute parent.



33
34
35
 
# File 'lib/adsl/spass/spass_translator.rb', line 33

def parent
  @parent
end

Class Method Details

.get_common_context(c1, c2) ⇒ Object 



69
70
71
72
73
74
75
76
77
78
79
80
81
 
# 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

Instance Method Details

#before(c2, c1var, c2var, executed_before) ⇒ Object 



83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
 
# 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) ⇒ Object 



65
66
67
 
# 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) ⇒ Object 



61
62
63
 
# 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) ⇒ Object 



35
36
37
 
# File 'lib/adsl/spass/spass_translator.rb', line 35

def type_pred(*args)
  return @level == 0 ? 'true' : @type_pred[*args.flatten]
end