Class: Ibex::LALR::Counterexample

Inherits:
Object
  • Object
show all
Defined in:
lib/ibex/lalr/counterexample.rb,
sig/ibex/lalr/counterexample.rbs

Overview

Produces shortest-path conflict witnesses using Automaton IR only.

Constant Summary collapse

DEFAULT_MAX_TOKENS =

Signature:

  • Integer

Returns:

  • (Integer) 
ConflictSearch::DEFAULT_MAX_TOKENS
DEFAULT_MAX_CONFIGURATIONS =

Signature:

  • Integer

Returns:

  • (Integer) 
ConflictSearch::DEFAULT_MAX_CONFIGURATIONS

Instance Method Summary collapse

Constructor Details

#initialize(automaton, max_tokens: DEFAULT_MAX_TOKENS, max_configurations: DEFAULT_MAX_CONFIGURATIONS) ⇒ Counterexample

Returns a new instance of Counterexample.

RBS:

  • (IR::Automaton automaton, ?max_tokens: Integer, ?max_configurations: Integer) -> void

Parameters:

  • automaton (IR::Automaton)
  • max_tokens: (Integer) (defaults to: DEFAULT_MAX_TOKENS)
  • max_configurations: (Integer) (defaults to: DEFAULT_MAX_CONFIGURATIONS) 


11
12
13
14
15
16
17
18
 
# File 'lib/ibex/lalr/counterexample.rb', line 11

def initialize(automaton, max_tokens: DEFAULT_MAX_TOKENS, max_configurations: DEFAULT_MAX_CONFIGURATIONS)
  ConflictSearchLimits.validate!(max_tokens: max_tokens, max_configurations: max_configurations)
  @automaton = automaton
  @grammar = automaton.grammar
  @max_tokens = max_tokens
  @max_configurations = max_configurations
  @shortest_yields = compute_shortest_yields
end

Instance Method Details

#all ⇒ Array[IR::counterexample]

RBS:

  • () -> Array[IR::counterexample]

Returns:

  • (Array[IR::counterexample]) 


21
22
23
24
25
 
# File 'lib/ibex/lalr/counterexample.rb', line 21

def all
  @automaton.states.flat_map do |state|
    state.conflicts.map { |conflict| build_example(state, conflict) }
  end
end

#better_yield?(candidate, current) ⇒ Boolean

RBS:

  • (Array[Integer] candidate, Array[Integer]? current) -> bool

Parameters:

  • candidate (Array[Integer])
  • current (Array[Integer], nil)

Returns:

  • (Boolean) 


107
108
109
110
111
112
113
 
# File 'lib/ibex/lalr/counterexample.rb', line 107

def better_yield?(candidate, current)
  return true unless current
  return candidate.length < current.length if candidate.length != current.length

  comparison = names(candidate) <=> names(current)
  comparison ? comparison.negative? : false
end

#build_example(state, conflict) ⇒ IR::counterexample

RBS:

  • (IR::AutomatonState state, IR::conflict conflict) -> IR::counterexample

Parameters:

Returns:

  • (IR::counterexample) 


43
44
45
46
47
48
49
50
 
# File 'lib/ibex/lalr/counterexample.rb', line 43

def build_example(state, conflict)
  unifying = ConflictSearch.new(
    @automaton, state, conflict, max_tokens: @max_tokens, max_configurations: @max_configurations
  ).call
  return unifying_example(state, conflict, unifying) if unifying

  reachability_example(state, conflict)
end

#compute_shortest_yields ⇒ Hash[Integer, Array[Integer]]

RBS:

  • () -> Hash[Integer, Array[Integer]]

Returns:

  • (Hash[Integer, Array[Integer]]) 


90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
 
# File 'lib/ibex/lalr/counterexample.rb', line 90

def compute_shortest_yields
  yields = @grammar.terminals.to_h { |terminal| [terminal.id, [terminal.id]] }
  loop do
    changed = false
    @grammar.productions.each do |production|
      candidate = production.rhs.flat_map { |id| yields[id] || [] }
      next unless production.rhs.all? { |id| yields.key?(id) }
      next unless better_yield?(candidate, yields[production.lhs])

      yields[production.lhs] = candidate
      changed = true
    end
    return yields unless changed
  end
end

#for_conflict(state_id, conflict_index) ⇒ IR::counterexample

RBS:

  • (Integer state_id, Integer conflict_index) -> IR::counterexample

Parameters:

  • state_id (Integer)
  • conflict_index (Integer)

Returns:

  • (IR::counterexample) 


28
29
30
31
32
33
34
35
36
37
38
 
# File 'lib/ibex/lalr/counterexample.rb', line 28

def for_conflict(state_id, conflict_index)
  state = @automaton.states.find { |candidate| candidate.id == state_id }
  raise ArgumentError, "unknown automaton state #{state_id}" unless state

  unless conflict_index.is_a?(Integer) && conflict_index >= 0 && conflict_index < state.conflicts.length
    raise ArgumentError, "conflict index #{conflict_index.inspect} is invalid for automaton state #{state_id}"
  end

  conflict = state.conflicts.fetch(conflict_index)
  build_example(state, conflict)
end

#interpretations(conflict) ⇒ Array[IR::interpretation]

RBS:

  • (IR::conflict conflict) -> Array[IR::interpretation]

Parameters:

  • conflict (IR::conflict)

Returns:

  • (Array[IR::interpretation]) 


116
117
118
119
120
121
122
123
124
125
126
 
# File 'lib/ibex/lalr/counterexample.rb', line 116

def interpretations(conflict)
  case conflict[:type]
  when :shift_reduce
    shift_reduce = conflict #: IR::shift_reduce_conflict
    [shift_interpretation(shift_reduce), reduce_interpretation(shift_reduce[:reduce])]
  when :reduce_reduce
    reduce_reduce = conflict #: IR::reduce_reduce_conflict
    reduce_reduce[:reductions].map { |production_id| reduce_interpretation(production_id) }
  else []
  end
end

#names(symbol_ids) ⇒ Array[String]

RBS:

  • (Array[Integer] symbol_ids) -> Array[String]

Parameters:

  • symbol_ids (Array[Integer])

Returns:

  • (Array[String]) 


142
143
144
 
# File 'lib/ibex/lalr/counterexample.rb', line 142

def names(symbol_ids)
  symbol_ids.map { |id| symbol_name(id) }
end

#reachability_example(state, conflict) ⇒ IR::counterexample

RBS:

  • (IR::AutomatonState state, IR::conflict conflict) -> IR::counterexample

Parameters:

Returns:

  • (IR::counterexample) 


60
61
62
63
64
65
66
67
 
# File 'lib/ibex/lalr/counterexample.rb', line 60

def reachability_example(state, conflict)
  path = shortest_state_path(state.id, conflict)
  lookahead = @grammar.symbol(conflict[:symbol])
  terminal_ids = path.flat_map { |symbol_id| @shortest_yields[symbol_id] || [] }
  terminal_ids << lookahead.id if lookahead
  { state: state.id, type: conflict[:type], symbol_path: names(path), sentence: names(terminal_ids),
    lookahead_index: terminal_ids.length - 1, unifying: false, interpretations: interpretations(conflict) }
end

#reduce_interpretation(production_id) ⇒ IR::interpretation

RBS:

  • (Integer production_id) -> IR::interpretation

Parameters:

  • production_id (Integer)

Returns:

  • (IR::interpretation) 


134
135
136
137
138
139
 
# File 'lib/ibex/lalr/counterexample.rb', line 134

def reduce_interpretation(production_id)
  production = @grammar.productions.fetch(production_id)
  lhs = symbol_name(production.lhs)
  rhs = names(production.rhs)
  { kind: :reduce, production: production_id, tree: { symbol: lhs, children: rhs } }
end

#shift_interpretation(conflict) ⇒ IR::interpretation

RBS:

  • (IR::shift_reduce_conflict conflict) -> IR::interpretation

Parameters:

  • conflict (IR::shift_reduce_conflict)

Returns:

  • (IR::interpretation) 


129
130
131
 
# File 'lib/ibex/lalr/counterexample.rb', line 129

def shift_interpretation(conflict)
  { kind: :shift, state: conflict[:shift_to], tree: { token: conflict[:symbol] } }
end

#shortest_state_path(target, conflict) ⇒ Array[Integer]

RBS:

  • (Integer target, IR::conflict conflict) -> Array[Integer]

Parameters:

  • target (Integer)
  • conflict (IR::conflict)

Returns:

  • (Array[Integer]) 


70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
 
# File 'lib/ibex/lalr/counterexample.rb', line 70

def shortest_state_path(target, conflict)
  entry = conflict[:entries]&.first || @grammar.start
  initial = @automaton.entry_states.fetch(entry)
  queue = [[initial, Array.new(0)]] #: Array[[Integer, Array[Integer]]]
  visited = { initial => true }
  until queue.empty?
    state_id, path = queue.shift
    return path if state_id == target

    @automaton.states.fetch(state_id).transitions.sort.each do |symbol_id, next_state|
      next if visited[next_state]

      visited[next_state] = true
      queue << [next_state, path + [symbol_id]]
    end
  end
  []
end

#symbol_name(id) ⇒ String

RBS:

  • (Integer id) -> String

Parameters:

  • id (Integer)

Returns:

  • (String) 


147
148
149
150
 
# File 'lib/ibex/lalr/counterexample.rb', line 147

def symbol_name(id)
  symbol = @grammar.symbol_by_id(id) || raise(Ibex::Error, "missing grammar symbol id #{id}")
  symbol.name
end

#unifying_example(state, conflict, result) ⇒ IR::counterexample

RBS:

  • (IR::AutomatonState state, IR::conflict conflict, Hash[Symbol, untyped] result) -> IR::counterexample

Parameters:

Returns:

  • (IR::counterexample) 


53
54
55
56
57
 
# File 'lib/ibex/lalr/counterexample.rb', line 53

def unifying_example(state, conflict, result)
  { state: state.id, type: conflict[:type], symbol_path: Array.new(0),
    sentence: names(result[:sentence_ids]), lookahead_index: result[:lookahead_index], unifying: true,
    interpretations: result[:interpretations] }
end