Skip to content

Commit 05a6b09

Browse files
[constraint-generator] Removing declarations of unimplemented functions
1 parent 302f92e commit 05a6b09

File tree

1 file changed

+0
-13
lines changed

1 file changed

+0
-13
lines changed

src/solvers/refinement/string_constraint_generator.h

-13
Original file line numberDiff line numberDiff line change
@@ -227,13 +227,6 @@ class string_constraint_generatort final
227227
exprt add_axioms_from_bool(const array_string_exprt &res, const exprt &i);
228228
exprt add_axioms_from_char(const function_application_exprt &f);
229229
exprt add_axioms_from_char(const array_string_exprt &res, const exprt &i);
230-
array_string_exprt
231-
add_axioms_from_char_array(const function_application_exprt &f);
232-
array_string_exprt add_axioms_from_char_array(
233-
const exprt &length,
234-
const exprt &data,
235-
const exprt &offset,
236-
const exprt &count);
237230
exprt add_axioms_for_index_of(
238231
const array_string_exprt &str,
239232
const exprt &c,
@@ -306,15 +299,9 @@ class string_constraint_generatort final
306299
const array_string_exprt &expr);
307300
exprt add_axioms_for_trim(const function_application_exprt &f);
308301

309-
// Add axioms corresponding to the String.valueOf([CII) function
310-
// TODO: not working correctly at the moment
311-
array_string_exprt
312-
add_axioms_for_value_of(const function_application_exprt &f);
313-
314302
exprt add_axioms_for_code_point(
315303
const array_string_exprt &res,
316304
const exprt &code_point);
317-
array_string_exprt add_axioms_for_java_char_array(const exprt &char_array);
318305
array_string_exprt add_axioms_for_if(const if_exprt &expr);
319306
exprt add_axioms_for_char_literal(const function_application_exprt &f);
320307

0 commit comments

Comments
 (0)