CBMC
edit_distance.cpp
Go to the documentation of this file.
1 
6 #include "edit_distance.h"
7 
9  const std::string &string,
10  std::size_t allowed_errors)
11 {
12  const std::size_t layer_offset = string.size() + 1;
13  for(std::size_t i = 0; i <= allowed_errors; ++i)
14  {
15  final_states.push_back(string.size() + layer_offset * i);
16  }
17  for(std::size_t string_index = 0; string_index < string.size();
18  ++string_index)
19  {
20  for(std::size_t error_layer = 0; error_layer <= allowed_errors;
21  ++error_layer)
22  {
23  // position string_index matches
25  error_layer * layer_offset + string_index,
26  string[string_index],
27  error_layer * layer_offset + string_index + 1);
28  if(error_layer < allowed_errors)
29  {
30  // insertion, swap or deletion
32  error_layer * layer_offset + string_index,
33  (error_layer + 1) * layer_offset + string_index);
35  error_layer * layer_offset + string_index,
36  (error_layer + 1) * layer_offset + string_index + 1);
38  error_layer * layer_offset + string_index,
39  (error_layer + 1) * layer_offset + string_index + 1);
40  }
41  }
42  }
43  for(std::size_t error_layer = 0; error_layer < allowed_errors; ++error_layer)
44  {
45  // arbitrary transitions between error layers
47  error_layer * layer_offset + string.size(),
48  (error_layer + 1) * layer_offset + string.size());
49  }
50 }
51 
52 bool levenshtein_automatont::matches(const std::string &string) const
53 {
54  return get_edit_distance(string).has_value();
55 }
56 
57 std::optional<std::size_t>
58 levenshtein_automatont::get_edit_distance(const std::string &string) const
59 {
60  auto current = nfa.initial_state(0);
61  for(const auto c : string)
62  {
63  current = nfa.next_state(current, c);
64  }
65  for(std::size_t distance = 0; distance < final_states.size(); ++distance)
66  {
67  if(current.contains(final_states[distance]))
68  {
69  return distance;
70  }
71  }
72  return {};
73 }
levenshtein_automatont(const std::string &string, std::size_t allowed_errors=2)
std::optional< std::size_t > get_edit_distance(const std::string &string) const
bool matches(const std::string &string) const
std::vector< state_labelt > final_states
Definition: edit_distance.h:29
statet initial_state(state_labelt initial) const
Definition: nfa.h:72
statet next_state(const statet &current, const T &input) const
Definition: nfa.h:80
void add_arbitrary_transition(state_labelt from, state_labelt to)
Add a transition from "from" to "to" when any input is consumed This is handled a special case so not...
Definition: nfa.h:59
void add_transition(state_labelt from, T when, state_labelt to)
Add a transition from "from" to "to" exactly when "when" is consumed.
Definition: nfa.h:50
void add_epsilon_transition(state_labelt from, state_labelt to)
Add a transition from "from" to "to" that doesn’t consume input.
Definition: nfa.h:66