Remove anything that causes doxygen problems

Author: JohnDumbell

src/solvers/README.md

@@ -419,92 +419,92 @@ This is described in more detail \link string_builtin_functiont here. \endlink
   * `cprover_string_associate_length_to_array` : Link the length of the array
     with the given integer value.
   * `cprover_string_char_at` :
-  \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
+  \copybrief string_constraint_generatort::add_axioms_for_char_at(const function_application_exprt &f)
+  \link  string_constraint_generatort::add_axioms_for_char_at More... \endlink
   * `cprover_string_length` :
-  \copybrief add_axioms_for_length(const function_application_exprt &f, array_poolt &array_pool)
-  \link add_axioms_for_length More... \endlink
+  \copybrief string_constraint_generatort::add_axioms_for_length(const function_application_exprt &f)
+  \link string_constraint_generatort::add_axioms_for_length More... \endlink
 
 \subsection comparisons Comparisons:
 
   * `cprover_string_compare_to` :
-   \copybrief add_axioms_for_compare_to(symbol_generatort &fresh_symbol,const function_application_exprt &f, array_poolt &array_pool)
-   \link add_axioms_for_compare_to(symbol_generatort &fresh_symbol,const function_application_exprt &f, array_poolt &array_pool) More... \endlink
+   \copybrief string_constraint_generatort::add_axioms_for_compare_to(const function_application_exprt &f)
+   \link string_constraint_generatort::add_axioms_for_compare_to(const function_application_exprt &f) More... \endlink
   * `cprover_string_contains` :
-  \copybrief add_axioms_for_contains(symbol_generatort &fresh_symbol,const function_application_exprt &f, array_poolt &array_pool)
-  \link add_axioms_for_contains(symbol_generatort &fresh_symbol,const function_application_exprt &f, array_poolt &array_pool) More... \endlink
+  \copybrief string_constraint_generatort::add_axioms_for_contains(const function_application_exprt &f)
+  \link string_constraint_generatort::add_axioms_for_contains(const function_application_exprt &f) More... \endlink
   * `cprover_string_equals` :
-  \copybrief add_axioms_for_equals(symbol_generatort &fresh_symbol,const function_application_exprt &f, array_poolt &array_pool)
-  \link add_axioms_for_equals(symbol_generatort &fresh_symbol,const function_application_exprt &f, array_poolt &array_pool) More... \endlink
+  \copybrief string_constraint_generatort::add_axioms_for_equals(const function_application_exprt &f)
+  \link string_constraint_generatort::add_axioms_for_equals(const function_application_exprt &f) More... \endlink
   * `cprover_string_equals_ignore_case` :
-  \copybrief add_axioms_for_equals_ignore_case(symbol_generatort &fresh_symbol,const function_application_exprt &f, array_poolt &array_pool)
-  \link add_axioms_for_equals_ignore_case(symbol_generatort &fresh_symbol,const function_application_exprt &f, array_poolt &array_pool) More... \endlink
+  \copybrief string_constraint_generatort::add_axioms_for_equals_ignore_case(const function_application_exprt &f)
+  \link string_constraint_generatort::add_axioms_for_equals_ignore_case(const function_application_exprt &f) More... \endlink
   * `cprover_string_is_prefix` :
-  \copybrief add_axioms_for_is_prefix
-  \link add_axioms_for_is_prefix More... \endlink
+  \copybrief string_constraint_generatort::add_axioms_for_is_prefix
+  \link string_constraint_generatort::add_axioms_for_is_prefix More... \endlink
   * `cprover_string_index_of` :
-  \copybrief add_axioms_for_index_of(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
-  \link add_axioms_for_index_of(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink
+  \copybrief string_constraint_generatort::add_axioms_for_index_of(const function_application_exprt &f=)
+  \link string_constraint_generatort::add_axioms_for_index_of(const function_application_exprt &f) More... \endlink
   * `cprover_string_last_index_of` :
-  \copybrief add_axioms_for_last_index_of(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
-  \link add_axioms_for_last_index_of(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)  More... \endlink
+  \copybrief string_constraint_generatort::add_axioms_for_last_index_of(const function_application_exprt &f)
+  \link string_constraint_generatort::add_axioms_for_last_index_of(const function_application_exprt &f)  More... \endlink
 
 \subsection transformations Transformations:
 
   * `cprover_string_char_set` :
     \copybrief string_set_char_builtin_functiont::constraints
     \link string_set_char_builtin_functiont::constraints More... \endlink
   * `cprover_string_concat` :
-    \copybrief add_axioms_for_concat
-    \link add_axioms_for_concat More... \endlink
+    \copybrief string_constraint_generatort::add_axioms_for_concat
+    \link string_constraint_generatort::add_axioms_for_concat More... \endlink
   * `cprover_string_delete` :
-    \copybrief add_axioms_for_delete(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
-    \link add_axioms_for_delete(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink
+    \copybrief string_constraint_generatort::add_axioms_for_delete(const function_application_exprt &f)
+    \link string_constraint_generatort::add_axioms_for_delete(const function_application_exprt &f) More... \endlink
   * `cprover_string_insert` :
-    \copybrief add_axioms_for_insert(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
-    \link add_axioms_for_insert(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink
+    \copybrief string_constraint_generatort::add_axioms_for_insert(const function_application_exprt &f)
+    \link string_constraint_generatort::add_axioms_for_insert(const function_application_exprt &f) More... \endlink
   * `cprover_string_replace` :
-    \copybrief add_axioms_for_replace(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
-    \link add_axioms_for_replace(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink
+    \copybrief string_constraint_generatort::add_axioms_for_replace(const function_application_exprt &f)
+    \link string_constraint_generatort::add_axioms_for_replace(const function_application_exprt &f) More... \endlink
   * `cprover_string_set_length` :
-    \copybrief add_axioms_for_set_length(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
-    \link add_axioms_for_set_length(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink
+    \copybrief string_constraint_generatort::add_axioms_for_set_length(const function_application_exprt &f)
+    \link string_constraint_generatort::add_axioms_for_set_length(const function_application_exprt &f) More... \endlink
   * `cprover_string_substring` :
-    \copybrief add_axioms_for_substring(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
-    \link add_axioms_for_substring(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink
+    \copybrief string_constraint_generatort::add_axioms_for_substring(const function_application_exprt &f)
+    \link string_constraint_generatort::add_axioms_for_substring(const function_application_exprt &f) More... \endlink
   * `cprover_string_to_lower_case` :
     \copybrief string_to_lower_case_builtin_functiont::constraints
     \link string_to_lower_case_builtin_functiont::constraints More... \endlink
   * `cprover_string_to_upper_case` :
     \copybrief string_to_upper_case_builtin_functiont::constraints
     \link string_to_upper_case_builtin_functiont::constraints More... \endlink
   * `cprover_string_trim` :
-    \copybrief add_axioms_for_trim(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
-    \link add_axioms_for_trim(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink
+    \copybrief string_constraint_generatort::add_axioms_for_trim(const function_application_exprt &f)
+    \link string_constraint_generatort::add_axioms_for_trim(const function_application_exprt &f) More... \endlink
 
 \subsection conversions Conversions:
 
   * `cprover_string_format` :
     \copybrief add_axioms_for_format
     \link add_axioms_for_format More... \endlink
   * `cprover_string_from_literal` :
-    \copybrief add_axioms_from_literal(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
-    \link add_axioms_from_literal(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink
+    \copybrief string_constraint_generatort::add_axioms_from_literal(const function_application_exprt &f)
+    \link string_constraint_generatort::add_axioms_from_literal(const function_application_exprt &f) More... \endlink
   * `cprover_string_of_int` :
-    \copybrief add_axioms_for_string_of_int
-    \link add_axioms_for_string_of_int More... \endlink
+    \copybrief string_constraint_generatort::add_axioms_for_string_of_int
+    \link string_constraint_generatort::add_axioms_for_string_of_int More... \endlink
   * `cprover_string_of_float` :
-    \copybrief add_axioms_for_string_of_float
-    \link add_axioms_for_string_of_float More... \endlink
+    \copybrief string_constraint_generatort::add_axioms_for_string_of_float
+    \link string_constraint_generatort::add_axioms_for_string_of_float More... \endlink
   * `cprover_string_of_float_scientific_notation` :
-    \copybrief add_axioms_from_float_scientific_notation
-    \link add_axioms_from_float_scientific_notation More... \endlink
+    \copybrief string_constraint_generatort::add_axioms_from_float_scientific_notation
+    \link string_constraint_generatort::add_axioms_from_float_scientific_notation More... \endlink
   * `cprover_string_of_char` :
-    \copybrief add_axioms_from_char(const function_application_exprt &f, array_poolt &array_pool)
-    \link add_axioms_from_char(const function_application_exprt &f, array_poolt &array_pool) More... \endlink
+    \copybrief string_constraint_generatort::add_axioms_from_char(const function_application_exprt &f)
+    \link string_constraint_generatort::add_axioms_from_char(const function_application_exprt &f) More... \endlink
   * `cprover_string_parse_int` :
-    \copybrief add_axioms_for_parse_int
-    \link add_axioms_for_parse_int More... \endlink
+    \copybrief string_constraint_generatort::add_axioms_for_parse_int
+    \link string_constraint_generatort::add_axioms_for_parse_int More... \endlink
 
 \subsection solvers-deprecated Deprecated primitives:
 

src/solvers/strings/string_concatenation_builtin_function.cpp

@@ -43,13 +43,11 @@ string_concatenation_builtin_functiont::string_concatenation_builtin_functiont(
 ///   2. \f$\forall i<|s_1|. res[i]=s_1[i] \f$
 ///   3. \f$\forall i< |res| - |s_1|.\ res[i+|s_1|] = s_2[start\_index'+i]\f$
 ///
-/// \param fresh_symbol: generator of fresh symbols
 /// \param res: an array of characters expression
 /// \param s1: an array of characters expression
 /// \param s2: an array of characters expression
 /// \param start_index: integer expression
 /// \param end_index: integer expression
-/// \param array_pool: pool of arrays representing strings
 /// \return integer expression `0`
 std::pair<exprt, string_constraintst>
 string_constraint_generatort::add_axioms_for_concat_substr(
@@ -152,11 +150,9 @@ exprt length_constraint_for_concat_char(
 /// `s2`.
 ///
 /// \deprecated should use concat_substr instead
-/// \param fresh_symbol: generator of fresh symbols
 /// \param res: string_expression corresponding to the result
 /// \param s1: the string expression to append to
 /// \param s2: the string expression to append to the first one
-/// \param array_pool: pool of arrays representing strings
 /// \return an integer expression
 std::pair<exprt, string_constraintst>
 string_constraint_generatort::add_axioms_for_concat(
@@ -175,9 +171,7 @@ string_constraint_generatort::add_axioms_for_concat(
 
 /// Add axioms corresponding to the StringBuilder.appendCodePoint(I) function
 /// \deprecated java specific
-/// \param fresh_symbol: generator of fresh symbols
 /// \param f: function application with two arguments: a string and a code point
-/// \param array_pool: pool of arrays representing strings
 /// \return an expression
 std::pair<exprt, string_constraintst>
 string_constraint_generatort::add_axioms_for_concat_code_point(

src/solvers/strings/string_constraint_generator_code_points.cpp

@@ -16,7 +16,6 @@ Author: Romain Brenguier, [email protected]
 /// code point to a utf-16 string
 /// \param res: array of characters corresponding to the result fo the function
 /// \param code_point: an expression representing a java code point
-/// \param array_pool: pool of arrays representing strings
 /// \return integer expression equal to zero
 std::pair<exprt, string_constraintst>
 string_constraint_generatort::add_axioms_for_code_point(
@@ -116,10 +115,8 @@ exprt pair_value(exprt char1, exprt char2, typet return_type)
 }
 
 /// add axioms corresponding to the String.codePointAt java function
-/// \param fresh_symbol: generator of fresh symbols
 /// \param f: function application with arguments a string and an
 ///   index
-/// \param array_pool: pool of arrays representing strings
 /// \return a integer expression corresponding to a code point
 std::pair<exprt, string_constraintst>
 string_constraint_generatort::add_axioms_for_code_point_at(
@@ -185,10 +182,8 @@ string_constraint_generatort::add_axioms_for_code_point_before(
 
 /// add axioms giving approximate bounds on the result of the
 /// String.codePointCount java function
-/// \param fresh_symbol: generator of fresh symbols
 /// \param f: function application with three arguments string `str`, integer
 ///   `begin` and integer `end`.
-/// \param array_pool: pool of arrays representing strings
 /// \return an integer expression
 std::pair<exprt, string_constraintst>
 string_constraint_generatort::add_axioms_for_code_point_count(
@@ -213,7 +208,6 @@ string_constraint_generatort::add_axioms_for_code_point_count(
 /// add axioms giving approximate bounds on the result of the
 /// String.offsetByCodePointCount java function. We approximate the result by
 /// saying the result is between index + offset and index + 2 * offset
-/// \param fresh_symbol: generator of fresh symbols
 /// \param f: function application with arguments string `str`, integer `index`
 ///           and integer `offset`.
 /// \return a new string expression

src/solvers/strings/string_constraint_generator_comparison.cpp

@@ -24,10 +24,8 @@ Author: Romain Brenguier, [email protected]
 ///   2. \f$ \forall i<|s_1|.\ eq \Rightarrow s_1[i]=s_2[i] \f$
 ///   3. \f$ \lnot eq \Rightarrow (|s_1| \ne |s_2| \land witness=-1)
 ///          \lor (0 \le witness<|s_1| \land s_1[witness] \ne s_2[witness]) \f$
-/// \param fresh_symbol: generator of fresh symbols
 /// \param f: function application with arguments refined_string `s1` and
 ///   refined_string `s2`
-/// \param array_pool: pool of arrays representing strings
 /// \return Boolean expression `eq`
 std::pair<exprt, string_constraintst>
 string_constraint_generatort::add_axioms_for_equals(
@@ -130,10 +128,8 @@ static exprt character_equals_ignore_case(
 ///          \ eq \Rightarrow {\tt equal\_ignore\_case}(s_1[i],s_2[i]) \f$
 ///   3. \f$ \lnot eq \Rightarrow |s_1| \ne |s_2| \lor (0 \le witness<|s_1|
 ///          \land\lnot {\tt equal\_ignore\_case}(s_1[witness],s_2[witness]) \f$
-/// \param fresh_symbol: generator of fresh symbols
 /// \param f: function application with arguments refined_string `s1` and
 ///   refined_string `s2`
-/// \param array_pool: pool of arrays representing strings
 /// \return Boolean expression `eq`
 std::pair<exprt, string_constraintst>
 string_constraint_generatort::add_axioms_for_equals_ignore_case(
@@ -204,10 +200,8 @@ string_constraint_generatort::add_axioms_for_equals_ignore_case(
 ///         (|s1|<|s2| \land x=|s1|) \lor (|s1| > |s2| \land x=|s2|)
 ///         \land res=|s1|-|s2|) \f$
 ///   * \f$ \forall i'<x. res\ne 0 \Rightarrow s1[i]=s2[i] \f$
-/// \param fresh_symbol: generator of fresh symbols
 /// \param f: function application with arguments refined_string `s1` and
 ///   refined_string `s2`
-/// \param array_pool: pool of arrays representing strings
 /// \return integer expression `res`
 std::pair<exprt, string_constraintst>
 string_constraint_generatort::add_axioms_for_compare_to(

src/solvers/strings/string_constraint_generator_constants.cpp

@@ -18,7 +18,6 @@ Author: Romain Brenguier, [email protected]
 /// equal.
 /// \param res: array of characters for the result
 /// \param sval: a string constant
-/// \param array_pool: pool of arrays representing strings
 /// \param guard: condition under which the axiom should apply, true by default
 /// \return integer expression equal to zero
 std::pair<exprt, string_constraintst>
@@ -74,11 +73,9 @@ string_constraint_generatort::add_axioms_for_empty_string(
 }
 
 /// Convert an expression of type string_typet to a string_exprt
-/// \param fresh_symbol: generator of fresh symbols
 /// \param res: string expression for the result
 /// \param arg: expression of type string typet
 /// \param guard: condition under which `res` should be equal to arg
-/// \param array_pool: pool of arrays representing strings
 /// \return 0 if constraints were added, 1 if expression could not be handled
 ///   and no constraint was added. Expression we can handle are of the form
 ///   \f$ e := "<string constant>" | (expr)? e : e \f$
@@ -108,10 +105,8 @@ string_constraint_generatort::add_axioms_for_cprover_string(
 /// Add axioms ensuring that the returned string expression is equal to the
 /// string literal.
 /// \todo The name of the function should be changed to reflect what it does.
-/// \param fresh_symbol: generator of fresh symbols
 /// \param f: function application with an argument which is a string literal
 ///   that is a constant with a string value.
-/// \param array_pool: pool of arrays representing strings
 /// \return string expression
 std::pair<exprt, string_constraintst>
 string_constraint_generatort::add_axioms_from_literal(