Merge pull request #1163 from romainbrenguier/feature/string-solver-debug-info

Debug information in string solver

Author: romainbrenguier

src/solvers/refinement/string_refinement.cpp

@@ -826,35 +826,35 @@ std::string string_refinementt::string_of_array(const array_exprt &arr)
   return result.str();
 }
 
-/// Fill in `current_model` by mapping the variables created by the solver to
-/// constant expressions given by the current model
-void string_refinementt::fill_model()
+/// Display part of the current model by mapping the variables created by the
+/// solver to constant expressions given by the current model
+void string_refinementt::debug_model()
 {
+  const std::string indent("  ");
   for(auto it : symbol_resolve)
   {
     if(refined_string_typet::is_refined_string_type(it.second.type()))
     {
+      debug() << "- " << from_expr(ns, "", to_symbol_expr(it.first)) << ":\n";
       string_exprt refined=to_string_expr(it.second);
-      // TODO: check whith this is necessary:
-      replace_expr(symbol_resolve, refined);
+      debug() << indent << indent << "in_map: "
+              << from_expr(ns, "", refined) << eom;
+      debug() << indent << indent << "resolved: "
+              << from_expr(ns, "", refined) << eom;
       const exprt &econtent=refined.content();
       const exprt &elength=refined.length();
 
       exprt len=supert::get(elength);
       len=simplify_expr(len, ns);
       exprt arr=get_array(econtent, len);
-
-      current_model[elength]=len;
-      current_model[econtent]=arr;
-      debug() << from_expr(ns, "", to_symbol_expr(it.first)) << "="
-              << from_expr(ns, "", refined);
-
       if(arr.id()==ID_array)
-        debug() << " = \"" << string_of_array(to_array_expr(arr))
-                << "\" (size:" << from_expr(ns, "", len) << ")"<< eom;
+        debug() << indent << indent << "as_string: \""
+                << string_of_array(to_array_expr(arr)) << "\"\n";
       else
-        debug() << " = " << from_expr(ns, "", arr)
-                << " (size:" << from_expr(ns, "", len) << ")" << eom;
+        debug() << indent << indent << "as_char_array: "
+                << from_expr(ns, "", arr) << "\n";
+
+      debug() << indent << indent << "size: " << from_expr(ns, "", len) << eom;
     }
     else
     {
@@ -865,32 +865,28 @@ void string_refinementt::fill_model()
           "handled"));
       exprt arr=it.second;
       replace_expr(symbol_resolve, arr);
-      replace_expr(current_model, arr);
+      debug() << "- " << from_expr(ns, "", to_symbol_expr(it.first)) << ":\n";
+      debug() << indent << indent << "resolved: "
+              << from_expr(ns, "", arr) << "\n";
       exprt arr_model=get_array(arr);
-      current_model[it.first]=arr_model;
-
-      debug() << from_expr(ns, "", to_symbol_expr(it.first)) << "="
-              << from_expr(ns, "", arr) << " = "
-              << from_expr(ns, "", arr_model) << "" << eom;
+      debug() << indent << indent << "char_array: "
+              << from_expr(ns, "", arr_model) << eom;
     }
   }
 
   for(auto it : generator.boolean_symbols)
   {
-      debug() << "" << it.get_identifier() << " := "
+      debug() << " - " << it.get_identifier() << ": "
               << from_expr(ns, "", supert::get(it)) << eom;
-      current_model[it]=supert::get(it);
   }
 
   for(auto it : generator.index_symbols)
   {
-     debug() << "" << it.get_identifier() << " := "
-              << from_expr(ns, "", supert::get(it)) << eom;
-     current_model[it]=supert::get(it);
+     debug() << " - " << it.get_identifier() << ": "
+             << from_expr(ns, "", supert::get(it)) << eom;
   }
 }
 
-
 /// Create a new expression where 'with' expressions on arrays are replaced by
 /// 'if' expressions. e.g. for an array access arr[x], where: `arr :=
 /// array_of(12) with {0:=24} with {2:=42}` the constructed expression will be:
@@ -1125,7 +1121,7 @@ bool string_refinementt::check_axioms()
           << "===========================================" << eom;
   debug() << "string_refinementt::check_axioms: build the"
           << " interpretation from the model of the prop_solver" << eom;
-  fill_model();
+  debug_model();
 
   // Maps from indexes of violated universal axiom to a witness of violation
   std::map<size_t, exprt> violated;

src/solvers/refinement/string_refinement.h

@@ -94,10 +94,6 @@ class string_refinementt: public bv_refinementt
   std::map<exprt, exprt_listt> reverse_symbol_resolve;
   std::list<std::pair<exprt, bool>> non_string_axioms;
 
-  // Valuation in the current model of the symbols that have been created
-  // by the solver
-  replace_mapt current_model;
-
   // Length of char arrays found during concretization
   std::map<exprt, exprt> found_length;
   // Content of char arrays found during concretization
@@ -127,7 +123,7 @@ class string_refinementt: public bv_refinementt
     const exprt &val,
     const symbol_exprt &univ_var);
   exprt negation_of_constraint(const string_constraintt &axiom);
-  void fill_model();
+  void debug_model();
   bool check_axioms();
   bool is_axiom_sat(
     const exprt &axiom, const symbol_exprt& var, exprt &witness);