Class: ADSL::Spass::SpassTranslator::Translation

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

Instance Attribute Summary collapse

Instance Method Summary collapse

Constructor Details

#initialize ⇒ Translation

Returns a new instance of Translation.



200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
 
# 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

Instance Attribute Details

#all_contexts ⇒ Object (readonly)

Returns the value of attribute all_contexts.



195
196
197
 
# File 'lib/adsl/spass/spass_translator.rb', line 195

def all_contexts
  @all_contexts
end

#classes ⇒ Object (readonly)

Returns the value of attribute classes.



195
196
197
 
# File 'lib/adsl/spass/spass_translator.rb', line 195

def classes
  @classes
end

#conjectures ⇒ Object (readonly)

Returns the value of attribute conjectures.



196
197
198
 
# File 'lib/adsl/spass/spass_translator.rb', line 196

def conjectures
  @conjectures
end

#context ⇒ Object

Returns the value of attribute context.



192
193
194
 
# File 'lib/adsl/spass/spass_translator.rb', line 192

def context
  @context
end

#create_obj_stmts ⇒ Object (readonly)

Returns the value of attribute create_obj_stmts.



195
196
197
 
# File 'lib/adsl/spass/spass_translator.rb', line 195

def create_obj_stmts
  @create_obj_stmts
end

#delete_obj_stmts ⇒ Object (readonly)

Returns the value of attribute delete_obj_stmts.



195
196
197
 
# File 'lib/adsl/spass/spass_translator.rb', line 195

def delete_obj_stmts
  @delete_obj_stmts
end

#existed_initially ⇒ Object (readonly)

Returns the value of attribute existed_initially.



193
194
195
 
# File 'lib/adsl/spass/spass_translator.rb', line 193

def existed_initially
  @existed_initially
end

#exists_finally ⇒ Object (readonly)

Returns the value of attribute exists_finally.



193
194
195
 
# File 'lib/adsl/spass/spass_translator.rb', line 193

def exists_finally
  @exists_finally
end

#invariant_state ⇒ Object

Returns the value of attribute invariant_state.



192
193
194
 
# File 'lib/adsl/spass/spass_translator.rb', line 192

def invariant_state
  @invariant_state
end

#is_either_resolution ⇒ Object (readonly)

Returns the value of attribute is_either_resolution.



194
195
196
 
# File 'lib/adsl/spass/spass_translator.rb', line 194

def is_either_resolution
  @is_either_resolution
end

#is_object ⇒ Object (readonly)

Returns the value of attribute is_object.



194
195
196
 
# File 'lib/adsl/spass/spass_translator.rb', line 194

def is_object
  @is_object
end

#is_tuple ⇒ Object (readonly)

Returns the value of attribute is_tuple.



194
195
196
 
# File 'lib/adsl/spass/spass_translator.rb', line 194

def is_tuple
  @is_tuple
end

#prev_state ⇒ Object

Returns the value of attribute prev_state.



192
193
194
 
# File 'lib/adsl/spass/spass_translator.rb', line 192

def prev_state
  @prev_state
end

#resolved_as_true ⇒ Object (readonly)

Returns the value of attribute resolved_as_true.



194
195
196
 
# File 'lib/adsl/spass/spass_translator.rb', line 194

def resolved_as_true
  @resolved_as_true
end

#root_context ⇒ Object (readonly)

Returns the value of attribute root_context.



193
194
195
 
# File 'lib/adsl/spass/spass_translator.rb', line 193

def root_context
  @root_context
end

Instance Method Details

#_reserve_names(*names) ⇒ Object 



294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
 
# 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) ⇒ Object

Raises:

  • (ArgumentError) 


258
259
260
261
 
# 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) ⇒ Object 



234
235
236
237
238
239
240
241
242
243
 
# 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) ⇒ Object

Raises:

  • (ArgumentError) 


253
254
255
256
 
# 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) ⇒ Object 



263
264
265
266
267
 
# 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) ⇒ Object 



269
270
271
272
273
 
# 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) ⇒ Object 



223
224
225
226
227
228
229
230
231
232
 
# 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) ⇒ Object 



319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
 
# 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) ⇒ Object 



275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
 
# 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 ⇒ Object 



249
250
251
 
# File 'lib/adsl/spass/spass_translator.rb', line 249

def pop_formula_frame
  @formulae.pop
end

#push_formula_frame ⇒ Object 



245
246
247
 
# File 'lib/adsl/spass/spass_translator.rb', line 245

def push_formula_frame
  @formulae.push []
end

#reserve_names(*names) ⇒ Object 



310
311
312
313
314
315
316
317
 
# 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) ⇒ Object 



351
352
353
 
# 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) ⇒ Object 



346
347
348
349
 
# 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 ⇒ Object 



355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
 
# 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