class ADSL::Spass::SpassTranslator::ChainedContext

Attributes

before_pred[RW]
first[RW]
just_before[RW]
last[RW]

Public Class Methods

new(translation, name, parent) click to toggle source
# 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

Public Instance Methods

same_level_before_formula(ps, c1, c2) click to toggle source
# File lib/adsl/spass/spass_translator.rb, line 186
def same_level_before_formula(ps, c1, c2)
  @before_pred[ps, c1, c2]
end