Class: ADSL::Spass::SpassTranslator::ChainedContext

Inherits:
ContextCommon show all
Includes:
FOL
Defined in:
lib/adsl/spass/spass_translator.rb

Instance Attribute Summary collapse

Attributes inherited from ContextCommon

#level, #parent

Instance Method Summary collapse

Methods inherited from ContextCommon

#before, get_common_context, #p_names, #type_pred

Constructor Details

#initialize(translation, name, parent) ⇒ ChainedContext

Returns a new instance of ChainedContext.



136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
 
# File 'lib/adsl/spass/spass_translator.rb', line 136

def initialize(translation, name, parent)
  super

  @before_pred = translation.create_predicate "#{@type_pred.name}_before", @type_pred.arity + 1
  @just_before = translation.create_predicate "#{@type_pred.name}_just_before", @type_pred.arity + 1
  @first = translation.create_predicate "#{@type_pred.name}_first", @type_pred.arity
  @last = translation.create_predicate "#{@type_pred.name}_last", @type_pred.arity

  ps = []
  (@type_pred.arity-1).times{ |i| ps << "p#{i}" }
  translation.create_formula _for_all(ps, :c, _not(@before_pred[ps, :c, :c]))
  translation.create_formula _for_all(ps, :c1, :c2, _implies(@before_pred[ps, :c1, :c2], _and(
    @type_pred[ps, :c1],
    @type_pred[ps, :c2],
    _not(@before_pred[ps, :c2, :c1]),
    _implies(
      _and(@type_pred[ps, :c1], @type_pred[ps, :c2]),
      _or(_equal(:c1, :c2), @before_pred[ps, :c1, :c2], @before_pred[ps, :c2, :c1])
    )
  )))
  translation.create_formula _for_all(ps, :c1, :c2, :c3, _implies(
    _and(@before_pred[ps, :c1, :c2], @before_pred[ps, :c2, :c3]),
    @before_pred[ps, :c1, :c3]
  ))
  translation.create_formula _for_all(ps, :c1, :c2, _equiv(
    @just_before[ps, :c1, :c2],
    _and(
      @before_pred[ps, :c1, :c2],
      _not(_exists(:mid, _and(@before_pred[ps, :c1, :mid], @before_pred[ps, :mid, :c2])))
    )
  ))
  translation.create_formula _for_all(ps, _and(
    _equiv(
      _exists(:c, @type_pred[ps, :c]),
      _exists(:c, @first[ps, :c]),
      _exists(:c, @last[ps, :c])
    ),
    _for_all(ps, :c, _implies(
      @type_pred[ps, :c],
      _one_of(@last[ps, :c], _exists(:next, @just_before[ps, :c, :next]))
    )),
    _for_all(ps, :c, _equiv(@first[ps, :c],
      _and(@type_pred[ps, :c], _not(_exists(:pre, @before_pred[ps, :pre, :c])))
    )),
    _for_all(ps, :c, _equiv(@last[ps, :c],
      _and(@type_pred[ps, :c], _not(_exists(:post, @before_pred[ps, :c, :post])))
    ))
  ))
end

Instance Attribute Details

#before_pred ⇒ Object

Returns the value of attribute before_pred.



133
134
135
 
# File 'lib/adsl/spass/spass_translator.rb', line 133

def before_pred
  @before_pred
end

#first ⇒ Object

Returns the value of attribute first.



133
134
135
 
# File 'lib/adsl/spass/spass_translator.rb', line 133

def first
  @first
end

#just_before ⇒ Object

Returns the value of attribute just_before.



133
134
135
 
# File 'lib/adsl/spass/spass_translator.rb', line 133

def just_before
  @just_before
end

#last ⇒ Object

Returns the value of attribute last.



133
134
135
 
# File 'lib/adsl/spass/spass_translator.rb', line 133

def last
  @last
end

Instance Method Details

#same_level_before_formula(ps, c1, c2) ⇒ Object 



186
187
188
 
# File 'lib/adsl/spass/spass_translator.rb', line 186

def same_level_before_formula(ps, c1, c2)
  @before_pred[ps, c1, c2]
end