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