Merge pull request diffblue#1893 from diffblue/expression-printer

Expression printer

Author: Daniel Kroening

src/solvers/flattening/arrays.cpp

@@ -8,13 +8,12 @@ Author: Daniel Kroening, [email protected]
 
 #include "arrays.h"
 
-#include <langapi/language_util.h>
-
-#include <util/std_expr.h>
-#include <util/std_types.h>
 #include <util/arith_tools.h>
 #include <util/base_type.h>
+#include <util/format_expr.h>
 #include <util/namespace.h>
+#include <util/std_expr.h>
+#include <util/std_types.h>
 
 #include <solvers/prop/prop.h>
 
@@ -402,10 +401,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/flattening/boolbv_equality.cpp

@@ -13,8 +13,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/std_expr.h>
 #include <util/base_type.h>
 
-#include <langapi/language_util.h>
-
 #include "flatten_byte_operators.h"
 
 literalt boolbvt::convert_equality(const equal_exprt &expr)

src/solvers/prop/bdd_expr.cpp

@@ -11,10 +11,11 @@ Author: Michael Tautschnig, [email protected]
 
 #include "bdd_expr.h"
 
-#include <langapi/language_util.h>
-
 #include <util/std_expr.h>
 #include <util/expr_util.h>
+#include <util/format_expr.h>
+
+#include <sstream>
 
 mini_bddt bdd_exprt::from_expr_rec(const exprt &expr)
 {
@@ -83,8 +84,9 @@ mini_bddt bdd_exprt::from_expr_rec(const exprt &expr)
 
     if(entry.second)
     {
-      std::string s=::from_expr(ns, "", expr);
-      entry.first->second=bdd_mgr.Var(s);
+      std::ostringstream s;
+      s << format(expr);
+      entry.first->second=bdd_mgr.Var(s.str());
 
       node_map.insert(std::make_pair(entry.first->second.var(),
                                      expr));

src/solvers/qbf/qbf_bdd_core.cpp

@@ -14,8 +14,6 @@ Author: CM Wintersteiger
 #include <util/arith_tools.h>
 #include <util/std_expr.h>
 
-#include <langapi/language_util.h>
-
 #include <cuddObj.hh> // CUDD Library
 
 /*! \cond */

src/solvers/refinement/refine_arrays.cpp

@@ -10,7 +10,6 @@ Author: Daniel Kroening, [email protected]
 
 #ifdef DEBUG
 #include <iostream>
-#include <langapi/language_util.h>
 #endif
 
 #include <util/std_expr.h>

src/solvers/refinement/string_constraint.h

@@ -20,11 +20,13 @@ 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/format_expr.h>
+#include <util/format_type.h>
 #include <util/refined_string_type.h>
 #include <util/string_expr.h>
-#include <langapi/language_util.h>
 
 ///  ### Universally quantified string constraint
 ///
@@ -147,15 +149,14 @@ extern inline string_constraintt &to_string_constraint(exprt &expr)
 /// \param [in] expr: constraint to render
 /// \return rendered string
 inline std::string from_expr(
-  const namespacet &ns,
   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.
@@ -222,18 +223,17 @@ class string_not_contains_constraintt: public exprt
 /// \param [in] expr: constraint to render
 /// \return rendered string
 inline std::string from_expr(
-  const namespacet &ns,
   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