Skip to content

Commit 985b7cd

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 a0cb233 commit 985b7cd

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
@@ -424,6 +424,14 @@ array_string_exprt array_poolt::of_argument(const exprt &arg)
424424
return find(string_argument.op1(), string_argument.op0());
425425
}
426426

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

443446
if(id==ID_cprover_char_literal_func)

0 commit comments

Comments
 (0)