class ADSL::Spass::SpassTranslator::Translation

Attributes

all_contexts[R]
classes[R]
conjectures[R]
context[RW]
create_obj_stmts[R]
delete_obj_stmts[R]
existed_initially[R]
exists_finally[R]
invariant_state[RW]
is_either_resolution[R]
is_object[R]
is_tuple[R]
prev_state[RW]
resolved_as_true[R]
root_context[R]

Public Class Methods

new() click to toggle source
# File lib/adsl/spass/spass_translator.rb, line 200
def initialize
  @classes = []
  @temp_vars = []
  @functions = []
  @predicates = []
  @formulae = [[]]
  @conjectures = []
  @all_contexts = []
  @existed_initially = create_predicate :existed_initially, 1
  @exists_finally = create_predicate :exists_finally, 1
  @is_object = create_predicate :is_object, 1
  @is_tuple = create_predicate :is_tuple, 1
  @is_either_resolution = create_predicate :is_either_resolution, 1
  @root_context = create_context 'root_context', true, nil
  @context = @root_context
  # {class => [[before_stmt, context], [after_stmt, context]]}
  @create_obj_stmts = Hash.new{ |hash, klass| hash[klass] = [] }
  @delete_obj_stmts = Hash.new{ |hash, klass| hash[klass] = [] }
  @prev_state = create_state :init_state

  @invariant_state = nil
end

Public Instance Methods

_reserve_names(*names) click to toggle source
# File lib/adsl/spass/spass_translator.rb, line 294
def _reserve_names(*names)
  result = []
  names.each do |name|
    if name.is_a? Array
      result << _reserve_names(*name)
    else
      while @temp_vars.include? name
        name = name.to_s.increment_suffix.to_sym
      end
      @temp_vars.push name
      result << name
    end
  end
  result
end
create_conjecture(formula) click to toggle source
# File lib/adsl/spass/spass_translator.rb, line 258
def create_conjecture(formula)
  raise ArgumentError, 'Formula not resolveable to Spass' unless formula.class.method_defined? :resolve_spass
  @conjectures.push formula
end
create_context(name, flat, parent) click to toggle source
# File lib/adsl/spass/spass_translator.rb, line 234
def create_context(name, flat, parent)
  context = nil
  if flat
    context = FlatContext.new self, name, parent
  else
    context = ChainedContext.new self, name, parent
  end
  @all_contexts << context
  context
end
create_formula(formula) click to toggle source
# File lib/adsl/spass/spass_translator.rb, line 253
def create_formula(formula)
  raise ArgumentError, 'Formula not resolveable to Spass' unless formula.class.method_defined? :resolve_spass
  @formulae.last.push formula
end
create_function(name, arity) click to toggle source
# File lib/adsl/spass/spass_translator.rb, line 263
def create_function(name, arity)
  function = Predicate.new get_pred_name(name.to_s), arity
  @functions << function
  function
end
create_predicate(name, arity) click to toggle source
# File lib/adsl/spass/spass_translator.rb, line 269
def create_predicate(name, arity)
  pred = Predicate.new get_pred_name(name.to_s), arity
  @predicates << pred
  pred
end
create_state(name) click to toggle source
# File lib/adsl/spass/spass_translator.rb, line 223
def create_state name
  state = create_predicate name, @context.level + 1
  reserve_names([:c_1] * @context.level, :o) do |cs, o|
    create_formula FOL::ForAll.new(cs, o, FOL::Implies.new(
      state[cs, o],
      FOL::And.new(@context.type_pred(cs), FOL::Or.new(@is_object[o], @is_tuple[o]))
    ))
  end
  state
end
gen_formula_for_unique_arg(pred, *args) click to toggle source
# File lib/adsl/spass/spass_translator.rb, line 319
def gen_formula_for_unique_arg(pred, *args)
  individuals = []
  args.each do |arg|
    arg = arg.is_a?(Range) ? arg.to_a : [arg].flatten
    next if arg.empty?
    vars1 = (1..pred.arity).map{ |i| "e#{i}" }
    vars2 = vars1.dup
    as = []
    bs = []
    arg.each do |index|
      a = "a#{index+1}".to_sym
      vars1[index] = a
      b = "b#{index+1}".to_sym
      vars2[index] = b
      as << a
      bs << b
    end
    reserve_names (vars1 | vars2) do
      individuals << _for_all(vars1 | vars2, _implies(_and(pred[vars1], pred[vars2]), _pairwise_equal(as, bs)))
    end
  end
  return true if individuals.empty?
  formula = _and(individuals)
  create_formula formula
  return formula
end
get_pred_name(common_name) click to toggle source
# File lib/adsl/spass/spass_translator.rb, line 275
def get_pred_name common_name
  registered_names = (@functions + @predicates).map{ |a| a.name }
  prefix = common_name
  prefix = common_name.scan(/^(.+)_\d+$/).first.first if prefix =~ /^.+_\d+$/
  regexp = /^#{ Regexp.escape prefix }(?:_(\d+))?$/

  already_registered = registered_names.select{ |a| a =~ regexp }
  return common_name if already_registered.empty?
  
  rhs_numbers = already_registered.map{ |a| [a, a.scan(regexp).first.first] }
  
  rhs_numbers.each do |a|
    a[1] = a[1].nil? ? -1 : a[1].to_i
  end

  max_name = rhs_numbers.max_by{ |a| a[1] }
  return max_name[0].increment_suffix
end
pop_formula_frame() click to toggle source
# File lib/adsl/spass/spass_translator.rb, line 249
def pop_formula_frame
  @formulae.pop
end
push_formula_frame() click to toggle source
# File lib/adsl/spass/spass_translator.rb, line 245
def push_formula_frame
  @formulae.push []
end
reserve_names(*names) { |*result| ... } click to toggle source
# File lib/adsl/spass/spass_translator.rb, line 310
def reserve_names(*names)
  result = _reserve_names(*names)
  yield *result
ensure
  names.flatten.length.times do
    @temp_vars.pop
  end 
end
spass_list_of(what, *content) click to toggle source
# File lib/adsl/spass/spass_translator.rb, line 351
def spass_list_of(what, *content)
  spass_wrap "list_of_#{what.to_s}.%s\nend_of_list.", content.flatten.map{ |c| "\n  " + c.to_s }.join("")
end
spass_wrap(with, what) click to toggle source
# File lib/adsl/spass/spass_translator.rb, line 346
def spass_wrap(with, what)
  return "" if what.length == 0
  return with % what
end
to_spass_string() click to toggle source
# File lib/adsl/spass/spass_translator.rb, line 355
        def to_spass_string
          functions = @functions.map{ |f| "(#{f.name}, #{f.arity})" }.join(", ")
          predicates = @predicates.map{ |p| "(#{p.name}, #{p.arity})" }.join(", ")
          formulae = @formulae.first.map do |f|
            begin
              next "formula(#{f.resolve_spass})."
            rescue => e
              pp f
              raise e
            end
          end
          conjectures = @conjectures.map{ |f| "formula(#{f.resolve_spass})." }
          <<-SPASS
          begin_problem(Blahblah).
          list_of_descriptions.
            name({* *}).
            author({* *}).
            status(satisfiable).
            description( {* *} ).
          end_of_list.
          #{spass_list_of( :symbols,
            spass_wrap("functions[%s].", functions),
            spass_wrap("predicates[%s].", predicates)
          )}
          #{spass_list_of( "formulae(axioms)",
            formulae
          )}
          #{spass_list_of( "formulae(conjectures)",
            conjectures
          )}
          end_problem.
          SPASS
        end