diff --git a/src/solvers/README.md b/src/solvers/README.md index 32643b15f4b..d53258c6ffa 100644 --- a/src/solvers/README.md +++ b/src/solvers/README.md @@ -221,7 +221,7 @@ allocates a new string before calling a primitive. \copybrief add_axioms_for_char_at(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) \link add_axioms_for_char_at More... \endlink * `cprover_string_length` : - \copybrief add_axioms_for_length(symbol_generatort &fresh_symbol,const function_application_exprt &f, array_poolt &array_pool) + \copybrief add_axioms_for_length(const function_application_exprt &f, array_poolt &array_pool) \link add_axioms_for_length More... \endlink \subsection comparisons Comparisons: diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h index 7bf61dad3d1..5306ba35801 100644 --- a/src/solvers/refinement/string_constraint_generator.h +++ b/src/solvers/refinement/string_constraint_generator.h @@ -267,11 +267,9 @@ std::pair add_axioms_for_is_suffix( bool swap_arguments, array_poolt &array_pool); std::pair add_axioms_for_length( - symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool); std::pair add_axioms_for_empty_string( - symbol_generatort &fresh_symbol, const function_application_exprt &f); std::pair add_axioms_for_copy( @@ -438,7 +436,6 @@ std::pair add_axioms_for_string_of_float( array_poolt &array_pool, const namespacet &ns); std::pair add_axioms_for_fractional_part( - symbol_generatort &fresh_symbol, const array_string_exprt &res, const exprt &i, size_t max_size); @@ -491,11 +488,9 @@ std::pair add_axioms_for_trim( array_poolt &array_pool); std::pair add_axioms_for_code_point( - symbol_generatort &fresh_symbol, const array_string_exprt &res, const exprt &code_point); std::pair add_axioms_for_char_literal( - symbol_generatort &fresh_symbol, const function_application_exprt &f); /// Add axioms corresponding the String.codePointCount java function diff --git a/src/solvers/refinement/string_constraint_generator_code_points.cpp b/src/solvers/refinement/string_constraint_generator_code_points.cpp index 53ffbb02388..787bfe72e25 100644 --- a/src/solvers/refinement/string_constraint_generator_code_points.cpp +++ b/src/solvers/refinement/string_constraint_generator_code_points.cpp @@ -14,12 +14,10 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com /// add axioms for the conversion of an integer representing a java /// code point to a utf-16 string -/// \param fresh_symbol: generator of fresh symbols /// \param res: array of characters corresponding to the result fo the function /// \param code_point: an expression representing a java code point /// \return integer expression equal to zero std::pair add_axioms_for_code_point( - symbol_generatort &fresh_symbol, const array_string_exprt &res, const exprt &code_point) { diff --git a/src/solvers/refinement/string_constraint_generator_concat.cpp b/src/solvers/refinement/string_constraint_generator_concat.cpp index 26be4cd41c0..6b5465b0daa 100644 --- a/src/solvers/refinement/string_constraint_generator_concat.cpp +++ b/src/solvers/refinement/string_constraint_generator_concat.cpp @@ -154,6 +154,6 @@ std::pair add_axioms_for_concat_code_point( const array_string_exprt code_point = array_pool.fresh_string(index_type, char_type); return combine_results( - add_axioms_for_code_point(fresh_symbol, code_point, f.arguments()[3]), + add_axioms_for_code_point(code_point, f.arguments()[3]), add_axioms_for_concat(fresh_symbol, res, s1, code_point)); } diff --git a/src/solvers/refinement/string_constraint_generator_constants.cpp b/src/solvers/refinement/string_constraint_generator_constants.cpp index 2bd0be6fc7a..8daf47c57e5 100644 --- a/src/solvers/refinement/string_constraint_generator_constants.cpp +++ b/src/solvers/refinement/string_constraint_generator_constants.cpp @@ -57,12 +57,10 @@ std::pair add_axioms_for_constant( } /// Add axioms to say that the returned string expression is empty -/// \param fresh_symbol: generator of fresh symbols /// \param f: function application with arguments integer `length` and character /// pointer `ptr`. /// \return integer expression equal to zero std::pair add_axioms_for_empty_string( - symbol_generatort &fresh_symbol, const function_application_exprt &f) { PRECONDITION(f.arguments().size() == 2); diff --git a/src/solvers/refinement/string_constraint_generator_float.cpp b/src/solvers/refinement/string_constraint_generator_float.cpp index 5cf6a763b06..3c9876816a7 100644 --- a/src/solvers/refinement/string_constraint_generator_float.cpp +++ b/src/solvers/refinement/string_constraint_generator_float.cpp @@ -221,8 +221,8 @@ std::pair add_axioms_for_string_of_float( const mod_exprt fractional_part(shifted, max_non_exponent_notation); const array_string_exprt fractional_part_str = array_pool.fresh_string(index_type, char_type); - auto result1 = add_axioms_for_fractional_part( - fresh_symbol, fractional_part_str, fractional_part, 6); + auto result1 = + add_axioms_for_fractional_part(fractional_part_str, fractional_part, 6); // The axiom added to convert to integer should always be satisfiable even // when the preconditions are not satisfied. @@ -247,14 +247,12 @@ std::pair add_axioms_for_string_of_float( /// Add axioms for representing the fractional part of a floating point starting /// with a dot -/// \param fresh_symbol: generator of fresh symbols /// \param res: string expression for the result /// \param int_expr: an integer expression /// \param max_size: a maximal size for the string, this includes the /// potential minus sign and therefore should be greater than 2 /// \return code 0 on success std::pair add_axioms_for_fractional_part( - symbol_generatort &fresh_symbol, const array_string_exprt &res, const exprt &int_expr, size_t max_size) @@ -478,7 +476,7 @@ std::pair add_axioms_from_float_scientific_notation( array_string_exprt string_fractional_part = array_pool.fresh_string(index_type, char_type); auto result2 = add_axioms_for_fractional_part( - fresh_symbol, string_fractional_part, fractional_part_shifted, 6); + string_fractional_part, fractional_part_shifted, 6); // string_expr_with_fractional_part = // concat(string_with_do, string_fractional_part) diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp index 6f8d70cb0d3..d2110bd2fd5 100644 --- a/src/solvers/refinement/string_constraint_generator_main.cpp +++ b/src/solvers/refinement/string_constraint_generator_main.cpp @@ -374,9 +374,9 @@ string_constraint_generatort::add_axioms_for_function_application( const irep_idt &id = get_function_name(expr); if(id==ID_cprover_char_literal_func) - return add_axioms_for_char_literal(fresh_symbol, expr); + return add_axioms_for_char_literal(expr); else if(id==ID_cprover_string_length_func) - return add_axioms_for_length(fresh_symbol, expr, array_pool); + return add_axioms_for_length(expr, array_pool); else if(id==ID_cprover_string_equal_func) return add_axioms_for_equals(fresh_symbol, expr, array_pool); else if(id==ID_cprover_string_equals_ignore_case_func) @@ -436,7 +436,7 @@ string_constraint_generatort::add_axioms_for_function_application( else if(id==ID_cprover_string_trim_func) return add_axioms_for_trim(fresh_symbol, expr, array_pool); else if(id==ID_cprover_string_empty_string_func) - return add_axioms_for_empty_string(fresh_symbol, expr); + return add_axioms_for_empty_string(expr); else if(id==ID_cprover_string_copy_func) return add_axioms_for_copy(fresh_symbol, expr, array_pool); else if(id==ID_cprover_string_of_int_hex_func) @@ -507,12 +507,10 @@ std::pair add_axioms_for_copy( /// Length of a string /// /// Returns the length of the string argument of the given function application -/// \param fresh_symbol: generator of fresh symbols /// \param f: function application with argument string `str` /// \param array_pool: pool of arrays representing strings /// \return expression `|str|` std::pair add_axioms_for_length( - symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) { @@ -529,11 +527,9 @@ exprt is_positive(const exprt &x) } /// add axioms stating that the returned value is equal to the argument -/// \param fresh_symbol: generator of fresh symbols /// \param f: function application with one character argument /// \return a new character expression std::pair add_axioms_for_char_literal( - symbol_generatort &fresh_symbol, const function_application_exprt &f) { const function_application_exprt::argumentst &args=f.arguments();