From a7c6dd609c0306393f9f038417a6f864583f79bb Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 21 Mar 2017 16:37:03 +0000 Subject: [PATCH] [string-refine] Adapt add_axioms_for_insert for 5 arguments #110 --- .../string_constraint_generator_insert.cpp | 25 +++++++++++++++---- 1 file changed, 20 insertions(+), 5 deletions(-) diff --git a/src/solvers/refinement/string_constraint_generator_insert.cpp b/src/solvers/refinement/string_constraint_generator_insert.cpp index cd5f4376a93..7a63279699e 100644 --- a/src/solvers/refinement/string_constraint_generator_insert.cpp +++ b/src/solvers/refinement/string_constraint_generator_insert.cpp @@ -40,17 +40,32 @@ Function: string_constraint_generatort::add_axioms_for_insert Outputs: a new string expression - Purpose: add axioms corresponding to the StringBuilder.insert(String) java - function + Purpose: add axioms corresponding to the + StringBuilder.insert(int, CharSequence) + and StringBuilder.insert(int, CharSequence, int, int) + java functions \*******************************************************************/ string_exprt string_constraint_generatort::add_axioms_for_insert( const function_application_exprt &f) { - string_exprt s1=get_string_expr(args(f, 3)[0]); - string_exprt s2=get_string_expr(args(f, 3)[2]); - return add_axioms_for_insert(s1, s2, args(f, 3)[1]); + assert(f.arguments().size()>=3); + string_exprt s1=get_string_expr(f.arguments()[0]); + string_exprt s2=get_string_expr(f.arguments()[2]); + const exprt &offset=f.arguments()[1]; + if(f.arguments().size()==5) + { + const exprt &start=f.arguments()[3]; + const exprt &end=f.arguments()[4]; + string_exprt substring=add_axioms_for_substring(s2, start, end); + return add_axioms_for_insert(s1, substring, offset); + } + else + { + assert(f.arguments().size()==3); + return add_axioms_for_insert(s1, s2, offset); + } } /*******************************************************************\