Get rid of string_max_length field

In constraint generator, this was used for adding default axioms but is
no longer used.

Author: romainbrenguier

src/cbmc/cbmc_solvers.cpp

@@ -177,7 +177,7 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_string_refinement()
   info.refinement_bound=DEFAULT_MAX_NB_REFINEMENT;
   info.ui=ui;
   if(options.get_bool_option("string-max-length"))
-    info.string_max_length=options.get_signed_int_option("string-max-length");
+    info.max_string_length = options.get_signed_int_option("string-max-length");
   info.trace=options.get_bool_option("trace");
   if(options.get_bool_option("max-node-refinement"))
     info.max_node_refinement=

src/solvers/refinement/string_constraint_generator.h

@@ -94,14 +94,7 @@ class string_constraint_generatort final
   // Used by format function
   class format_specifiert;
 
-  /// Arguments pack for the string_constraint_generator constructor
-  struct infot
-  {
-    /// Max length of non-deterministic strings
-    size_t string_max_length=std::numeric_limits<size_t>::max();
-  };
-
-  string_constraint_generatort(const infot& info, const namespacet& ns);
+  explicit string_constraint_generatort(const namespacet &ns);
 
   /// Axioms are of three kinds: universally quantified string constraint,
   /// not contains string constraints and simple formulas.
@@ -401,7 +394,6 @@ class string_constraint_generatort final
 
   // MEMBERS
 public:
-  const size_t max_string_length;
   // Used to store information about witnesses for not_contains constraints
   std::map<string_not_contains_constraintt, symbol_exprt> witness;
 private:

src/solvers/refinement/string_constraint_generator_main.cpp

@@ -28,10 +28,8 @@ Author: Romain Brenguier, [email protected]
 #include <util/string_constant.h>
 #include <util/deprecate.h>
 
-string_constraint_generatort::string_constraint_generatort(
-  const string_constraint_generatort::infot &info,
-  const namespacet &ns)
-  : array_pool(fresh_symbol), max_string_length(info.string_max_length), ns(ns)
+string_constraint_generatort::string_constraint_generatort(const namespacet &ns)
+  : array_pool(fresh_symbol), ns(ns)
 {
 }
 

src/solvers/refinement/string_refinement.cpp

@@ -165,11 +165,14 @@ static bool validate(const string_refinementt::infot &info)
   return true;
 }
 
-string_refinementt::string_refinementt(const infot &info, bool):
-  supert(info),
-  config_(info),
-  loop_bound_(info.refinement_bound),
-  generator(info, *info.ns) { }
+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)
+{
+}
 
 string_refinementt::string_refinementt(const infot &info):
   string_refinementt(info, validate(info)) { }
@@ -734,13 +737,13 @@ decision_proceduret::resultt string_refinementt::dec_solve()
   {
     bool satisfied;
     std::vector<exprt> counter_examples;
-    std::tie(satisfied, counter_examples)=check_axioms(
+    std::tie(satisfied, counter_examples) = check_axioms(
       axioms,
       generator,
       get,
       debug(),
       ns,
-      generator.max_string_length,
+      max_string_length,
       config_.use_counter_example,
       supert::config_.ui,
       symbol_resolve);
@@ -778,13 +781,13 @@ decision_proceduret::resultt string_refinementt::dec_solve()
     {
       bool satisfied;
       std::vector<exprt> counter_examples;
-      std::tie(satisfied, counter_examples)=check_axioms(
+      std::tie(satisfied, counter_examples) = check_axioms(
         axioms,
         generator,
         get,
         debug(),
         ns,
-        generator.max_string_length,
+        max_string_length,
         config_.use_counter_example,
         supert::config_.ui,
         symbol_resolve);
@@ -2138,7 +2141,7 @@ exprt string_refinementt::get(const exprt &expr) const
 
     if(
       const auto arr_model_opt =
-        get_array(super_get, ns, generator.max_string_length, debug(), arr))
+        get_array(super_get, ns, max_string_length, debug(), arr))
       return *arr_model_opt;
 
     if(generator.get_created_strings().count(arr))

src/solvers/refinement/string_refinement.h

@@ -43,11 +43,11 @@ class string_refinementt final: public bv_refinementt
     /// Concretize strings after solver is finished
     bool trace=false;
     bool use_counter_example=true;
+    std::size_t max_string_length;
   };
 public:
   /// string_refinementt constructor arguments
   struct infot : public bv_refinementt::infot,
-                 public string_constraint_generatort::infot,
                  public configt
   {
   };
@@ -69,6 +69,7 @@ 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

unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp

@@ -192,8 +192,7 @@ SCENARIO("instantiate_not_contains",
     // Generating the corresponding axioms and simplifying, recording info
     symbol_tablet symtab;
     const namespacet empty_ns(symtab);
-    string_constraint_generatort::infot info;
-    string_constraint_generatort generator(info, ns);
+    string_constraint_generatort generator(ns);
     exprt res=generator.add_axioms_for_function_application(func);
     std::string axioms;
     std::vector<string_not_contains_constraintt> nc_axioms;
@@ -288,8 +287,7 @@ SCENARIO("instantiate_not_contains",
     // Create witness for axiom
     symbol_tablet symtab;
     const namespacet empty_ns(symtab);
-    string_constraint_generatort::infot info;
-    string_constraint_generatort generator(info, ns);
+    string_constraint_generatort generator(ns);
     generator.witness[vacuous]=
       generator.fresh_symbol("w", t.witness_type());
 
@@ -342,8 +340,7 @@ SCENARIO("instantiate_not_contains",
     // Create witness for axiom
     symbol_tablet symtab;
     const namespacet ns(symtab);
-    string_constraint_generatort::infot info;
-    string_constraint_generatort generator(info, ns);
+    string_constraint_generatort generator(ns);
     generator.witness[trivial]=
       generator.fresh_symbol("w", t.witness_type());
 
@@ -397,8 +394,7 @@ SCENARIO("instantiate_not_contains",
     // Create witness for axiom
     symbol_tablet symtab;
     const namespacet empty_ns(symtab);
-    string_constraint_generatort::infot info;
-    string_constraint_generatort generator(info, ns);
+    string_constraint_generatort generator(ns);
     generator.witness[trivial]=
       generator.fresh_symbol("w", t.witness_type());
 
@@ -455,8 +451,7 @@ SCENARIO("instantiate_not_contains",
     symbol_tablet symtab;
     const namespacet empty_ns(symtab);
 
-    string_constraint_generatort::infot info;
-    string_constraint_generatort generator(info, ns);
+    string_constraint_generatort generator(ns);
     generator.witness[trivial]=
       generator.fresh_symbol("w", t.witness_type());
 
@@ -510,8 +505,7 @@ SCENARIO("instantiate_not_contains",
     // Create witness for axiom
     symbol_tablet symtab;
     const namespacet empty_ns(symtab);
-    string_constraint_generatort::infot info;
-    string_constraint_generatort generator(info, ns);
+    string_constraint_generatort generator(ns);
     generator.witness[trivial]=
       generator.fresh_symbol("w", t.witness_type());