Merge pull request #1300 from LAJW/refactor/string-refinement-constructors

Refactor string refinement constructors

Author: romainbrenguier

src/cbmc/cbmc_solvers.cpp

@@ -146,54 +146,49 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_bv_refinement()
 
   prop->set_message_handler(get_message_handler());
 
-  auto bv_refinement=util_make_unique<bv_refinementt>(ns, *prop);
-  bv_refinement->set_ui(ui);
+  bv_refinementt::infot info;
+  info.ns=&ns;
+  info.prop=prop.get();
+  info.ui=ui;
 
   // we allow setting some parameters
-  if(options.get_option("max-node-refinement")!="")
-    bv_refinement->max_node_refinement =
+  if(options.get_bool_option("max-node-refinement"))
+    info.max_node_refinement=
       options.get_unsigned_int_option("max-node-refinement");
 
-  bv_refinement->do_array_refinement =
-    options.get_bool_option("refine-arrays");
-  bv_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(bv_refinement), std::move(prop));
+  return util_make_unique<solvert>(
+    util_make_unique<bv_refinementt>(info),
+    std::move(prop));
 }
 
 /// the string refinement adds to the bit vector refinement specifications for
 /// functions from the Java string library
 /// \return a solver for cbmc
 std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_string_refinement()
 {
+  string_refinementt::infot info;
+  info.ns=&ns;
   auto prop=util_make_unique<satcheck_no_simplifiert>();
   prop->set_message_handler(get_message_handler());
-
-  auto string_refinement=util_make_unique<string_refinementt>(
-    ns, *prop, MAX_NB_REFINEMENT);
-  string_refinement->set_ui(ui);
-
-  string_refinement->do_concretizing=options.get_bool_option("trace");
+  info.prop=prop.get();
+  info.refinement_bound=MAX_NB_REFINEMENT;
+  info.ui=ui;
   if(options.get_bool_option("string-max-length"))
-    string_refinement->set_max_string_length(
-      options.get_signed_int_option("string-max-length"));
-  if(options.get_bool_option("string-non-empty"))
-    string_refinement->enforce_non_empty_string();
-  if(options.get_bool_option("string-printable"))
-    string_refinement->enforce_printable_characters();
-
-  if(options.get_option("max-node-refinement")!="")
-    string_refinement->max_node_refinement=
+    info.string_max_length=options.get_signed_int_option("string-max-length");
+  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");
+  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/bv_refinement.h

@@ -21,34 +21,44 @@ Author: Daniel Kroening, [email protected]
 class bv_refinementt:public bv_pointerst
 {
 public:
-  bv_refinementt(const namespacet &_ns, propt &_prop);
-  ~bv_refinementt();
+  struct infot
+  {
+    const namespacet *ns=nullptr;
+    propt *prop=nullptr;
+    language_uit::uit ui=language_uit::uit::PLAIN;
+    /// Max number of times we refine a formula node
+    unsigned max_node_refinement=5;
+    /// Enable array refinement
+    bool refine_arrays=true;
+    /// Enable arithmetic refinement
+    bool refine_arithmetic=true;
+  };
 
-  virtual decision_proceduret::resultt dec_solve();
+  explicit bv_refinementt(const infot &info);
 
-  virtual std::string decision_procedure_text() const
+  decision_proceduret::resultt dec_solve() override;
+
+  std::string decision_procedure_text() const override
   {
     return "refinement loop with "+prop.solver_text();
   }
 
-  // NOLINTNEXTLINE(readability/identifiers)
-  typedef bv_pointerst SUB;
-
-  // maximal number of times we refine a formula node
-  unsigned max_node_refinement;
-  // enable/disable refinements
-  bool do_array_refinement;
-  bool do_arithmetic_refinement;
+protected:
 
-  using bv_pointerst::is_in_conflict;
+  // Refine array
+  void post_process_arrays() override;
 
-  void set_ui(language_uit::uit _ui) { ui=_ui; }
+  // Refine arithmetic
+  bvt convert_mult(const exprt &expr) override;
+  bvt convert_div(const div_exprt &expr) override;
+  bvt convert_mod(const mod_exprt &expr) override;
+  bvt convert_floatbv_op(const exprt &expr) override;
 
-protected:
-  resultt prop_solve();
+  void set_assumptions(const bvt &_assumptions) override;
 
+private:
   // the list of operator approximations
-  struct approximationt
+  struct approximationt final
   {
   public:
     explicit approximationt(std::size_t _id_nr):
@@ -79,39 +89,30 @@ class bv_refinementt:public bv_pointerst
     std::size_t id_nr;
   };
 
-  typedef std::list<approximationt> approximationst;
-  approximationst approximations;
-
+  resultt prop_solve();
   approximationt &add_approximation(const exprt &expr, bvt &bv);
+  bool conflicts_with(approximationt &approximation);
   void check_SAT(approximationt &approximation);
   void check_UNSAT(approximationt &approximation);
   void initialize(approximationt &approximation);
   void get_values(approximationt &approximation);
-  bool is_in_conflict(approximationt &approximation);
-
-  virtual void check_SAT();
-  virtual void check_UNSAT();
-  bool progress;
-
-  // we refine the theory of arrays
-  virtual void post_process_arrays();
+  void check_SAT();
+  void check_UNSAT();
   void arrays_overapproximated();
   void freeze_lazy_constraints();
 
-  // we refine expensive arithmetic
-  virtual bvt convert_mult(const exprt &expr);
-  virtual bvt convert_div(const div_exprt &expr);
-  virtual bvt convert_mod(const mod_exprt &expr);
-  virtual bvt convert_floatbv_op(const exprt &expr);
-
-  // for collecting statistics
-  virtual void set_to(const exprt &expr, bool value);
-
-  // overloading
-  virtual void set_assumptions(const bvt &_assumptions);
+  // MEMBERS
 
+  // Maximum number of times we refine a formula node
+  const unsigned max_node_refinement;
+  // Refinement toggles
+  const bool do_array_refinement;
+  const bool do_arithmetic_refinement;
+  bool progress;
+  std::vector<approximationt> approximations;
   bvt parent_assumptions;
 
+protected:
   // use gui format
   language_uit::uit ui;
 };

src/solvers/refinement/bv_refinement_loop.cpp

@@ -12,25 +12,20 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/xml.h>
 
-bv_refinementt::bv_refinementt(
-  const namespacet &_ns, propt &_prop):
-  bv_pointerst(_ns, _prop),
-  max_node_refinement(5),
-  do_array_refinement(true),
-  do_arithmetic_refinement(true),
+bv_refinementt::bv_refinementt(const infot &info):
+  bv_pointerst(*info.ns, *info.prop),
+  max_node_refinement(info.max_node_refinement),
+  do_array_refinement(info.refine_arrays),
+  do_arithmetic_refinement(info.refine_arithmetic),
   progress(false),
-  ui(ui_message_handlert::uit::PLAIN)
+  ui(info.ui)
 {
   // check features we need
   PRECONDITION(prop.has_set_assumptions());
   PRECONDITION(prop.has_set_to());
   PRECONDITION(prop.has_is_in_conflict());
 }
 
-bv_refinementt::~bv_refinementt()
-{
-}
-
 decision_proceduret::resultt bv_refinementt::dec_solve()
 {
   // do the usual post-processing
@@ -96,17 +91,16 @@ decision_proceduret::resultt bv_refinementt::prop_solve()
   // this puts the underapproximations into effect
   bvt assumptions=parent_assumptions;
 
-  for(approximationst::const_iterator
-      a_it=approximations.begin();
-      a_it!=approximations.end();
-      a_it++)
+  for(const approximationt &approximation : approximations)
   {
     assumptions.insert(
       assumptions.end(),
-      a_it->over_assumptions.begin(), a_it->over_assumptions.end());
+      approximation.over_assumptions.begin(),
+      approximation.over_assumptions.end());
     assumptions.insert(
       assumptions.end(),
-      a_it->under_assumptions.begin(), a_it->under_assumptions.end());
+      approximation.under_assumptions.begin(),
+      approximation.under_assumptions.end());
   }
 
   prop.set_assumptions(assumptions);
@@ -127,40 +121,16 @@ void bv_refinementt::check_SAT()
 
   arrays_overapproximated();
 
-  for(approximationst::iterator
-      a_it=approximations.begin();
-      a_it!=approximations.end();
-      a_it++)
-    check_SAT(*a_it);
+  for(approximationt &approximation : this->approximations)
+    check_SAT(approximation);
 }
 
 void bv_refinementt::check_UNSAT()
 {
   progress=false;
 
-  for(approximationst::iterator
-      a_it=approximations.begin();
-      a_it!=approximations.end();
-      a_it++)
-    check_UNSAT(*a_it);
-}
-
-void bv_refinementt::set_to(const exprt &expr, bool value)
-{
-  #if 0
-  unsigned prev=prop.no_variables();
-  SUB::set_to(expr, value);
-  unsigned n=prop.no_variables()-prev;
-  std::cout << n << " EEE " << expr.id() << "@" << expr.type().id();
-  forall_operands(it, expr)
-    std::cout << " " << it->id() << "@" << it->type().id();
-  if(expr.id()=="=" && expr.operands().size()==2)
-    forall_operands(it, expr.op1())
-      std::cout << " " << it->id() << "@" << it->type().id();
-  std::cout << '\n';
-  #else
-  SUB::set_to(expr, value);
-  #endif
+  for(approximationt &approximation : this->approximations)
+    check_UNSAT(approximation);
 }
 
 void bv_refinementt::set_assumptions(const bvt &_assumptions)

src/solvers/refinement/refine_arithmetic.cpp

@@ -373,7 +373,7 @@ void bv_refinementt::check_SAT(approximationt &a)
 void bv_refinementt::check_UNSAT(approximationt &a)
 {
   // part of the conflict?
-  if(!is_in_conflict(a))
+  if(!this->conflicts_with(a))
     return;
 
   status() << "Found assumption for `" << a.as_string()
@@ -458,7 +458,7 @@ void bv_refinementt::check_UNSAT(approximationt &a)
 }
 
 /// check if an under-approximation is part of the conflict
-bool bv_refinementt::is_in_conflict(approximationt &a)
+bool bv_refinementt::conflicts_with(approximationt &a)
 {
   for(std::size_t i=0; i<a.under_assumptions.size(); i++)
     if(prop.is_in_conflict(a.under_assumptions[i]))

src/solvers/refinement/string_constraint.h

@@ -144,7 +144,7 @@ extern inline string_constraintt &to_string_constraint(exprt &expr)
 /// \param [in] identifier: identifier for `from_expr`
 /// \param [in] expr: constraint to render
 /// \return rendered string
-inline static std::string from_expr(
+inline std::string from_expr(
   const namespacet &ns,
   const irep_idt &identifier,
   const string_constraintt &expr)
@@ -218,7 +218,7 @@ class string_not_contains_constraintt: public exprt
 /// \param [in] identifier: identifier for `from_expr`
 /// \param [in] expr: constraint to render
 /// \return rendered string
-inline static std::string from_expr(
+inline std::string from_expr(
   const namespacet &ns,
   const irep_idt &identifier,
   const string_not_contains_constraintt &expr)