Merge pull request #2542 from tautschnig/vs-string-refinement

String refinement: remove unused parameters

Author: tautschnig

src/solvers/refinement/string_builtin_function.h

@@ -195,7 +195,7 @@ class string_insertion_builtin_functiont : public string_builtin_functiont
   exprt length_constraint() const override
   {
     if(args.size() == 1)
-      return length_constraint_for_insert(result, input1, input2, args[0]);
+      return length_constraint_for_insert(result, input1, input2);
     if(args.size() == 3)
       UNIMPLEMENTED;
     UNREACHABLE;

src/solvers/refinement/string_constraint_generator.h

@@ -365,7 +365,6 @@ class string_constraint_generatort final
     const exprt &radix,
     const unsigned long radix_ul);
   void add_axioms_for_correct_number_format(
-    const exprt &input_int,
     const array_string_exprt &str,
     const exprt &radix_as_char,
     const unsigned long radix_ul,
@@ -457,7 +456,6 @@ exprt length_constraint_for_concat_substr(
 exprt length_constraint_for_insert(
   const array_string_exprt &res,
   const array_string_exprt &s1,
-  const array_string_exprt &s2,
-  const exprt &offset);
+  const array_string_exprt &s2);
 
 #endif

src/solvers/refinement/string_constraint_generator_insert.cpp

@@ -41,7 +41,7 @@ exprt string_constraint_generatort::add_axioms_for_insert(
     maximum(from_integer(0, index_type), minimum(s1.length(), offset));
 
   // Axiom 1.
-  lemmas.push_back(length_constraint_for_insert(res, s1, s2, offset));
+  lemmas.push_back(length_constraint_for_insert(res, s1, s2));
 
   // Axiom 2.
   constraints.push_back([&] { // NOLINT
@@ -69,13 +69,12 @@ exprt string_constraint_generatort::add_axioms_for_insert(
   return from_integer(0, get_return_code_type());
 }
 
-/// Add axioms ensuring the length of `res` corresponds that of `s1` where we
-/// inserted `s2` at position `offset`.
+/// Add axioms ensuring the length of `res` corresponds to that of `s1` where we
+/// inserted `s2`.
 exprt length_constraint_for_insert(
   const array_string_exprt &res,
   const array_string_exprt &s1,
-  const array_string_exprt &s2,
-  const exprt &offset)
+  const array_string_exprt &s2)
 {
   return equal_exprt(res.length(), plus_exprt(s1.length(), s2.length()));
 }

src/solvers/refinement/string_constraint_generator_valueof.cpp

@@ -169,7 +169,7 @@ exprt string_constraint_generatort::add_axioms_from_int_with_radix(
   const bool strict_formatting=true;
 
   add_axioms_for_correct_number_format(
-    input_int, res, radix_as_char, radix_ul, max_size, strict_formatting);
+    res, radix_as_char, radix_ul, max_size, strict_formatting);
 
   add_axioms_for_characters_in_integer_string(
     input_int,
@@ -306,7 +306,6 @@ exprt string_constraint_generatort::add_axioms_from_char(
 
 /// Add axioms making the return value true if the given string is a correct
 /// number in the given radix
-/// \param input_int: the number being represented as a string
 /// \param str: string expression
 /// \param radix_as_char: the radix as an expression of the same type as the
 ///   characters in str
@@ -316,7 +315,6 @@ exprt string_constraint_generatort::add_axioms_from_char(
 /// \param strict_formatting: if true, don't allow a leading plus, redundant
 ///   zeros or upper case letters
 void string_constraint_generatort::add_axioms_for_correct_number_format(
-  const exprt &input_int,
   const array_string_exprt &str,
   const exprt &radix_as_char,
   const unsigned long radix_ul,
@@ -515,7 +513,6 @@ exprt string_constraint_generatort::add_axioms_for_parse_int(
   /// \note the only thing stopping us from taking longer strings with many
   /// leading zeros is the axioms for correct number format
   add_axioms_for_correct_number_format(
-    input_int,
     str,
     radix_as_char,
     radix_ul,

src/solvers/refinement/string_refinement.cpp

@@ -37,7 +37,6 @@ static bool is_valid_string_constraint(
 
 static optionalt<exprt> find_counter_example(
   const namespacet &ns,
-  ui_message_handlert::uit ui,
   const exprt &axiom,
   const symbol_exprt &var);
 
@@ -63,9 +62,7 @@ static std::pair<bool, std::vector<exprt>> check_axioms(
   const std::function<exprt(const exprt &)> &get,
   messaget::mstreamt &stream,
   const namespacet &ns,
-  std::size_t max_string_length,
   bool use_counter_example,
-  ui_message_handlert::uit ui,
   const union_find_replacet &symbol_resolve);
 
 static void initial_index_set(
@@ -119,7 +116,6 @@ static std::vector<exprt> instantiate(
 static optionalt<exprt> get_array(
   const std::function<exprt(const exprt &)> &super_get,
   const namespacet &ns,
-  const std::size_t max_string_length,
   messaget::mstreamt &stream,
   const array_string_exprt &arr);
 
@@ -171,7 +167,6 @@ string_refinementt::string_refinementt(const infot &info, bool)
   : supert(info),
     config_(info),
     loop_bound_(info.refinement_bound),
-    max_string_length(info.max_string_length),
     generator(*info.ns)
 {
 }
@@ -232,7 +227,6 @@ static void display_index_set(
 ///      for details)
 static std::vector<exprt> generate_instantiations(
   messaget::mstreamt &stream,
-  const namespacet &ns,
   const string_constraint_generatort &generator,
   const index_set_pairt &index_set,
   const string_axiomst &axioms)
@@ -532,16 +526,17 @@ union_find_replacet string_identifiers_resolution_from_equations(
   return result;
 }
 
+#ifdef DEBUG
 /// Output a vector of equations to the given stream, used for debugging.
-void output_equations(
+static void output_equations(
   std::ostream &output,
-  const std::vector<equal_exprt> &equations,
-  const namespacet &ns)
+  const std::vector<equal_exprt> &equations)
 {
   for(std::size_t i = 0; i < equations.size(); ++i)
     output << "  [" << i << "] " << format(equations[i].lhs())
            << " == " << format(equations[i].rhs()) << std::endl;
 }
+#endif
 
 /// Main decision procedure of the solver. Looks for a valuation of variables
 /// compatible with the constraints that have been given to `set_to` so far.
@@ -611,7 +606,7 @@ decision_proceduret::resultt string_refinementt::dec_solve()
 {
 #ifdef DEBUG
   debug() << "dec_solve: Initial set of equations" << eom;
-  output_equations(debug(), equations, ns);
+  output_equations(debug(), equations);
 #endif
 
   debug() << "dec_solve: Build symbol solver from equations" << eom;
@@ -650,7 +645,7 @@ decision_proceduret::resultt string_refinementt::dec_solve()
   make_char_array_pointer_associations(generator, equations);
 
 #ifdef DEBUG
-  output_equations(debug(), equations, ns);
+  output_equations(debug(), equations);
 #endif
 
   debug() << "dec_solve: compute dependency graph and remove function "
@@ -671,7 +666,7 @@ decision_proceduret::resultt string_refinementt::dec_solve()
   dependencies.add_constraints(generator);
 
 #ifdef DEBUG
-  output_equations(debug(), equations, ns);
+  output_equations(debug(), equations);
 #endif
 
 #ifdef DEBUG
@@ -744,9 +739,7 @@ decision_proceduret::resultt string_refinementt::dec_solve()
       get,
       debug(),
       ns,
-      max_string_length,
       config_.use_counter_example,
-      supert::config_.ui,
       symbol_resolve);
     if(satisfied)
     {
@@ -767,7 +760,6 @@ decision_proceduret::resultt string_refinementt::dec_solve()
   for(const auto &instance :
         generate_instantiations(
           debug(),
-          ns,
           generator,
           index_sets,
           axioms))
@@ -788,9 +780,7 @@ decision_proceduret::resultt string_refinementt::dec_solve()
         get,
         debug(),
         ns,
-        max_string_length,
         config_.use_counter_example,
-        supert::config_.ui,
         symbol_resolve);
       if(satisfied)
       {
@@ -830,7 +820,6 @@ decision_proceduret::resultt string_refinementt::dec_solve()
       for(const auto &instance :
         generate_instantiations(
           debug(),
-          ns,
           generator,
           index_sets,
           axioms))
@@ -899,14 +888,12 @@ void string_refinementt::add_lemma(
 /// \param super_get: function returning the valuation of an expression
 ///        in a model
 /// \param ns: namespace
-/// \param max_string_length: maximum length of strings to analyze
 /// \param stream: output stream for warning messages
 /// \param arr: expression of type array representing a string
 /// \return an optional array expression or array_of_exprt
 static optionalt<exprt> get_array(
   const std::function<exprt(const exprt &)> &super_get,
   const namespacet &ns,
-  const std::size_t max_string_length,
   messaget::mstreamt &stream,
   const array_string_exprt &arr)
 {
@@ -975,14 +962,12 @@ static std::string string_of_array(const array_exprt &arr)
 /// `super_get` and concretize unknown characters.
 /// \param super_get: give a valuation to variables
 /// \param ns: namespace
-/// \param max_string_length: limit up to which we concretize strings
 /// \param stream: output stream
 /// \param arr: array expression
 /// \return expression corresponding to `arr` in the model
 static exprt get_char_array_and_concretize(
   const std::function<exprt(const exprt &)> &super_get,
   const namespacet &ns,
-  const std::size_t max_string_length,
   messaget::mstreamt &stream,
   const array_string_exprt &arr)
 {
@@ -991,7 +976,7 @@ static exprt get_char_array_and_concretize(
   stream << "- " << format(arr) << ":\n";
   stream << indent << indent << "- type: " << format(arr.type()) << eom;
   const auto arr_model_opt =
-    get_array(super_get, ns, max_string_length, stream, arr);
+    get_array(super_get, ns, stream, arr);
   if(arr_model_opt)
   {
     stream << indent << indent << "- char_array: " << format(*arr_model_opt)
@@ -1003,7 +988,7 @@ static exprt get_char_array_and_concretize(
            << eom;
     if(
       const auto concretized_array = get_array(
-        super_get, ns, max_string_length, stream, to_array_string_expr(simple)))
+        super_get, ns, stream, to_array_string_expr(simple)))
     {
       stream << indent << indent
              << "- concretized_char_array: " << format(*concretized_array)
@@ -1032,7 +1017,6 @@ void debug_model(
   const string_constraint_generatort &generator,
   messaget::mstreamt &stream,
   const namespacet &ns,
-  const std::size_t max_string_length,
   const std::function<exprt(const exprt &)> &super_get,
   const std::vector<symbol_exprt> &boolean_symbols,
   const std::vector<symbol_exprt> &index_symbols)
@@ -1044,7 +1028,7 @@ void debug_model(
   {
     const auto arr = pointer_array.second;
     const exprt model = get_char_array_and_concretize(
-      super_get, ns, max_string_length, stream, arr);
+      super_get, ns, stream, arr);
 
     stream << "- " << format(arr) << ":\n"
            << indent << "- pointer: " << format(pointer_array.first) << "\n"
@@ -1243,7 +1227,6 @@ static exprt negation_of_not_contains_constraint(
 template <typename T>
 static void debug_check_axioms_step(
   messaget::mstreamt &stream,
-  const namespacet &ns,
   const T &axiom,
   const T &axiom_in_model,
   const exprt &negaxiom,
@@ -1269,9 +1252,7 @@ static std::pair<bool, std::vector<exprt>> check_axioms(
   const std::function<exprt(const exprt &)> &get,
   messaget::mstreamt &stream,
   const namespacet &ns,
-  std::size_t max_string_length,
   bool use_counter_example,
-  ui_message_handlert::uit ui,
   const union_find_replacet &symbol_resolve)
 {
   const auto eom=messaget::eom;
@@ -1297,7 +1278,6 @@ static std::pair<bool, std::vector<exprt>> check_axioms(
     generator,
     stream,
     ns,
-    max_string_length,
     get,
     generator.get_boolean_symbols(),
     generator.get_index_symbols());
@@ -1324,11 +1304,11 @@ static std::pair<bool, std::vector<exprt>> check_axioms(
     const exprt with_concretized_arrays =
       substitute_array_access(negaxiom, gen_symbol, true);
     debug_check_axioms_step(
-      stream, ns, axiom, axiom_in_model, negaxiom, with_concretized_arrays);
+      stream, axiom, axiom_in_model, negaxiom, with_concretized_arrays);
 
     if(
       const auto &witness =
-        find_counter_example(ns, ui, with_concretized_arrays, axiom.univ_var))
+        find_counter_example(ns, with_concretized_arrays, axiom.univ_var))
     {
       stream << indent2 << "- violated_for: " << format(axiom.univ_var) << "="
              << format(*witness) << eom;
@@ -1354,11 +1334,11 @@ static std::pair<bool, std::vector<exprt>> check_axioms(
 
     stream << indent << i << ".\n";
     debug_check_axioms_step(
-      stream, ns, nc_axiom, nc_axiom, negated_axiom, negated_axiom);
+      stream, nc_axiom, nc_axiom, negated_axiom, negated_axiom);
 
     if(
       const auto witness =
-        find_counter_example(ns, ui, negated_axiom, univ_var))
+        find_counter_example(ns, negated_axiom, univ_var))
     {
       stream << indent2 << "- violated_for: " << univ_var.get_identifier()
              << "=" << format(*witness) << eom;
@@ -2051,7 +2031,7 @@ exprt string_refinementt::get(const exprt &expr) const
 
     if(
       const auto arr_model_opt =
-        get_array(super_get, ns, max_string_length, debug(), arr))
+        get_array(super_get, ns, debug(), arr))
       return *arr_model_opt;
 
     if(generator.get_created_strings().count(arr))
@@ -2073,14 +2053,12 @@ exprt string_refinementt::get(const exprt &expr) const
 /// is SAT, then true is returned and the given evaluation of `var` is stored
 /// in `witness`. If UNSAT, then what witness is is undefined.
 /// \param ns: namespace
-/// \param ui: message handler
 /// \param [in] axiom: the axiom to be checked
 /// \param [in] var: the variable whose evaluation will be stored in witness
 /// \return: the witness of the satisfying assignment if one
 /// exists. If UNSAT, then behaviour is undefined.
 static optionalt<exprt> find_counter_example(
   const namespacet &ns,
-  const ui_message_handlert::uit ui,
   const exprt &axiom,
   const symbol_exprt &var)
 {

src/solvers/refinement/string_refinement.h

@@ -67,7 +67,6 @@ class string_refinementt final: public bv_refinementt
 
   const configt config_;
   std::size_t loop_bound_;
-  std::size_t max_string_length;
   string_constraint_generatort generator;
 
   // Simple constraints that have been given to the solver