Class: CoreEnumerationAlgo

Inherits:

Object

• Object
• CoreEnumerationAlgo

Defined in:

lib/mbt-gen.rb

Class Method Summary

• .parse_assignment(str) ⇒ Object
• .parse_continuation_point(line) ⇒ Object
• .parse_new_assignment(str) ⇒ Object
• .parse_state(state_str) ⇒ Object

Instance Method Summary

• #determine_progress(state, vars) ⇒ Object

  NOTE: can only be called when all key-fields are finite-state.

• #display_combination_space(assignment, vars, switched, blocked) ⇒ Object

  TODO: logging.

• #enumerate(progress, switched, vars, assignment, message, key, output_dir, config, options, state = [nil] * vars.size()) ⇒ Object

  core algo.

• #enumerate_blocking_clause(var_xpath, var_def, blocked) ⇒ Object

  prevent the var from taking values that already have been enumerated exhaustively.

• #enumerate_fixing_clause(assignment, vars, switched) ⇒ Object

  fix values of all variables left from switched.

• #generate_doc_return_key_values(progress, message, key, output_filename, config, options) ⇒ Object
• #generate_docs_for_key(message, key, output_dir, config, options) ⇒ Object
• #generate_sparse_doc(progress, message, key, config, options, code, output_doc_filename) ⇒ Object
• #initialize ⇒ CoreEnumerationAlgo constructor

  A new instance of CoreEnumerationAlgo.

• #is_final_state(state, new_assignment, key_fields_list) ⇒ Object

  NOTE: can only be called when all key-fields are finite-state.

• #keys_are_finite_state(list) ⇒ Object
• #log_filename_for_output_filename(output_filename) ⇒ Object
• #num_combinations(key_def) ⇒ Object
• #store_continuation_point(doc_number, state, assignment, new_assignment, filename) ⇒ Object
• #summarize_blocking_clause(var_xpath, blocked) ⇒ Object
• #summarize_fixing_clause(assignment, vars, switched) ⇒ Object
• #value_of_type(value, type) ⇒ Object

Constructor Details

#initialize ⇒ CoreEnumerationAlgo

Returns a new instance of CoreEnumerationAlgo.

# File 'lib/mbt-gen.rb', line 1148

def initialize()
  @num_tries = 0
  @num_docs = 0
  @on_new_doc = nil
  @on_unsat = nil
end

Class Method Details

.parse_assignment(str) ⇒ Object

# File 'lib/mbt-gen.rb', line 1295

def self.parse_assignment(str)
  unless str =~ /assignment\((.*)\)/
    return nil
  end
  split = $1.split(",")
  result = {}
  split.each do |e|
    s2 = e.split(":")
    key = s2[0]
    value = s2[1]
    if value == "nil" then
      result[key] = nil
    elsif value == "true" then
      result[key] = true
    elsif value == "false" then
      result[key] = false
    elsif value =~ /\"(.*)\"/
      result[key] = $1
    end
  end
  result
end

.parse_continuation_point(line) ⇒ Object

# File 'lib/mbt-gen.rb', line 1341

def self.parse_continuation_point(line)
  split = line.split(";")
  doc_number = Integer(split[0])
  num_docs = Integer(split[1])
  state = CoreEnumerationAlgo.parse_state(split[2])
  assignment = CoreEnumerationAlgo.parse_assignment(split[3])
  new_assignment = CoreEnumerationAlgo.parse_assignment(split[4])
  return [doc_number, num_docs, state, assignment, new_assignment]
end

.parse_new_assignment(str) ⇒ Object

# File 'lib/mbt-gen.rb', line 1318

def self.parse_new_assignment(str)
  unless str =~ /new_assignment\((.*)\)/
    return nil
  end
  split = $1.split(",")
  result = {}
  split.each do |e|
    s2 = e.split(":")
    key = s2[0]
    value = s2[1]
    if value == "nil" then
      result[key] = nil
    elsif value == "true" then
      result[key] = true
    elsif value == "false" then
      result[key] = false
    elsif value =~ /\"(.*)\"/
      result[key] = $1
    end
  end
  result
end

.parse_state(state_str) ⇒ Object

# File 'lib/mbt-gen.rb', line 1271

def self.parse_state(state_str)
  unless state_str =~ /state\((.*)\)/
    return nil
  end
  split = $1.split("#")
  split.map do |e|
    if e == "nil" then
      nil
    elsif e =~ /\[(.*)\]/ then
      $1.split(",").map do |i|
        if i.strip == "nil" then
          nil
        elsif i.strip == "true" then
          true
        elsif i.strip == "false" then
          false
        elsif i.strip =~ /\"(.*)\"/ then
          $1
        end
      end
    end
  end
end

Instance Method Details

#determine_progress(state, vars) ⇒ Object

NOTE: can only be called when all key-fields are finite-state

# File 'lib/mbt-gen.rb', line 1418

def determine_progress(state, vars)
  combinations_per_value = [nil] * vars.size()
  comb = 1
  vars.size().times.to_a.reverse_each do |i|
    combinations_per_value[i] = comb
    comb = values_for_key_field(vars[i][1]).size() * comb
  end

  blocked_combinations = 0
  state.size().times do |i|
    if state[i] then
      blocked_combinations += state[i].size() * combinations_per_value[i]
    end
  end
  blocked_combinations
end

#display_combination_space(assignment, vars, switched, blocked) ⇒ Object

TODO: logging

# File 'lib/mbt-gen.rb', line 1353

def display_combination_space(assignment, vars, switched, blocked)
  # enumerate_fixing_clause(assignment, vars, switched) + enumerate_blocking_clause(vars[switched][0], vars[switched][1], blocked)

  # => all vars left of switched are fixed to their assigned values (when the value is nil, then they are empty)
  # => the switched var is prevented to have any of the blocked values
  res = switched.times.to_a.map do |index|
    var_xpath = vars[index][0]
    "#{var_xpath}=#{assignment[var_xpath].inspect}"
  end + ["#{vars[switched][0]}|#{blocked.map{|v| v.inspect}.join(",")}"]
  "{#{res.join(", ")}}"
end

#enumerate(progress, switched, vars, assignment, message, key, output_dir, config, options, state = [nil] * vars.size()) ⇒ Object

core algo

# File 'lib/mbt-gen.rb', line 1366

def enumerate(progress, switched, vars, assignment, message, key, output_dir, config, options, state = [nil] * vars.size())
  enumerate(progress, switched+1, vars, assignment, message, key, output_dir, config, options, state) if switched < vars.size()-1
  is_finite_state = keys_are_finite_state(vars)
  if state[switched] == nil then
    blocked = [assignment[vars[switched][0]]]
    state[switched] = blocked
  else
    blocked = state[switched] + [assignment[vars[switched][0]]]
    state[switched] = blocked
  end
  found = true
  while found do
    found = false
    # - fix all vars left of switched to their values in assignment
    # - block switched from obtaining the values in blocked
    # progress.print_line "DEBUG: #{summarize_fixing_clause(assignment, vars, switched)}, #{summarize_blocking_clause(vars[switched][0], blocked)}"
    clauses = enumerate_fixing_clause(assignment, vars, switched) + enumerate_blocking_clause(vars[switched][0], vars[switched][1], blocked)
    output_doc_filename = prepare_output_doc_filename(@num_tries, output_dir)
    new_assignment = generate_sparse_doc(progress, message, key, config, options, clauses, output_doc_filename)
    generated_doc_number = @num_tries
    store_continuation_point(generated_doc_number, state, assignment, new_assignment, "#{output_dir}/#{CONTINUATION_FILE}")
    if is_finite_state then
      progress.report_progress(determine_progress(state, vars))
    else
      progress.report_progress(nil)
    end
    @num_tries += 1
    if new_assignment then # sat
      @num_docs += 1
      @on_new_doc.call(generated_doc_number, output_doc_filename, new_assignment) if @on_new_doc
      if switched < vars.size()-1 then
        enumerate(progress, switched+1, vars, new_assignment, message, key, output_dir, config, options, state)
      end
      blocked << new_assignment[vars[switched][0]]
      state[switched] = blocked
      found = true
    else # unsat
      @on_unsat.call(generated_doc_number, log_filename_for_output_filename(output_doc_filename), display_combination_space(assignment, vars, switched, blocked)) if @on_unsat
      found = false
    end
  end
  state[switched] = nil
end

#enumerate_blocking_clause(var_xpath, var_def, blocked) ⇒ Object

prevent the var from taking values that already have been enumerated exhaustively

# File 'lib/mbt-gen.rb', line 1192

def enumerate_blocking_clause(var_xpath, var_def, blocked)
  clauses = []
  num = 0
  if var_def[:type] == :field then
    blocked.each do |value|
      if value == nil then
        clauses << "(assert (! (not (= #{filled_var_for_field(var_xpath)} false)) :named blocking_clause_#{num}))"
      else
        clauses << "(assert (! (not (and (= #{filled_var_for_field(var_xpath)} true) (= #{value_var_for_field(var_xpath)} #{value_of_type(value, var_def[:datatype])}))) :named blocking_clause_#{num}))"
      end
      num += 1
    end
  elsif var_def[:type] == :structure then
    blocked.each do |value|
      clauses << "(assert (! (not (= #{exists_var_for_structure(var_xpath)} #{value.inspect})) :named blocking_clause_#{num}))"
      num += 1
    end
  end
  "; blocking clauses:\n#{clauses.join("\n")}" 
end

#enumerate_fixing_clause(assignment, vars, switched) ⇒ Object

fix values of all variables left from switched

# File 'lib/mbt-gen.rb', line 1157

def enumerate_fixing_clause(assignment, vars, switched)
  clauses = []
  switched.times do |index|
    var_xpath = vars[index][0]
    var_def = vars[index][1]
    if var_def[:type] == :field then
      if assignment[var_xpath] == nil then
        clauses << "(assert (! (= #{filled_var_for_field(var_xpath)} false) :named fixing_clause_#{index}))"
      else
        clauses << "(assert (! (and (= #{filled_var_for_field(var_xpath)} true) (= #{value_var_for_field(var_xpath)} #{value_of_type(assignment[var_xpath], var_def[:datatype])})) :named fixing_clause_#{index}))"
      end
    elsif var_def[:type] == :structure then
      clauses << "(assert (! (= #{exists_var_for_structure(var_xpath)} #{assignment[var_xpath].inspect}) :named fixing_clause_#{index}))"
    end
  end
  "; fixing clauses:\n#{clauses.join("\n")}" 
end

#generate_doc_return_key_values(progress, message, key, output_filename, config, options) ⇒ Object

# File 'lib/mbt-gen.rb', line 1229

def generate_doc_return_key_values(progress, message, key, output_filename, config, options)
  log = options[:log] || nil
  log.puts "generating doc #{output_filename}" if log
  options[:solverLog] = log_filename_for_output_filename(output_filename)

  key_fields = collect_key_fields(key, message)

  z3path = config[:z3path] || DEFAULT_Z3_PATH
  z3 = Z3Solver.new(progress, z3path)
  begin
    model = z3.query_model(progress, options) do |solver|
      solver.to_solver(progress, "(set-option :produce-unsat-cores true) ; enable generation of unsat cores")
      solver.to_solver(progress, "")
      log.puts "translating structure" if log
      translate_structure_to_SMTLIB(progress, solver, message, :options => options, :config => config)
      solver.to_solver(progress, "")
    end
  ensure
    z3.close()
  end

  if model then
    result_doc = build_document_from_model(progress, message, model)
    dir = File.dirname(output_filename)
    FileUtils.mkdir_p(dir) unless Dir.exist?(dir)
    File.open(output_filename, "w") do |f|
      f.puts result_doc.to_xml(:save_with => Nokogiri::XML::Node::SaveOptions::AS_XML)
    end
    progress.print_line "DONE. Generated XML was written to #{output_filename}, SMTLIB log was written to #{options[:solverLog]}"
    return extract_key_field_values_from_model(key_fields, model)
  else
    progress.print_line "FAILED. No XML document was generated. For more details, please see the SMTLIB log in #{options[:solverLog]}"
    return nil
  end
end

#generate_docs_for_key(message, key, output_dir, config, options) ⇒ Object

# File 'lib/mbt-gen.rb', line 1469

def generate_docs_for_key(message, key, output_dir, config, options)

  number_of_combinations = calc_combinations(message, key)
  if number_of_combinations.is_a?(String) then
    progress = ProgressBar.new(100000000000000)
  else
    progress = ProgressBar.new(number_of_combinations)
  end
  begin
  ensure
  end
  progress.report_progress(0.0)
  progress.print_line "generating sparse documents efficiently..."
  progress.print_line "there is a theoretical maximum of #{number_of_combinations} combinations."
  progress.print_line "Note, however, that we are generating only those documents that are valid, which are usually much less."

  progress.print_line "preparing output dir #{output_dir}..."
  if options[:continue] then
    unless Dir.exist?(output_dir) then
      raise FatalError.new("FATAL: directory #{output_dir} not found. There seems to be nothing to continue from...")
    end
    log_mode = "a"
  else
    unless Dir.exist?(output_dir) then
      FileUtils.mkdir_p(output_dir)
    end
    log_mode = "w"
  end
  log_filename = "#{output_dir}/#{COMBINATION_LOG}"

  key_fields = collect_key_fields(key, message)
  key_fields_list = key_fields.each_pair.to_a
  key_fields_list.sort! {|a,b| num_combinations(b[1]) <=> num_combinations(a[1]) }

  if options[:continue] then
    stored_key_fields_str = File.read("#{output_dir}/#{VARS_LOG}")
    unless key_fields_list.to_yaml == stored_key_fields_str then
      raise FatalError.new("vars are differing! please specify the same key in order to use -continue!")
    end
    progress.print_line "continuing enumerating documents for key #{key}!"
  else
    # store vars
    File.open("#{output_dir}/#{VARS_LOG}", "w") do |f|
      f.puts(key_fields_list.to_yaml)
    end
  end

  #progress.print_line "DEBUG: key_fields_list=#{key_fields_list.inspect}"

  cont_filename = "#{output_dir}/#{CONTINUATION_FILE}"
  if options[:continue] then
    unless File.exist?(cont_filename) then
      raise FatalError.new("FATAL: file #{cont_filename} not found. There seems to be no continuation point to continue from...")
    end
    doc_number, num_docs, state, assignment, new_assignment = CoreEnumerationAlgo.parse_continuation_point(File.read(cont_filename).chomp)
    if is_final_state(state, new_assignment, key_fields_list) then
      progress.report_progress(number_of_combinations)
      raise FatalError.new("FATAL: The enumeration is finished. There is nothing left to do. Resuming the enumeration hence does not make sense.")
    end
    progress.print_line "RESUMING enumeration from the following continuation point:"
    progress.print_line "|doc_number=#{doc_number}"
    progress.print_line "|num_docs=#{num_docs}"
    progress.print_line "|state=#{state.inspect}"
    progress.print_line "|assignment=#{assignment.inspect}"
    progress.print_line "|new_assignment=#{new_assignment.inspect}"
    if keys_are_finite_state(key_fields_list) then
      progress.report_progress(determine_progress(state, key_fields_list))
    else
      progress.report_progress(nil)
    end

    if new_assignment && !new_assignment.empty? then
      assignment = new_assignment
    end

    # restore state at continuation point
    @num_tries = doc_number+1 # we do not want to overwrite the last document written before the STOP
    number_of_combinations += 1 # account for this in the safety mechanism
    @num_docs = num_docs
    doc_counter = 0
    File.open(log_filename, log_mode) do |log|

      @on_new_doc = Proc.new { |num_doc, doc_filename, combination|
        # combination logging
        log.puts "#{doc_filename} <- {#{combination.map{|k,v| "#{k}: #{v.inspect}"}.join(", ")}}"

        doc_counter += 1
        if options[:max_num_docs] && doc_counter >= options[:max_num_docs] then
          raise NormalProgramTermination.new("-max-num-docs exceeded. Stopping!")
        end

        # safety mechanism
        if @num_docs > number_of_combinations then
          raise RuntimeError.new("This should never happen! Number of combinations exceeded. #{@num_docs} documents generated, but there are only #{number_of_combinations} possible combinations of the key vars.")
        end
      }
      @on_unsat = Proc.new { |num_doc, log_filename, combination_str|
            log.puts "CONTRADICTION (see: #{log_filename}) <- #{combination_str}"
            progress.print_line "doc#{num_doc} NOT generated"
            progress.print_line "No more valid combinations of the free vars could be found. -> Switching"
      }

      # core algo - resume from state
      enumerate(progress, 0, key_fields_list, assignment, message, key, output_dir, config, options, state)
    end
  else
    # init safety mechanism
    @num_tries = 0
    @num_docs = 0
    doc_counter = 0
    # first try - a freely generated document
    File.open(log_filename, log_mode) do |log|
      output_doc_filename = prepare_output_doc_filename(@num_tries, output_dir)
      key_values = generate_doc_return_key_values(progress, message, key, output_doc_filename, config, options)
      log.puts "#{output_doc_filename} <- {#{key_values.map{|k,v| "#{k}: #{v.inspect}"}.join(", ")}}"
      doc_counter += 1
      @num_tries += 1
      @on_new_doc = Proc.new { |num_doc, doc_filename, combination|
        # combination logging
        log.puts "#{doc_filename} <- {#{combination.map{|k,v| "#{k}: #{v.inspect}"}.join(", ")}}"

        doc_counter += 1
        if options[:max_num_docs] && doc_counter >= options[:max_num_docs] then
          raise NormalProgramTermination.new("-max-num-docs exceeded. Stopping!")
        end

        # safety mechanism
        unless number_of_combinations.is_a?(String) then
          if @num_docs > number_of_combinations then
            raise RuntimeError.new("This should never happen! Number of combinations exceeded. #{@num_docs} documents generated, but there are only #{number_of_combinations} possible combinations of the key vars.")
          end
        end
      }
      @on_unsat = Proc.new { |num_doc, log_filename, combination_str|
            log.puts "CONTRADICTION (see: #{log_filename}) <- #{combination_str}"
            progress.print_line "doc#{num_doc} NOT generated"
            progress.print_line "No more valid combinations of the free vars could be found. -> Switching"
      }

      # core algo - start enumeration
      enumerate(progress, 0, key_fields_list, key_values, message, key, output_dir, config, options)
    end
    
    progress.print_line "No more valid documents could be found. -> Exiting"
    progress.report_progress(number_of_combinations)
  end
end

#generate_sparse_doc(progress, message, key, config, options, code, output_doc_filename) ⇒ Object

# File 'lib/mbt-gen.rb', line 1217

def generate_sparse_doc(progress, message, key, config, options, code, output_doc_filename)
  additional_options = {}
  if code then
      additional_options = { :add_SMTLIB => code }
  end
  return generate_doc_return_key_values(progress, message, key, output_doc_filename, config, options.merge(additional_options))
end

#is_final_state(state, new_assignment, key_fields_list) ⇒ Object

NOTE: can only be called when all key-fields are finite-state

# File 'lib/mbt-gen.rb', line 1411

def is_final_state(state, new_assignment, key_fields_list)
  return state[1,state.size()] == [nil] * (state.size()-1) &&
     state[0].to_set == values_for_key_field(key_fields_list[0][1]).to_set &&
     new_assignment.empty?
end

#keys_are_finite_state(list) ⇒ Object

# File 'lib/mbt-gen.rb', line 1453

def keys_are_finite_state(list)
  list.each do |field|
    name = field[0]
    if field[1][:type] == :field then
      if field[1][:datatype] == :enum then
        # enums are finite-state
      elsif field[1][:datatype] == :int and field[1].has_key?(:min) and field[1].has_key?(:max) and field[1][:min] <= field[1][:max] then
        # ints are finite-state when both bounds are given and :min <= :max
      else
        return false
      end
    end
  end
  return true
end

#log_filename_for_output_filename(output_filename) ⇒ Object

# File 'lib/mbt-gen.rb', line 1225

def log_filename_for_output_filename(output_filename)
  "#{output_filename}.smt2"
end

#num_combinations(key_def) ⇒ Object

# File 'lib/mbt-gen.rb', line 1435

def num_combinations(key_def)
  if key_def[:type] == :field then
    if key_def[:datatype] == :enum then
      key_def[:values].size() + (key_def[:optional] ? 1 : 0)
    elsif key_def[:datatype] == :int then
      if key_def.has_key?(:min) and key_def.has_key?(:max) and key_def[:min] <= key_def[:max] then
        1 + key_def[:max] - key_def[:min] + (key_def[:optional] ? 1 : 0)
      else
        nil
      end
    else
      nil
    end
  elsif key_def[:type] == :structure then
    2
  end
end

#store_continuation_point(doc_number, state, assignment, new_assignment, filename) ⇒ Object

# File 'lib/mbt-gen.rb', line 1265

def store_continuation_point(doc_number, state, assignment, new_assignment, filename)
  File.open(filename, "w") do |f|
    f.puts("#{doc_number};#{@num_docs};state(#{state.map{|s| if s then "[#{s.map{|v| v.inspect}.join(",")}]" else "nil" end}.join("#")});assignment(#{assignment.to_a.map{|k,v| "#{k}:#{v.inspect}"}.join(",")});new_assignment(#{new_assignment.to_a.map{|k,v| "#{k}:#{v.inspect}"}.join(",")})")
  end
end

#summarize_blocking_clause(var_xpath, blocked) ⇒ Object

# File 'lib/mbt-gen.rb', line 1213

def summarize_blocking_clause(var_xpath, blocked)
  "blocked(#{var_xpath})=[#{blocked.map{|v| v.inspect}.join(", ")}]"
end

#summarize_fixing_clause(assignment, vars, switched) ⇒ Object

# File 'lib/mbt-gen.rb', line 1175

def summarize_fixing_clause(assignment, vars, switched)
  fixed = switched.times.to_a.map do |index|
    var_xpath = vars[index][0]
    "#{var_xpath}=#{assignment[var_xpath].inspect}"
  end
  "fixed(#{fixed.join(", ")})"
end

#value_of_type(value, type) ⇒ Object

# File 'lib/mbt-gen.rb', line 1183

def value_of_type(value, type)
  if type == :string or type == :enum then
    "\"#{value}\""
  elsif type == :int then
    value.to_s
  end
end