Merge pull request #1404 from LAJW/string-refinement-functional

TG-634 Functional style for string refinement

Author: Thomas Kiley

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,11 +41,11 @@ 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);
-      std::cout << xml << '\n';
+      status() << xml << '\n';
     }
 
     switch(prop_solve())

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_constraint_generator.h

@@ -40,14 +40,13 @@ class string_constraint_generatort final
   /// Arguments pack for the string_constraint_generator constructor
   struct infot
   {
-    const namespacet *ns=nullptr;
     /// Max length of non-deterministic strings
     size_t string_max_length=std::numeric_limits<size_t>::max();
     /// Prefer printable characters in non-deterministic strings
     bool string_printable=false;
   };
 
-  explicit string_constraint_generatort(const infot& info);
+  string_constraint_generatort(const infot& info, const namespacet& ns);
 
   /// Axioms are of three kinds: universally quantified string constraint,
   /// not contains string constraints and simple formulas.
@@ -81,6 +80,11 @@ class string_constraint_generatort final
 
   symbol_exprt fresh_exist_index(const irep_idt &prefix, const typet &type);
 
+  /// remove functions applications and create the necessary axioms
+  /// \par parameters: an expression containing function applications
+  /// \return an expression containing no function application
+  exprt substitute_function_applications(const exprt& expr);
+
 private:
   symbol_exprt fresh_boolean(const irep_idt &prefix);
   string_exprt fresh_string(const refined_string_typet &type);

src/solvers/refinement/string_constraint_generator_main.cpp

@@ -28,10 +28,10 @@ Author: Romain Brenguier, [email protected]
 #include <util/ssa_expr.h>
 
 string_constraint_generatort::string_constraint_generatort(
-  const string_constraint_generatort::infot& info):
+  const string_constraint_generatort::infot& info, const namespacet& ns):
   max_string_length(info.string_max_length),
   m_force_printable_characters(info.string_printable),
-  m_ns(*info.ns) { }
+  m_ns(ns) { }
 
 const std::vector<exprt> &string_constraint_generatort::get_axioms() const
 {
@@ -628,3 +628,19 @@ exprt string_constraint_generatort::add_axioms_for_to_char_array(
   string_exprt str=get_string_expr(args(f, 1)[0]);
   return str.content();
 }
+
+exprt string_constraint_generatort::substitute_function_applications(
+  const exprt &expr)
+{
+  exprt copy=expr;
+  for(exprt &operand : copy.operands())
+    operand=substitute_function_applications(exprt(operand));
+
+  if(copy.id()==ID_function_application)
+  {
+    function_application_exprt f=to_function_application_expr(copy);
+    return this->add_axioms_for_function_application(f);
+  }
+
+  return copy;
+}