Skip to content

Commit 29bf15d

Browse files
Pull out a get_function_name function
This decrease the size of add_axioms_for_function_application and this new function can be reused.
1 parent 37bb1c8 commit 29bf15d

File tree

1 file changed

+9
-6
lines changed

1 file changed

+9
-6
lines changed

src/solvers/refinement/string_constraint_generator_main.cpp

Lines changed: 9 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -421,6 +421,14 @@ array_string_exprt array_poolt::of_argument(const exprt &arg)
421421
return find(string_argument.op1(), string_argument.op0());
422422
}
423423

424+
static irep_idt get_function_name(const function_application_exprt &expr)
425+
{
426+
const exprt &name = expr.function();
427+
PRECONDITION(name.id() == ID_symbol);
428+
return is_ssa_expr(name) ? to_ssa_expr(name).get_object_name()
429+
: to_symbol_expr(name).get_identifier();
430+
}
431+
424432
/// strings contained in this call are converted to objects of type
425433
/// `string_exprt`, through adding axioms. Axioms are then added to enforce that
426434
/// the result corresponds to the function application.
@@ -429,12 +437,7 @@ array_string_exprt array_poolt::of_argument(const exprt &arg)
429437
exprt string_constraint_generatort::add_axioms_for_function_application(
430438
const function_application_exprt &expr)
431439
{
432-
const exprt &name=expr.function();
433-
PRECONDITION(name.id()==ID_symbol);
434-
435-
const irep_idt &id=is_ssa_expr(name)?to_ssa_expr(name).get_object_name():
436-
to_symbol_expr(name).get_identifier();
437-
440+
const irep_idt &id = get_function_name(expr);
438441
exprt res;
439442

440443
if(id==ID_cprover_char_literal_func)

0 commit comments

Comments
 (0)