Skip to content

Commit 579d00c

Browse files
Remove redundant function application ID check
These functions are already handled by the string dependency graph. They should not appear in the add_axioms_for_function_application input.
1 parent e2961b5 commit 579d00c

File tree

1 file changed

+0
-12
lines changed

1 file changed

+0
-12
lines changed

src/solvers/refinement/string_constraint_generator_main.cpp

Lines changed: 0 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -456,10 +456,6 @@ exprt string_constraint_generatort::add_axioms_for_function_application(
456456
res=add_axioms_for_compare_to(expr);
457457
else if(id==ID_cprover_string_literal_func)
458458
res=add_axioms_from_literal(expr);
459-
else if(id==ID_cprover_string_concat_func)
460-
res=add_axioms_for_concat(expr);
461-
else if(id==ID_cprover_string_concat_char_func)
462-
res=add_axioms_for_concat_char(expr);
463459
else if(id==ID_cprover_string_concat_code_point_func)
464460
res=add_axioms_for_concat_code_point(expr);
465461
else if(id==ID_cprover_string_insert_func)
@@ -480,18 +476,10 @@ exprt string_constraint_generatort::add_axioms_for_function_application(
480476
res=add_axioms_for_substring(expr);
481477
else if(id==ID_cprover_string_trim_func)
482478
res=add_axioms_for_trim(expr);
483-
else if(id==ID_cprover_string_to_lower_case_func)
484-
res=add_axioms_for_to_lower_case(expr);
485-
else if(id==ID_cprover_string_to_upper_case_func)
486-
res=add_axioms_for_to_upper_case(expr);
487-
else if(id==ID_cprover_string_char_set_func)
488-
res=add_axioms_for_char_set(expr);
489479
else if(id==ID_cprover_string_empty_string_func)
490480
res=add_axioms_for_empty_string(expr);
491481
else if(id==ID_cprover_string_copy_func)
492482
res=add_axioms_for_copy(expr);
493-
else if(id==ID_cprover_string_of_int_func)
494-
res=add_axioms_from_int(expr);
495483
else if(id==ID_cprover_string_of_int_hex_func)
496484
res=add_axioms_from_int_hex(expr);
497485
else if(id==ID_cprover_string_of_float_func)

0 commit comments

Comments
 (0)