|
13 | 13 |
|
14 | 14 | #include <solvers/refinement/string_constraint_generator.h>
|
15 | 15 |
|
16 |
| -/// Add axioms to say that the returned string expression is equal to the |
| 16 | +/// Add axioms enforcing that the returned string expression is equal to the |
17 | 17 | /// concatenation of s1 with the substring of s2 starting at index start_index
|
18 | 18 | /// and ending at index end_index.
|
19 | 19 | ///
|
@@ -77,15 +77,15 @@ string_exprt string_constraint_generatort::add_axioms_for_concat(
|
77 | 77 | return add_axioms_for_concat_substr(s1, s2, index_zero, s2.length());
|
78 | 78 | }
|
79 | 79 |
|
80 |
| -/// Add axioms to say that the returned string expression is equal to the |
| 80 | +/// Add axioms enforcing that the returned string expression is equal to the |
81 | 81 | /// concatenation of the two string arguments of the function application.
|
82 | 82 | ///
|
83 | 83 | /// In case 4 arguments instead of 2 are given the last two arguments are
|
84 | 84 | /// intepreted as a start index and last index from which we extract a substring
|
85 | 85 | /// of the second argument: this is similar to the Java
|
86 | 86 | /// StringBuilder.append(CharSequence s, int start, int end) method.
|
87 | 87 | ///
|
88 |
| -/// \param f: function application with two arguments which are strings |
| 88 | +/// \param f: function application with two string arguments |
89 | 89 | /// \return a new string expression
|
90 | 90 | string_exprt string_constraint_generatort::add_axioms_for_concat(
|
91 | 91 | const function_application_exprt &f)
|
@@ -151,12 +151,11 @@ string_exprt string_constraint_generatort::add_axioms_for_concat_char(
|
151 | 151 | return add_axioms_for_concat_char(s1, args(f, 2)[1]);
|
152 | 152 | }
|
153 | 153 |
|
154 |
| -/// Add axioms corresponding adding the character char at the end of |
| 154 | +/// Add axioms corresponding to adding the character char at the end of |
155 | 155 | /// string_expr.
|
156 | 156 | /// \param string_expr: a string expression
|
157 | 157 | /// \param char' a character expression
|
158 | 158 | /// \return a new string expression
|
159 |
| - |
160 | 159 | string_exprt string_constraint_generatort::add_axioms_for_concat_char(
|
161 | 160 | const string_exprt &string_expr, const exprt &char_expr)
|
162 | 161 | {
|
|
0 commit comments