Skip to content

Commit a556d3d

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 859d74c commit a556d3d

File tree

1 file changed

+9
-6
lines changed

1 file changed

+9
-6
lines changed

src/solvers/refinement/string_constraint_generator_main.cpp

+9-6
Original file line numberDiff line numberDiff line change
@@ -430,6 +430,14 @@ array_string_exprt array_poolt::of_argument(const exprt &arg)
430430
return find(string_argument.op1(), string_argument.op0());
431431
}
432432

433+
static irep_idt get_function_name(const function_application_exprt &expr)
434+
{
435+
const exprt &name = expr.function();
436+
PRECONDITION(name.id() == ID_symbol);
437+
return is_ssa_expr(name) ? to_ssa_expr(name).get_object_name()
438+
: to_symbol_expr(name).get_identifier();
439+
}
440+
433441
/// strings contained in this call are converted to objects of type
434442
/// `string_exprt`, through adding axioms. Axioms are then added to enforce that
435443
/// the result corresponds to the function application.
@@ -438,12 +446,7 @@ array_string_exprt array_poolt::of_argument(const exprt &arg)
438446
exprt string_constraint_generatort::add_axioms_for_function_application(
439447
const function_application_exprt &expr)
440448
{
441-
const exprt &name=expr.function();
442-
PRECONDITION(name.id()==ID_symbol);
443-
444-
const irep_idt &id=is_ssa_expr(name)?to_ssa_expr(name).get_object_name():
445-
to_symbol_expr(name).get_identifier();
446-
449+
const irep_idt &id = get_function_name(expr);
447450
exprt res;
448451

449452
if(id==ID_cprover_char_literal_func)

0 commit comments

Comments
 (0)