Refactor string refinement constructors

src/cbmc/cbmc_solvers.cpp

@@ -179,20 +179,14 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_string_refinement()
   info.string_non_empty=options.get_bool_option("string-non-empty");
   info.trace=options.get_bool_option("trace");
   info.string_printable=options.get_bool_option("string-printable");
-
-  auto string_refinement=util_make_unique<string_refinementt>(info);
-
-  if(options.get_option("max-node-refinement")!="")
-    string_refinement->max_node_refinement=
+  if(options.get_bool_option("max-node-refinement"))
+    info.max_node_refinement=
       options.get_unsigned_int_option("max-node-refinement");
-
-  string_refinement->do_array_refinement=
-    options.get_bool_option("refine-arrays");
-  string_refinement->do_arithmetic_refinement=
-    options.get_bool_option("refine-arithmetic");
+  info.refine_arrays=options.get_bool_option("refine-arrays");
+  info.refine_arithmetic=options.get_bool_option("refine-arithmetic");
 
   return util_make_unique<solvert>(
-    std::move(string_refinement), std::move(prop));
+    util_make_unique<string_refinementt>(info), std::move(prop));
 }
 
 std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_smt1(

src/solvers/refinement/string_refinement.cpp

@@ -53,6 +53,9 @@ string_refinementt::string_refinementt(const infot &info, bool):
   this->set_ui(ui);
   generator.max_string_length=info.string_max_length;
   generator.force_printable_characters=info.string_printable;
+  this->max_node_refinement=info.max_node_refinement;
+  this->do_array_refinement=info.refine_arrays;
+  this->do_arithmetic_refinement=info.refine_arithmetic;
 }
 
 string_refinementt::string_refinementt(const infot &info):

src/solvers/refinement/string_refinement.h

@@ -28,7 +28,7 @@ Author: Alberto Griggio, [email protected]
 
 #define MAX_NB_REFINEMENT 100
 
-class string_refinementt: public bv_refinementt
+class string_refinementt final: public bv_refinementt
 {
 public:
   /// string_refinementt constructor arguments
@@ -41,19 +41,21 @@ class string_refinementt: public bv_refinementt
     size_t string_max_length=std::numeric_limits<size_t>::max();
     /// Make non deterministic character arrays have at least one character
     bool string_non_empty=false;
+    // Should we concretize strings when the solver finished
     bool trace=false;
     /// Make non-deterministic characters printable
     bool string_printable=false;
+    unsigned max_node_refinement=5;
+    bool refine_arrays=false;
+    bool refine_arithmetic=false;
   };
+
   explicit string_refinementt(const infot &);
 
   void set_mode();
 
   // Should we use counter examples at each iteration?
-  bool use_counter_example;
-
-  // Should we concretize strings when the solver finished
-  const bool do_concretizing;
+  const bool use_counter_example=false;
 
   virtual std::string decision_procedure_text() const override
   {
@@ -65,17 +67,18 @@ class string_refinementt: public bv_refinementt
   exprt get(const exprt &expr) const override;
 
 protected:
-  typedef std::set<exprt> expr_sett;
-  typedef std::list<exprt> exprt_listt;
-
   decision_proceduret::resultt dec_solve() override;
 
-  bvt convert_bool_bv(const exprt &boole, const exprt &orig);
-
 private:
+  const bool do_concretizing;
   // Base class
   typedef bv_refinementt supert;
+
+  typedef std::set<exprt> expr_sett;
+  typedef std::list<exprt> exprt_listt;
+
   string_refinementt(const infot &, bool);
+  bvt convert_bool_bv(const exprt &boole, const exprt &orig);
 
   unsigned initial_loop_bound;