CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
edit_distance.cpp
Go to the documentation of this file.
1
5
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();
19 {
20 for(std::size_t error_layer = 0; error_layer <= allowed_errors;
22 {
23 // position string_index matches
26 string[string_index],
29 {
30 // insertion, swap or deletion
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
52bool levenshtein_automatont::matches(const std::string &string) const
53{
54 return get_edit_distance(string).has_value();
55}
56
57std::optional<std::size_t>
58levenshtein_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}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
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
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