class ADSL::DS::DSRelation

Attributes

type_pred[R]

Public Instance Methods

[](variable) click to toggle source
# File lib/adsl/spass/spass_ds_extensions.rb, line 168
def [](variable)
  @type_pred[variable]
end
to_s() click to toggle source
# File lib/adsl/ds/data_store_spec.rb, line 90
def to_s
  "#{from_class.name}.#{name}"
end
translate(translation) click to toggle source
# File lib/adsl/spass/spass_ds_extensions.rb, line 172
def translate(translation)
  if @inverse_of
    @type_pred = @inverse_of.type_pred
    @left_link = @inverse_of.right_link
    @right_link = @inverse_of.left_link
  else
    @type_pred = translation.create_predicate "of_#{@from_class.name}_#{@name}_type", 1
    @left_link = translation.create_predicate "left_link_#{@from_class.name}_#{@name}", 2
    @right_link = translation.create_predicate "right_link_#{@from_class.name}_#{@name}", 2
    translation.create_formula _for_all(:t, :o, _implies(@left_link[:t, :o], _and(@from_class[:o], @type_pred[:t])))
    translation.create_formula _for_all(:t, :o, _implies(@right_link[:t, :o], _and(@to_class[:o], @type_pred[:t])))
    translation.create_formula _for_all(:t, :o1, :o2, _and(
      _implies(_and(@left_link[:t, :o1], @left_link[:t, :o2]), _equal(:o1, :o2)),
      _implies(_and(@right_link[:t, :o1], @right_link[:t, :o2]), _equal(:o1, :o2))
    ))
    translation.create_formula _for_all(:t, _implies(
      @type_pred[:t],
      _exists(:o1, :o2, _and(@left_link[:t, :o1], @right_link[:t, :o2]))
    ))
  end

  if @cardinality[0] > 0
    translation.create_formula _for_all(:o, _implies(@from_class[:o], _exists(:t, @left_link[:t, :o])))
  end
  if @cardinality[1] == 1
    translation.create_formula _for_all(:o, :t1, :t2, _implies(
      _and(@left_link[:t1, :o], @left_link[:t2, :o]),
      _equal(:t1, :t2)
    ))  
  end
end