Group bv_refinement config variables

Author: Lukasz A.J. Wrona

src/solvers/refinement/bv_refinement.h

@@ -20,11 +20,9 @@ Author: Daniel Kroening, [email protected]
 
 class bv_refinementt:public bv_pointerst
 {
-public:
-  struct infot
+private:
+  struct configt
   {
-    const namespacet *ns=nullptr;
-    propt *prop=nullptr;
     ui_message_handlert::uit ui=ui_message_handlert::uit::PLAIN;
     /// Max number of times we refine a formula node
     unsigned max_node_refinement=5;
@@ -33,6 +31,12 @@ class bv_refinementt:public bv_pointerst
     /// Enable arithmetic refinement
     bool refine_arithmetic=true;
   };
+public:
+  struct infot : public configt
+  {
+    const namespacet *ns=nullptr;
+    propt *prop=nullptr;
+  };
 
   explicit bv_refinementt(const infot &info);
 
@@ -103,18 +107,12 @@ class bv_refinementt:public bv_pointerst
 
   // 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
-  ui_message_handlert::uit ui;
+  configt config_;
 };
 
 #endif // CPROVER_SOLVERS_REFINEMENT_BV_REFINEMENT_H

src/solvers/refinement/bv_refinement_loop.cpp

@@ -14,11 +14,8 @@ Author: Daniel Kroening, [email protected]
 
 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(info.ui)
+  config_(info)
 {
   // check features we need
   PRECONDITION(prop.has_set_assumptions());
@@ -44,7 +41,7 @@ decision_proceduret::resultt bv_refinementt::dec_solve()
     status() << "BV-Refinement: iteration " << iteration << eom;
 
     // output the very same information in a structured fashion
-    if(ui==ui_message_handlert::uit::XML_UI)
+    if(config_.ui==ui_message_handlert::uit::XML_UI)
     {
       xmlt xml("refinement-iteration");
       xml.data=std::to_string(iteration);

src/solvers/refinement/refine_arithmetic.cpp

@@ -38,7 +38,7 @@ void bv_refinementt::approximationt::add_under_assumption(literalt l)
 
 bvt bv_refinementt::convert_floatbv_op(const exprt &expr)
 {
-  if(!do_arithmetic_refinement)
+  if(!config_.refine_arithmetic)
     return SUB::convert_floatbv_op(expr);
 
   if(ns.follow(expr.type()).id()!=ID_floatbv ||
@@ -52,7 +52,7 @@ bvt bv_refinementt::convert_floatbv_op(const exprt &expr)
 
 bvt bv_refinementt::convert_mult(const exprt &expr)
 {
-  if(!do_arithmetic_refinement || expr.type().id()==ID_fixedbv)
+  if(!config_.refine_arithmetic || expr.type().id()==ID_fixedbv)
     return SUB::convert_mult(expr);
 
   // we catch any multiplication
@@ -100,7 +100,7 @@ bvt bv_refinementt::convert_mult(const exprt &expr)
 
 bvt bv_refinementt::convert_div(const div_exprt &expr)
 {
-  if(!do_arithmetic_refinement || expr.type().id()==ID_fixedbv)
+  if(!config_.refine_arithmetic || expr.type().id()==ID_fixedbv)
     return SUB::convert_div(expr);
 
   // we catch any division
@@ -118,7 +118,7 @@ bvt bv_refinementt::convert_div(const div_exprt &expr)
 
 bvt bv_refinementt::convert_mod(const mod_exprt &expr)
 {
-  if(!do_arithmetic_refinement || expr.type().id()==ID_fixedbv)
+  if(!config_.refine_arithmetic || expr.type().id()==ID_fixedbv)
     return SUB::convert_mod(expr);
 
   // we catch any mod
@@ -228,7 +228,7 @@ void bv_refinementt::check_SAT(approximationt &a)
 
     // if(a.over_state==1) { debug() << "DISAGREEMENT!\n"; exit(1); }
 
-    if(a.over_state<max_node_refinement)
+    if(a.over_state<config_.max_node_refinement)
     {
       bvt r;
       float_utilst float_utils(prop);

src/solvers/refinement/refine_arrays.cpp

@@ -29,15 +29,15 @@ void bv_refinementt::post_process_arrays()
   update_index_map(true);
 
   // we don't actually add any constraints
-  lazy_arrays=do_array_refinement;
+  lazy_arrays=config_.refine_arrays;
   add_array_constraints();
   freeze_lazy_constraints();
 }
 
 /// check whether counterexample is spurious
 void bv_refinementt::arrays_overapproximated()
 {
-  if(!do_array_refinement)
+  if(!config_.refine_arrays)
     return;
 
   unsigned nb_active=0;

src/solvers/refinement/string_refinement.cpp

@@ -86,19 +86,6 @@ static bool validate(const string_refinementt::infot &info)
   return true;
 }
 
-static bv_refinementt::infot bv_refinement_info(
-  const string_refinementt::infot &in)
-{
-  bv_refinementt::infot out;
-  out.ns=in.ns;
-  out.prop=in.prop;
-  out.ui=in.ui;
-  out.max_node_refinement=in.max_node_refinement;
-  out.refine_arrays=in.refine_arrays;
-  out.refine_arithmetic=in.refine_arithmetic;
-  return out;
-}
-
 static string_constraint_generatort::infot
 generator_info(const string_refinementt::infot &in)
 {
@@ -110,7 +97,7 @@ generator_info(const string_refinementt::infot &in)
 }
 
 string_refinementt::string_refinementt(const infot &info, bool):
-  supert(bv_refinement_info(info)),
+  supert(info),
   use_counter_example(false),
   do_concretizing(info.trace),
   initial_loop_bound(info.refinement_bound),
@@ -1770,7 +1757,7 @@ bool string_refinementt::is_axiom_sat(
   info.refine_arithmetic=true;
   info.refine_arrays=true;
   info.max_node_refinement=5;
-  info.ui=ui;
+  info.ui=config_.ui;
   supert solver(info);
   solver << axiom;
 

src/solvers/refinement/string_refinement.h

@@ -31,13 +31,8 @@ Author: Alberto Griggio, [email protected]
 
 class string_refinementt final: public bv_refinementt
 {
-public:
-  /// string_refinementt constructor arguments
-  struct infot
-  {
-    const namespacet *ns=nullptr;
-    propt *prop=nullptr;
-    ui_message_handlert::uit ui=ui_message_handlert::uit::PLAIN;
+private:
+  struct configt {
     unsigned refinement_bound=0;
     size_t string_max_length=std::numeric_limits<size_t>::max();
     /// Make non-deterministic character arrays have at least one character
@@ -46,11 +41,11 @@ class string_refinementt final: public bv_refinementt
     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;
     bool use_counter_example=false;
   };
+public:
+  /// string_refinementt constructor arguments
+  struct infot:public bv_refinementt::infot, public configt { };
 
   explicit string_refinementt(const infot &);