usage of format() instead of from_expr for debugging

Author: Daniel Kroening

src/solvers/flattening/arrays.cpp

@@ -402,10 +402,8 @@ void arrayst::update_index_map(bool update_all)
     for(const auto &index : index_entry.second)
       std::cout << "Index set (" << index_entry.first << " = "
                 << arrays.find_number(index_entry.first) << " = "
-                << from_expr(ns, "",
-                             arrays[arrays.find_number(index_entry.first)])
-                << "): "
-                << from_expr(ns, "", index) << '\n';
+                << format(arrays[arrays.find_number(index_entry.first)])
+                << "): " << format(index) << '\n';
   std::cout << "-----\n";
 #endif
 }

src/solvers/refinement/string_constraint.h

@@ -20,11 +20,11 @@ Author: Romain Brenguier, [email protected]
 #ifndef CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_H
 #define CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_H
 
-#include <solvers/refinement/bv_refinement.h>
-#include <solvers/refinement/string_refinement_invariant.h>
+#include "bv_refinement.h"
+#include "string_refinement_invariant.h"
+
 #include <util/refined_string_type.h>
 #include <util/string_expr.h>
-#include <langapi/language_util.h>
 
 ///  ### Universally quantified string constraint
 ///
@@ -151,11 +151,11 @@ inline std::string from_expr(
   const irep_idt &identifier,
   const string_constraintt &expr)
 {
-  return "forall "+from_expr(ns, identifier, expr.univ_var())+" in ["+
-    from_expr(ns, identifier, expr.lower_bound())+", "+
-    from_expr(ns, identifier, expr.upper_bound())+"). "+
-    from_expr(ns, identifier, expr.premise())+" => "+
-    from_expr(ns, identifier, expr.body());
+  std::ostringstream out;
+  out << "forall " << format(expr.univ_var()) << " in ["
+      << format(expr.lower_bound()) << ", " << format(expr.upper_bound())
+      << "). " << format(expr.premise()) << " => " << format(expr.body());
+  return out.str();
 }
 
 /// Constraints to encode non containement of strings.
@@ -226,14 +226,14 @@ inline std::string from_expr(
   const irep_idt &identifier,
   const string_not_contains_constraintt &expr)
 {
-  return "forall x in ["+
-    from_expr(ns, identifier, expr.univ_lower_bound())+", "+
-    from_expr(ns, identifier, expr.univ_upper_bound())+"). "+
-    from_expr(ns, identifier, expr.premise())+" => ("+
-    "exists y in ["+from_expr(ns, identifier, expr.exists_lower_bound())+", "+
-    from_expr(ns, identifier, expr.exists_upper_bound())+"). "+
-    from_expr(ns, identifier, expr.s0())+"[x+y] != "+
-    from_expr(ns, identifier, expr.s1())+"[y])";
+  std::ostringstream out;
+  out << "forall x in [" << format(expr.univ_lower_bound()) << ", "
+      << format(expr.univ_upper_bound()) << "). " << format(expr.premise())
+      << " => ("
+      << "exists y in [" << format(expr.exists_lower_bound()) << ", "
+      << format(expr.exists_upper_bound()) << "). " << format(expr.s0())
+      << "[x+y] != " << format(expr.s1()) << "[y])";
+  return out.str();
 }
 
 inline const string_not_contains_constraintt