class ADSL::DS::DSVariable

Attributes

context[RW]
pred[RW]

Public Instance Methods

[](*args) click to toggle source
# File lib/adsl/spass/spass_ds_extensions.rb, line 677
def [](*args)
  @pred[args]
end
action_name() click to toggle source
# File lib/adsl/spass/spass_ds_extensions.rb, line 651
def action_name
  "var_#{@name}"
end
define_predicate(translation) click to toggle source
# File lib/adsl/spass/spass_ds_extensions.rb, line 660
def define_predicate(translation)
  @context = translation.context
  @pred = translation.create_predicate action_name, context.level + 1
end
invariant_name() click to toggle source
# File lib/adsl/spass/spass_ds_extensions.rb, line 669
def invariant_name
  "invariant_var_#{@name}"
end
prepare_action(translation) click to toggle source

The predicate is not defined in prepare_action as we want the predicate to be defined only when assigning to the variable not when using it a nil check does not work because it makes the translation non-reusable

# File lib/adsl/spass/spass_ds_extensions.rb, line 659
def prepare_action(translation); end
resolve_action_objset(translation, ps, var) click to toggle source
# File lib/adsl/spass/spass_ds_extensions.rb, line 665
def resolve_action_objset(translation, ps, var)
  return @pred[ps.first(@context.level), var]
end
resolve_invariant_objset(translation, var) click to toggle source
# File lib/adsl/spass/spass_ds_extensions.rb, line 673
def resolve_invariant_objset(translation, var)
  FOL::Equal.new(invariant_name, var)
end