Skip to content

Commit 595e976

Browse files
romainbrenguierromainbrenguier
committed
Remove constraint_generator qualifier in README
These methods are now non-member functions.
1 parent 4b3a914 commit 595e976

File tree

1 file changed

+54
-54
lines changed

1 file changed

+54
-54
lines changed

‎src/solvers/README.md

Lines changed: 54 additions & 54 deletions
Original file line numberDiff line numberDiff line change
@@ -205,95 +205,95 @@ allocates a new string before calling a primitive.
205205
* `cprover_string_associate_length_to_array` : Link the length of the array
206206
with the given integer value.
207207
* `cprover_string_char_at` :
208-
\copybrief string_constraint_generatort::add_axioms_for_char_at(const function_application_exprt &f)
209-
\link string_constraint_generatort::add_axioms_for_char_at(const function_application_exprt &f) More... \endlink
208+
\copybrief add_axioms_for_char_at(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
209+
\link add_axioms_for_char_at(const function_application_exprt &f) More... \endlink
210210
* `cprover_string_length` :
211-
\copybrief string_constraint_generatort::add_axioms_for_length(const function_application_exprt &f)
212-
\link string_constraint_generatort::add_axioms_for_length(const function_application_exprt &f) More... \endlink
211+
\copybrief add_axioms_for_length(symbol_generatort &fresh_symbol,const function_application_exprt &f, array_poolt &array_pool)
212+
\link add_axioms_for_length(const function_application_exprt &f) More... \endlink
213213

214214
\subsection comparisons Comparisons:
215215

216216
* `cprover_string_compare_to` :
217-
\copybrief string_constraint_generatort::add_axioms_for_compare_to(const function_application_exprt &f)
218-
\link string_constraint_generatort::add_axioms_for_compare_to(const function_application_exprt &f) More... \endlink
217+
\copybrief add_axioms_for_compare_to(symbol_generatort &fresh_symbol,const function_application_exprt &f, array_poolt &array_pool)
218+
\link add_axioms_for_compare_to(symbol_generatort &fresh_symbol,const function_application_exprt &f, array_poolt &array_pool) More... \endlink
219219
* `cprover_string_contains` :
220-
\copybrief string_constraint_generatort::add_axioms_for_contains(const function_application_exprt &f)
221-
\link string_constraint_generatort::add_axioms_for_contains(const function_application_exprt &f) More... \endlink
220+
\copybrief add_axioms_for_contains(symbol_generatort &fresh_symbol,const function_application_exprt &f, array_poolt &array_pool)
221+
\link add_axioms_for_contains(symbol_generatort &fresh_symbol,const function_application_exprt &f, array_poolt &array_pool) More... \endlink
222222
* `cprover_string_equals` :
223-
\copybrief string_constraint_generatort::add_axioms_for_equals(const function_application_exprt &f)
224-
\link string_constraint_generatort::add_axioms_for_equals(const function_application_exprt &f) More... \endlink
223+
\copybrief add_axioms_for_equals(symbol_generatort &fresh_symbol,const function_application_exprt &f, array_poolt &array_pool)
224+
\link add_axioms_for_equals(symbol_generatort &fresh_symbol,const function_application_exprt &f, array_poolt &array_pool) More... \endlink
225225
* `cprover_string_equals_ignore_case` :
226-
\copybrief string_constraint_generatort::add_axioms_for_equals_ignore_case(const function_application_exprt &f)
227-
\link string_constraint_generatort::add_axioms_for_equals_ignore_case(const function_application_exprt &f) More... \endlink
226+
\copybrief add_axioms_for_equals_ignore_case(symbol_generatort &fresh_symbol,const function_application_exprt &f, array_poolt &array_pool)
227+
\link add_axioms_for_equals_ignore_case(symbol_generatort &fresh_symbol,const function_application_exprt &f, array_poolt &array_pool) More... \endlink
228228
* `cprover_string_hash_code` :
229-
\copybrief string_constraint_generatort::add_axioms_for_hash_code
230-
\link string_constraint_generatort::add_axioms_for_hash_code More... \endlink
229+
\copybrief add_axioms_for_hash_code
230+
\link add_axioms_for_hash_code More... \endlink
231231
* `cprover_string_is_prefix` :
232-
\copybrief string_constraint_generatort::add_axioms_for_is_prefix
233-
\link string_constraint_generatort::add_axioms_for_is_prefix More... \endlink
232+
\copybrief add_axioms_for_is_prefix
233+
\link add_axioms_for_is_prefix More... \endlink
234234
* `cprover_string_index_of` :
235-
\copybrief string_constraint_generatort::add_axioms_for_index_of(const function_application_exprt &f)
236-
\link string_constraint_generatort::add_axioms_for_index_of(const function_application_exprt &f) More... \endlink
235+
\copybrief add_axioms_for_index_of(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
236+
\link add_axioms_for_index_of(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink
237237
* `cprover_string_last_index_of` :
238-
\copybrief string_constraint_generatort::add_axioms_for_last_index_of(const function_application_exprt &f)
239-
\link string_constraint_generatort::add_axioms_for_last_index_of(const function_application_exprt &f) More... \endlink
238+
\copybrief add_axioms_for_last_index_of(symbol_generatort &fresh_symbol, const function_application_exprt &f)
239+
\link add_axioms_for_last_index_of(symbol_generatort &fresh_symbol, const function_application_exprt &f) More... \endlink
240240

241241
\subsection transformations Transformations:
242242

243243
* `cprover_string_char_set` :
244-
\copybrief string_constraint_generatort::add_axioms_for_char_set(const function_application_exprt &f)
245-
\link string_constraint_generatort::add_axioms_for_char_set(const function_application_exprt &f) More... \endlink
244+
\copybrief add_axioms_for_char_set(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
245+
\link add_axioms_for_char_set(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink
246246
* `cprover_string_concat` :
247-
\copybrief string_constraint_generatort::add_axioms_for_concat(const function_application_exprt &f)
248-
\link string_constraint_generatort::add_axioms_for_concat(const function_application_exprt &f) More... \endlink
247+
\copybrief add_axioms_for_concat(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
248+
\link add_axioms_for_concat(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink
249249
* `cprover_string_delete` :
250-
\copybrief string_constraint_generatort::add_axioms_for_delete(const function_application_exprt &f)
251-
\link string_constraint_generatort::add_axioms_for_delete(const function_application_exprt &f) More... \endlink
250+
\copybrief add_axioms_for_delete(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
251+
\link add_axioms_for_delete(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink
252252
* `cprover_string_insert` :
253-
\copybrief string_constraint_generatort::add_axioms_for_insert(const function_application_exprt &f)
254-
\link string_constraint_generatort::add_axioms_for_insert(const function_application_exprt &f) More... \endlink
253+
\copybrief add_axioms_for_insert(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
254+
\link add_axioms_for_insert(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink
255255
* `cprover_string_replace` :
256-
\copybrief string_constraint_generatort::add_axioms_for_replace(const function_application_exprt &f)
257-
\link string_constraint_generatort::add_axioms_for_replace(const function_application_exprt &f) More... \endlink
256+
\copybrief add_axioms_for_replace(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
257+
\link add_axioms_for_replace(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink
258258
* `cprover_string_set_length` :
259-
\copybrief string_constraint_generatort::add_axioms_for_set_length(const function_application_exprt &f)
260-
\link string_constraint_generatort::add_axioms_for_set_length(const function_application_exprt &f) More... \endlink
259+
\copybrief add_axioms_for_set_length(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
260+
\link add_axioms_for_set_length(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink
261261
* `cprover_string_substring` :
262-
\copybrief string_constraint_generatort::add_axioms_for_substring(const function_application_exprt &f)
263-
\link string_constraint_generatort::add_axioms_for_substring(const function_application_exprt &f) More... \endlink
262+
\copybrief add_axioms_for_substring(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
263+
\link add_axioms_for_substring(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink
264264
* `cprover_string_to_lower_case` :
265-
\copybrief string_constraint_generatort::add_axioms_for_to_lower_case(const function_application_exprt &f)
266-
\link string_constraint_generatort::add_axioms_for_to_lower_case(const function_application_exprt &f) More... \endlink
265+
\copybrief add_axioms_for_to_lower_case(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
266+
\link add_axioms_for_to_lower_case(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink
267267
* `cprover_string_to_upper_case` :
268-
\copybrief string_constraint_generatort::add_axioms_for_to_upper_case(const function_application_exprt &f)
269-
\link string_constraint_generatort::add_axioms_for_to_upper_case(const function_application_exprt &f) More... \endlink
268+
\copybrief add_axioms_for_to_upper_case(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
269+
\link add_axioms_for_to_upper_case(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink
270270
* `cprover_string_trim` :
271-
\copybrief string_constraint_generatort::add_axioms_for_trim(const function_application_exprt &f)
272-
\link string_constraint_generatort::add_axioms_for_trim(const function_application_exprt &f) More... \endlink
271+
\copybrief add_axioms_for_trim(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
272+
\link add_axioms_for_trim(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink
273273

274274
\subsection conversions Conversions:
275275

276276
* `cprover_string_format` :
277-
\copybrief string_constraint_generatort::add_axioms_for_format(const function_application_exprt &f)
278-
\link string_constraint_generatort::add_axioms_for_format(const function_application_exprt &f) More... \endlink
277+
\copybrief add_axioms_for_format(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
278+
\link add_axioms_for_format(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink
279279
* `cprover_string_from_literal` :
280-
\copybrief string_constraint_generatort::add_axioms_from_literal(const function_application_exprt &f)
281-
\link string_constraint_generatort::add_axioms_from_literal(const function_application_exprt &f) More... \endlink
280+
\copybrief add_axioms_from_literal(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
281+
\link add_axioms_from_literal(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink
282282
* `cprover_string_of_int` :
283-
\copybrief string_constraint_generatort::add_axioms_from_int(const function_application_exprt &f)
284-
\link string_constraint_generatort::add_axioms_for_string_of_int(const function_application_exprt &f) More... \endlink
283+
\copybrief add_axioms_from_int(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
284+
\link add_axioms_for_string_of_int(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink
285285
* `cprover_string_of_float` :
286-
\copybrief string_constraint_generatort::add_axioms_for_string_of_float(const function_application_exprt &f)
287-
\link string_constraint_generatort::add_axioms_for_string_of_float(const function_application_exprt &f) More... \endlink
286+
\copybrief add_axioms_for_string_of_float(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
287+
\link add_axioms_for_string_of_float(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink
288288
* `cprover_string_of_float_scientific_notation` :
289-
\copybrief string_constraint_generatort::add_axioms_from_float_scientific_notation(const function_application_exprt &f)
290-
\link string_constraint_generatort::add_axioms_from_float_scientific_notation(const function_application_exprt &f) More... \endlink
289+
\copybrief add_axioms_from_float_scientific_notation(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
290+
\link add_axioms_from_float_scientific_notation(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink
291291
* `cprover_string_of_char` :
292-
\copybrief string_constraint_generatort::add_axioms_from_char(const function_application_exprt &f)
293-
\link string_constraint_generatort::add_axioms_from_char(const function_application_exprt &f) More... \endlink
292+
\copybrief add_axioms_from_char(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
293+
\link add_axioms_from_char(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink
294294
* `cprover_string_parse_int` :
295-
\copybrief string_constraint_generatort::add_axioms_for_parse_int(const function_application_exprt &f)
296-
\link string_constraint_generatort::add_axioms_for_parse_int(const function_application_exprt &f) More... \endlink
295+
\copybrief add_axioms_for_parse_int(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
296+
\link add_axioms_for_parse_int(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink
297297

298298
\subsection deprecated Deprecated primitives:
299299

0 commit comments

Comments
 (0)