diff --git a/src/solvers/flattening/arrays.cpp b/src/solvers/flattening/arrays.cpp
index 8a1fcfc328c..b48f4c65647 100644
--- a/src/solvers/flattening/arrays.cpp
+++ b/src/solvers/flattening/arrays.cpp
@@ -8,13 +8,12 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #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
 }
diff --git a/src/solvers/flattening/boolbv_equality.cpp b/src/solvers/flattening/boolbv_equality.cpp
index 95a379a5a95..999ec51b967 100644
--- a/src/solvers/flattening/boolbv_equality.cpp
+++ b/src/solvers/flattening/boolbv_equality.cpp
@@ -13,8 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #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)
diff --git a/src/solvers/prop/bdd_expr.cpp b/src/solvers/prop/bdd_expr.cpp
index 01dacc19048..8d612cef860 100644
--- a/src/solvers/prop/bdd_expr.cpp
+++ b/src/solvers/prop/bdd_expr.cpp
@@ -11,10 +11,11 @@ Author: Michael Tautschnig, michael.tautschnig@qmul.ac.uk
 
 #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));
diff --git a/src/solvers/qbf/qbf_bdd_core.cpp b/src/solvers/qbf/qbf_bdd_core.cpp
index 16bdf676ee2..da4b0013461 100644
--- a/src/solvers/qbf/qbf_bdd_core.cpp
+++ b/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 */
diff --git a/src/solvers/refinement/refine_arrays.cpp b/src/solvers/refinement/refine_arrays.cpp
index 31506bd5dd7..144f42b53d5 100644
--- a/src/solvers/refinement/refine_arrays.cpp
+++ b/src/solvers/refinement/refine_arrays.cpp
@@ -10,7 +10,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #ifdef DEBUG
 #include <iostream>
-#include <langapi/language_util.h>
 #endif
 
 #include <util/std_expr.h>
diff --git a/src/solvers/refinement/string_constraint.h b/src/solvers/refinement/string_constraint.h
index 1066235b61e..7e804ec6e13 100644
--- a/src/solvers/refinement/string_constraint.h
+++ b/src/solvers/refinement/string_constraint.h
@@ -20,11 +20,13 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 #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
diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index 20ff4a5c5da..050cc438c59 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -179,7 +179,6 @@ string_refinementt::string_refinementt(const infot &info):
 /// Write index set to the given stream, use for debugging
 static void display_index_set(
   messaget::mstreamt &stream,
-  const namespacet &ns,
   const index_set_pairt &index_set)
 {
   const auto eom=messaget::eom;
@@ -188,7 +187,7 @@ static void display_index_set(
   for(const auto &i : index_set.cumulative)
   {
     const exprt &s=i.first;
-    stream << "IS(" << from_expr(ns, "", s) << ")=={" << eom;
+    stream << "IS(" << format(s) << ")=={" << eom;
 
     for(const auto &j : i.second)
     {
@@ -198,7 +197,7 @@ static void display_index_set(
         count_current++;
         stream << "**";
       }
-      stream << "  " << from_expr(ns, "", j) << ";" << eom;
+      stream << "  " << format(j) << ";" << eom;
       count++;
     }
     stream << "}"  << eom;
@@ -436,16 +435,15 @@ static union_find_replacet generate_symbol_resolution_from_equations(
     const exprt &rhs = eq.rhs();
     if(lhs.id()!=ID_symbol)
     {
-      stream << log_message << "non symbol lhs: " << from_expr(ns, "", lhs)
-             << " with rhs: " << from_expr(ns, "", rhs) << eom;
+      stream << log_message << "non symbol lhs: " << format(lhs)
+             << " with rhs: " << format(rhs) << eom;
       continue;
     }
 
     if(lhs.type()!=rhs.type())
     {
-      stream << log_message << "non equal types lhs: " << from_expr(ns, "", lhs)
-             << "\n####################### rhs: " << from_expr(ns, "", rhs)
-             << eom;
+      stream << log_message << "non equal types lhs: " << format(lhs)
+             << "\n####################### rhs: " << format(rhs) << eom;
       continue;
     }
 
@@ -478,8 +476,7 @@ static union_find_replacet generate_symbol_resolution_from_equations(
       else
       {
         stream << log_message << "non struct with char pointer subexpr "
-               << from_expr(ns, "", rhs) << "\n  * of type "
-               << from_type(ns, "", rhs.type()) << eom;
+               << format(rhs) << "\n  * of type " << format(rhs.type()) << eom;
       }
     }
   }
@@ -643,8 +640,8 @@ union_find_replacet string_identifiers_resolution_from_equations(
       if(lhs_strings.empty())
       {
         stream << log_message << "non struct with string subtype "
-               << from_expr(ns, "", eq.lhs()) << "\n  * of type "
-               << from_type(ns, "", eq.lhs().type()) << eom;
+               << format(eq.lhs()) << "\n  * of type "
+               << format(eq.lhs().type()) << eom;
       }
 
       for(const exprt &expr : extract_strings(eq.rhs()))
@@ -681,8 +678,8 @@ void output_equations(
   const namespacet &ns)
 {
   for(std::size_t i = 0; i < equations.size(); ++i)
-    output << "  [" << i << "] " << from_expr(ns, "", equations[i].lhs())
-           << " == " << from_expr(ns, "", equations[i].rhs()) << std::endl;
+    output << "  [" << i << "] " << format(equations[i].lhs())
+           << " == " << format(equations[i].rhs()) << std::endl;
 }
 
 /// Main decision procedure of the solver. Looks for a valuation of variables
@@ -763,8 +760,7 @@ decision_proceduret::resultt string_refinementt::dec_solve()
 #ifdef DEBUG
   debug() << "symbol resolve:" << eom;
   for(const auto &pair : symbol_resolve.to_vector())
-    debug() << from_expr(ns, "", pair.first) << " --> "
-            << from_expr(ns, "", pair.second) << eom;
+    debug() << format(pair.first) << " --> " << format(pair.second) << eom;
 #endif
 
   const union_find_replacet string_id_symbol_resolve =
@@ -773,8 +769,7 @@ decision_proceduret::resultt string_refinementt::dec_solve()
   debug() << "symbol resolve string:" << eom;
   for(const auto &pair : string_id_symbol_resolve.to_vector())
   {
-    debug() << from_expr(ns, "", pair.first) << " --> "
-            << from_expr(ns, "", pair.second) << eom;
+    debug() << format(pair.first) << " --> " << format(pair.second) << eom;
   }
 #endif
 
@@ -803,16 +798,15 @@ decision_proceduret::resultt string_refinementt::dec_solve()
   debug() << "dec_solve: arrays_of_pointers:" << eom;
   for(auto pair : generator.get_arrays_of_pointers())
   {
-    debug() << "  * " << from_expr(ns, "", pair.first) << "\t--> "
-            << from_expr(ns, "", pair.second) << " : "
-            << from_type(ns, "", pair.second.type()) << eom;
+    debug() << "  * " << format(pair.first) << "\t--> " << format(pair.second)
+            << " : " << format(pair.second.type()) << eom;
   }
 #endif
 
   for(const auto &eq : equations)
   {
 #ifdef DEBUG
-    debug() << "dec_solve: set_to " << from_expr(ns, "", eq) << eom;
+    debug() << "dec_solve: set_to " << format(eq) << eom;
 #endif
     supert::set_to(eq, true);
   }
@@ -944,7 +938,7 @@ decision_proceduret::resultt string_refinementt::dec_solve()
       index_sets.current.clear();
       update_index_set(index_sets, ns, current_constraints);
 
-      display_index_set(debug(), ns, index_sets);
+      display_index_set(debug(), index_sets);
 
       if(index_sets.current.empty())
       {
@@ -1020,7 +1014,7 @@ void string_refinementt::add_lemma(
       ++it;
   }
 
-  debug() << "adding lemma " << from_expr(ns, "", simple_lemma) << eom;
+  debug() << "adding lemma " << format(simple_lemma) << eom;
 
   prop.l_set_to_true(convert(simple_lemma));
 }
@@ -1053,8 +1047,8 @@ static optionalt<exprt> get_array(
 
   if(size_val.id()!=ID_constant)
   {
-    stream << "(sr::get_array) string of unknown size: "
-           << from_expr(ns, "", size_val) << eom;
+    stream << "(sr::get_array) string of unknown size: " << format(size_val)
+           << eom;
     return {};
   }
 
@@ -1143,22 +1137,21 @@ static exprt get_char_array_and_concretize(
 {
   const auto &eom = messaget::eom;
   static const std::string indent("  ");
-  stream << "- " << from_expr(ns, "", arr) << ":\n";
-  stream << indent << indent << "- type: " << from_type(ns, "", arr.type())
-         << eom;
+  stream << "- " << format(arr) << ":\n";
+  stream << indent << indent << "- type: " << format(arr.type()) << eom;
   const auto arr_model_opt =
     get_array(super_get, ns, max_string_length, stream, arr);
   if(arr_model_opt)
   {
-    stream << indent << indent
-           << "- char_array: " << from_expr(ns, "", *arr_model_opt) << eom;
+    stream << indent << indent << "- char_array: " << format(*arr_model_opt)
+           << eom;
     const exprt simple = simplify_expr(*arr_model_opt, ns);
-    stream << indent << indent
-           << "- simplified_char_array: " << from_expr(ns, "", simple) << eom;
+    stream << indent << indent << "- simplified_char_array: " << format(simple)
+           << eom;
     const exprt concretized_array =
       concretize_arrays_in_expression(simple, max_string_length, ns);
-    stream << indent << indent << "- concretized_char_array: "
-           << from_expr(ns, "", concretized_array) << eom;
+    stream << indent << indent
+           << "- concretized_char_array: " << format(concretized_array) << eom;
 
     if(concretized_array.id() == ID_array)
     {
@@ -1170,8 +1163,8 @@ static exprt get_char_array_and_concretize(
       stream << indent << "- warning: not an array" << eom;
     }
 
-    stream << indent << indent
-           << "- type: " << from_type(ns, "", concretized_array.type()) << eom;
+    stream << indent << indent << "- type: " << format(concretized_array.type())
+           << eom;
     return concretized_array;
   }
   else
@@ -1201,23 +1194,21 @@ void debug_model(
     const exprt model = get_char_array_and_concretize(
       super_get, ns, max_string_length, stream, arr);
 
-    stream << "- " << from_expr(ns, "", arr) << ":\n"
-           << indent << "- pointer: " << from_expr(ns, "", pointer_array.first)
-           << "\n"
-           << indent << "- model: " << from_expr(ns, "", model)
-           << messaget::eom;
+    stream << "- " << format(arr) << ":\n"
+           << indent << "- pointer: " << format(pointer_array.first) << "\n"
+           << indent << "- model: " << format(model) << messaget::eom;
   }
 
   for(const auto &symbol : boolean_symbols)
   {
     stream << " - " << symbol.get_identifier() << ": "
-           << from_expr(ns, "", super_get(symbol)) << '\n';
+           << format(super_get(symbol)) << '\n';
   }
 
   for(const auto &symbol : index_symbols)
   {
     stream << " - " << symbol.get_identifier() << ": "
-           << from_expr(ns, "", super_get(symbol)) << '\n';
+           << format(super_get(symbol)) << '\n';
   }
   stream << messaget::eom;
 }
@@ -1645,27 +1636,25 @@ static void debug_check_axioms_step(
   stream << indent2 << "- axiom:\n" << indent2 << indent;
 
   if(axiom.id() == ID_string_constraint)
-    stream << from_expr(ns, "", to_string_constraint(axiom));
+    stream << format(to_string_constraint(axiom));
   else if(axiom.id() == ID_string_not_contains_constraint)
-    stream << from_expr(ns, "", to_string_not_contains_constraint(axiom));
+    stream << format(to_string_not_contains_constraint(axiom));
   else
-    stream << from_expr(ns, "", axiom);
+    stream << format(axiom);
   stream << '\n' << indent2 << "- axiom_in_model:\n" << indent2 << indent;
 
   if(axiom_in_model.id() == ID_string_constraint)
-    stream << from_expr(ns, "", to_string_constraint(axiom_in_model));
+    stream << format(to_string_constraint(axiom_in_model));
   else if(axiom_in_model.id() == ID_string_not_contains_constraint)
-    stream << from_expr(
-      ns, "", to_string_not_contains_constraint(axiom_in_model));
+    stream << format(to_string_not_contains_constraint(axiom_in_model));
   else
-    stream << from_expr(ns, "", axiom_in_model);
+    stream << format(axiom_in_model);
 
   stream << '\n'
          << indent2 << "- negated_axiom:\n"
-         << indent2 << indent << from_expr(ns, "", negaxiom) << '\n';
+         << indent2 << indent << format(negaxiom) << '\n';
   stream << indent2 << "- negated_axiom_with_concretized_arrays:\n"
-         << indent2 << indent << from_expr(ns, "", with_concretized_arrays)
-         << '\n';
+         << indent2 << indent << format(with_concretized_arrays) << '\n';
 }
 
 /// \return true if the current model satisfies all the axioms
@@ -1696,8 +1685,8 @@ static std::pair<bool, std::vector<exprt>> check_axioms(
   stream << "symbol_resolve:" << eom;
   auto pairs = symbol_resolve.to_vector();
   for(const auto &pair : pairs)
-    stream << "  - " << from_expr(ns, "", pair.first) << " --> "
-           << from_expr(ns, "", pair.second) << eom;
+    stream << "  - " << format(pair.first) << " --> " << format(pair.second)
+           << eom;
 
 #ifdef DEBUG
   debug_model(
@@ -1740,7 +1729,7 @@ static std::pair<bool, std::vector<exprt>> check_axioms(
        find_counter_example(ns, ui, with_concretized_arrays, univ_var))
     {
       stream << indent2 << "- violated_for: " << univ_var.get_identifier()
-             << "=" << from_expr(ns, "", *witness) << eom;
+             << "=" << format(*witness) << eom;
       violated[i]=*witness;
     }
     else
@@ -1793,7 +1782,7 @@ static std::pair<bool, std::vector<exprt>> check_axioms(
     if(const auto witness = find_counter_example(ns, ui, negaxiom, univ_var))
     {
       stream << indent2 << "- violated_for: " << univ_var.get_identifier()
-             << "=" << from_expr(ns, "", *witness) << eom;
+             << "=" << format(*witness) << eom;
       violated_not_contains[i]=*witness;
     }
   }
@@ -1830,7 +1819,7 @@ static std::pair<bool, std::vector<exprt>> check_axioms(
         replace_expr(axiom.univ_var(), val, bounds);
         const implies_exprt counter(bounds, instance);
 
-        stream << "  -  " << from_expr(ns, "", counter) << eom;
+        stream << "  -  " << format(counter) << eom;
         lemmas.push_back(counter);
       }
 
@@ -1848,7 +1837,7 @@ static std::pair<bool, std::vector<exprt>> check_axioms(
         const exprt counter=::instantiate_not_contains(
           axiom, indices, generator)[0];
 
-        stream << "    -  " << from_expr(ns, "", counter) << eom;
+        stream << "    -  " << format(counter) << eom;
         lemmas.push_back(counter);
       }
       return { false, lemmas };
@@ -2573,12 +2562,12 @@ static bool is_valid_string_constraint(
   const array_index_mapt premise_indices=gather_indices(expr.premise());
   if(!premise_indices.empty())
   {
-    stream << "Premise has indices: " << from_expr(ns, "", expr) << ", map: {";
+    stream << "Premise has indices: " << format(expr) << ", map: {";
     for(const auto &pair : premise_indices)
     {
-      stream << from_expr(ns, "", pair.first) << ": {";
+      stream << format(pair.first) << ": {";
       for(const auto &i : pair.second)
-        stream << from_expr(ns, "", i) <<  ", ";
+        stream << format(i) << ", ";
     }
     stream << "}}" << eom;
     return false;
@@ -2598,8 +2587,8 @@ static bool is_valid_string_constraint(
       const exprt result=simplify_expr(equals, ns);
       if(result.is_false())
       {
-        stream << "Indices not equal: " << from_expr(ns, "", expr) << ", str: "
-               << from_expr(ns, "", pair.first) << eom;
+        stream << "Indices not equal: " << format(expr)
+               << ", str: " << format(pair.first) << eom;
         return false;
       }
     }
@@ -2607,8 +2596,8 @@ static bool is_valid_string_constraint(
     // Condition 3: f must be linear in the quantified variable
     if(!is_linear_arithmetic_expr(rep, expr.univ_var()))
     {
-      stream << "f is not linear: " << from_expr(ns, "", expr) << ", str: "
-             << from_expr(ns, "", pair.first) << eom;
+      stream << "f is not linear: " << format(expr)
+             << ", str: " << format(pair.first) << eom;
       return false;
     }
 
@@ -2616,8 +2605,7 @@ static bool is_valid_string_constraint(
     // body
     if(!universal_only_in_index(expr))
     {
-      stream << "Universal variable outside of index:"
-             << from_expr(ns, "", expr) << eom;
+      stream << "Universal variable outside of index:" << format(expr) << eom;
       return false;
     }
   }
diff --git a/src/solvers/smt1/smt1_conv.cpp b/src/solvers/smt1/smt1_conv.cpp
index b52c86a5428..38ddf57393d 100644
--- a/src/solvers/smt1/smt1_conv.cpp
+++ b/src/solvers/smt1/smt1_conv.cpp
@@ -25,8 +25,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/std_types.h>
 #include <util/string_constant.h>
 
-#include <langapi/language_util.h>
-
 #include <solvers/flattening/boolbv_width.h>
 #include <solvers/flattening/pointer_logic.h>
 #include <solvers/flattening/flatten_byte_operators.h>
@@ -2765,12 +2763,10 @@ void smt1_convt::set_to(const exprt &expr, bool value)
 
   #if 0
   out << "; CONV: "
-                << from_expr(expr) << "\n";
+                << format(expr) << '\n';
   #endif
 
-  out << ":assumption ; set_to "
-      << (value?"true":"false") << "\n"
-      << " ";
+  out << ":assumption ; set_to " << (value ? "true" : "false") << '\n' << " ";
 
   assert(expr.type().id()==ID_bool);
 
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
index 0a79bfb9f89..03bd1dc736f 100644
--- a/src/solvers/smt2/smt2_conv.cpp
+++ b/src/solvers/smt2/smt2_conv.cpp
@@ -19,6 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/config.h>
 #include <util/expr_util.h>
 #include <util/fixedbv.h>
+#include <util/format_expr.h>
 #include <util/ieee_float.h>
 #include <util/invariant.h>
 #include <util/pointer_offset_size.h>
@@ -27,8 +28,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/string2int.h>
 #include <util/string_constant.h>
 
-#include <langapi/language_util.h>
-
 #include <solvers/flattening/boolbv_width.h>
 #include <solvers/flattening/flatten_byte_operators.h>
 #include <solvers/flattening/c_bit_field_replacement_type.h>
@@ -2079,9 +2078,10 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr)
     }
     else
     {
-      UNEXPECTEDCASE(
-        "TODO typecast2 "+src_type.id_string()+" -> "+
-        dest_type.id_string()+" src == "+from_expr(ns, "", src));
+      std::ostringstream e_str;
+      e_str << src_type.id() << " -> " << dest_type.id()
+            << " src == " << format(src);
+      UNEXPECTEDCASE("TODO typecast2 " + e_str.str());
     }
   }
   else if(dest_type.id()==ID_fixedbv) // to fixedbv
@@ -4087,7 +4087,7 @@ void smt2_convt::set_to(const exprt &expr, bool value)
 
   #if 0
   out << "; CONV: "
-      << from_expr(expr) << "\n";
+      << format(expr) << "\n";
   #endif
 
   out << "; set_to " << (value?"true":"false") << "\n"
diff --git a/src/util/Makefile b/src/util/Makefile
index 2eb5dfebce3..f4a06e1198a 100644
--- a/src/util/Makefile
+++ b/src/util/Makefile
@@ -17,7 +17,9 @@ SRC = arith_tools.cpp \
       find_symbols.cpp \
       fixedbv.cpp \
       format_constant.cpp \
+      format_expr.cpp \
       format_number_range.cpp \
+      format_type.cpp \
       fresh_symbol.cpp \
       get_base_name.cpp \
       get_module.cpp \
diff --git a/src/util/expr.cpp b/src/util/expr.cpp
index d952acd87c8..af2cff9946f 100644
--- a/src/util/expr.cpp
+++ b/src/util/expr.cpp
@@ -9,17 +9,13 @@ Author: Daniel Kroening, kroening@kroening.com
 /// \file
 /// Expression Representation
 
-#include "arith_tools.h"
 #include "expr.h"
 #include "expr_iterator.h"
 #include "fixedbv.h"
 #include "ieee_float.h"
-#include "invariant.h"
-#include "mp_arith.h"
 #include "rational.h"
 #include "rational_tools.h"
 #include "std_expr.h"
-#include "string2int.h"
 
 #include <stack>
 
diff --git a/src/util/expr.h b/src/util/expr.h
index ba64a3ce220..9e18d0a0c18 100644
--- a/src/util/expr.h
+++ b/src/util/expr.h
@@ -6,13 +6,12 @@ Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
-
 #ifndef CPROVER_UTIL_EXPR_H
 #define CPROVER_UTIL_EXPR_H
 
-#include <functional>
 #include "type.h"
 
+#include <functional>
 #include <list>
 
 #define forall_operands(it, expr) \
diff --git a/src/util/format.h b/src/util/format.h
new file mode 100644
index 00000000000..b73ea358835
--- /dev/null
+++ b/src/util/format.h
@@ -0,0 +1,40 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_UTIL_FORMAT_H
+#define CPROVER_UTIL_FORMAT_H
+
+#include <iosfwd>
+
+//! The below enables convenient syntax for feeding
+//! objects into streams, via stream << format(o)
+template <typename T>
+class format_containert
+{
+public:
+  explicit format_containert(const T &_o) : o(_o)
+  {
+  }
+
+  const T &o;
+};
+
+template <typename T>
+static inline std::ostream &
+operator<<(std::ostream &os, const format_containert<T> &f)
+{
+  return format_rec(os, f.o);
+}
+
+template <typename T>
+static inline format_containert<T> format(const T &o)
+{
+  return format_containert<T>(o);
+}
+
+#endif // CPROVER_UTIL_FORMAT_H
diff --git a/src/util/format_expr.cpp b/src/util/format_expr.cpp
new file mode 100644
index 00000000000..e7f91e43169
--- /dev/null
+++ b/src/util/format_expr.cpp
@@ -0,0 +1,220 @@
+/*******************************************************************\
+
+Module: Expression Pretty Printing
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+/// \file
+/// Expression Pretty Printing
+
+#include "arith_tools.h"
+#include "expr.h"
+#include "expr_iterator.h"
+#include "fixedbv.h"
+#include "format_expr.h"
+#include "format_type.h"
+#include "ieee_float.h"
+#include "invariant.h"
+#include "mp_arith.h"
+#include "rational.h"
+#include "rational_tools.h"
+#include "std_expr.h"
+#include "string2int.h"
+
+#include <stack>
+#include <ostream>
+
+/// We use the precendences that most readers expect
+/// (i.e., the ones you learn in primary school),
+/// and stay clear of the surprising ones that C has.
+static bool bracket_subexpression(
+  const exprt &sub_expr,
+  const exprt &expr)
+{
+  // no need for parentheses whenever the subexpression
+  // doesn't have operands
+  if(!sub_expr.has_operands())
+    return false;
+
+  // * and / bind stronger than + and -
+  if(
+    (sub_expr.id() == ID_mult || sub_expr.id() == ID_div) &&
+    (expr.id() == ID_plus || expr.id() == ID_minus))
+    return false;
+
+  // ==, !=, <, <=, >, >= bind stronger than && and ||
+  if(
+    (sub_expr.id() == ID_equal || sub_expr.id() == ID_notequal ||
+     sub_expr.id() == ID_lt || sub_expr.id() == ID_gt ||
+     sub_expr.id() == ID_le || sub_expr.id() == ID_ge) &&
+    (expr.id() == ID_and || expr.id() == ID_or))
+    return false;
+
+  return true;
+}
+
+/// This formats a multi-ary expression,
+/// adding parentheses where indicated by \ref bracket_subexpression
+static std::ostream &format_rec(
+  std::ostream &os,
+  const multi_ary_exprt &src)
+{
+  bool first = true;
+
+  for(const auto &op : src.operands())
+  {
+    if(first)
+      first = false;
+    else
+      os << ' ' << src.id() << ' ';
+
+    const bool need_parentheses = bracket_subexpression(op, src);
+
+    if(need_parentheses)
+      os << '(';
+
+    os << format(op);
+
+    if(need_parentheses)
+      os << ')';
+  }
+
+  return os;
+}
+
+/// This formats a binary expression,
+/// which we do as for multi-ary expressions
+static std::ostream &format_rec(
+  std::ostream &os,
+  const binary_exprt &src)
+{
+  return format_rec(os, to_multi_ary_expr(src));
+}
+
+/// This formats a unary expression,
+/// adding parentheses very aggressively.
+static std::ostream &format_rec(
+  std::ostream &os,
+  const unary_exprt &src)
+{
+  if(src.id() == ID_not)
+    os << '!';
+  else if(src.id() == ID_unary_minus)
+    os << '-';
+  else
+    return os << src.pretty();
+
+  if(src.op0().has_operands())
+    return os << '(' << format(src.op0()) << ')';
+  else
+    return os << format(src.op0());
+}
+
+/// This formats a constant
+static std::ostream &format_rec(
+  std::ostream &os,
+  const constant_exprt &src)
+{
+  auto type = src.type().id();
+
+  if(type == ID_bool)
+  {
+    if(src.is_true())
+      return os << "true";
+    else if(src.is_false())
+      return os << "false";
+    else
+      return os << src.pretty();
+  }
+  else if(type == ID_unsignedbv || type == ID_signedbv)
+    return os << *numeric_cast<mp_integer>(src);
+  else if(type == ID_integer)
+    return os << src.get_value();
+  else if(type == ID_floatbv)
+    return os << ieee_floatt(src);
+  else
+    return os << src.pretty();
+}
+
+// The below generates a string in a generic syntax
+// that is inspired by C/C++/Java, and is meant for debugging
+// purposes.
+std::ostream &format_rec(
+  std::ostream &os,
+  const exprt &expr)
+{
+  const auto &id = expr.id();
+
+  if(id == ID_plus || id == ID_mult || id == ID_and || id == ID_or)
+    return format_rec(os, to_multi_ary_expr(expr));
+  else if(
+    id == ID_lt || id == ID_gt || id == ID_ge || id == ID_le ||
+    id == ID_minus || id == ID_implies || id == ID_equal || id == ID_notequal)
+    return format_rec(os, to_binary_expr(expr));
+  else if(id == ID_not || id == ID_unary_minus)
+    return format_rec(os, to_unary_expr(expr));
+  else if(id == ID_constant)
+    return format_rec(os, to_constant_expr(expr));
+  else if(id == ID_typecast)
+    return os << "cast(" << format(to_typecast_expr(expr).op()) << ", "
+              << format(expr.type()) << ')';
+  else if(id == ID_member)
+    return os << format(to_member_expr(expr).op()) << '.'
+              << to_member_expr(expr).get_component_name();
+  else if(id == ID_symbol)
+    return os << to_symbol_expr(expr).get_identifier();
+  else if(id == ID_forall || id == ID_exists)
+    return os << id << ' ' << format(to_quantifier_expr(expr).symbol()) << " : "
+              << format(to_quantifier_expr(expr).symbol().type()) << " . "
+              << format(to_quantifier_expr(expr).where());
+  else if(id == ID_let)
+    return os << "LET " << format(to_let_expr(expr).symbol()) << " = "
+              << format(to_let_expr(expr).value()) << " IN "
+              << format(to_let_expr(expr).where());
+  else if(id == ID_array || id == ID_struct)
+  {
+    os << "{ ";
+
+    bool first = true;
+
+    for(const auto &op : expr.operands())
+    {
+      if(first)
+        first = false;
+      else
+        os << ", ";
+
+      os << format(op);
+    }
+
+    return os << '}';
+  }
+  else if(id == ID_if)
+  {
+    const auto &if_expr = to_if_expr(expr);
+    return os << format(if_expr.cond()) << '?' << format(if_expr.true_case())
+              << ':' << format(if_expr.false_case());
+  }
+  else
+  {
+    if(!expr.has_operands())
+      return os << id;
+
+    os << id << '(';
+    bool first = true;
+
+    for(const auto &op : expr.operands())
+    {
+      if(first)
+        first = false;
+      else
+        os << ", ";
+
+      os << format(op);
+    }
+
+    return os << ')';
+  }
+}
diff --git a/src/util/format_expr.h b/src/util/format_expr.h
new file mode 100644
index 00000000000..449ea23ce9d
--- /dev/null
+++ b/src/util/format_expr.h
@@ -0,0 +1,19 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_UTIL_FORMAT_EXPR_H
+#define CPROVER_UTIL_FORMAT_EXPR_H
+
+#include "format.h"
+#include "expr.h"
+
+//! Formats an expression in a generic syntax
+//! that is inspired by C/C++/Java, and is meant for debugging
+std::ostream &format_rec(std::ostream &, const exprt &);
+
+#endif // CPROVER_UTIL_FORMAT_EXPR_H
diff --git a/src/util/format_type.cpp b/src/util/format_type.cpp
new file mode 100644
index 00000000000..e026be7df75
--- /dev/null
+++ b/src/util/format_type.cpp
@@ -0,0 +1,60 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#include "format_expr.h"
+#include "format_type.h"
+#include "std_types.h"
+
+#include <ostream>
+
+/// format a \ref struct_typet
+static std::ostream &format_rec(
+  std::ostream &os,
+  const struct_typet &src)
+{
+  os << "struct"
+     << " {";
+  bool first = true;
+
+  for(const auto &c : src.components())
+  {
+    if(first)
+      first = false;
+    else
+      os << ',';
+
+    os << ' ' << format(c.type()) << ' ' << c.get_name();
+  }
+
+  return os << " }";
+}
+
+// The below generates a string in a generic syntax
+// that is inspired by C/C++/Java, and is meant for debugging
+// purposes.
+std::ostream &format_rec(std::ostream &os, const typet &type)
+{
+  const auto &id = type.id();
+
+  if(id == ID_pointer)
+    return os << '*' << format(type.subtype());
+  else if(id == ID_array)
+  {
+    const auto &t = to_array_type(type);
+    if(t.is_complete())
+      return os << format(type.subtype()) << '[' << format(t.size()) << ']';
+    else
+      return os << format(type.subtype()) << "[]";
+  }
+  else if(id == ID_struct)
+    return format_rec(os, to_struct_type(type));
+  else if(id == ID_symbol)
+    return os << "symbol_type " << to_symbol_type(type).get_identifier();
+  else
+    return os << id;
+}
diff --git a/src/util/format_type.h b/src/util/format_type.h
new file mode 100644
index 00000000000..9b3eb52dec0
--- /dev/null
+++ b/src/util/format_type.h
@@ -0,0 +1,19 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_UTIL_FORMAT_TYPE_H
+#define CPROVER_UTIL_FORMAT_TYPE_H
+
+#include "format.h"
+#include "type.h"
+
+//! Formats a type in a generic syntax
+//! that is inspired by C/C++/Java, and is meant for debugging
+std::ostream &format_rec(std::ostream &, const typet &);
+
+#endif // CPROVER_UTIL_FORMAT_TYPE_H
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
index f39237d6b48..711bade9e97 100644
--- a/src/util/simplify_expr.cpp
+++ b/src/util/simplify_expr.cpp
@@ -38,7 +38,6 @@ Author: Daniel Kroening, kroening@kroening.com
 // #define DEBUGX
 
 #ifdef DEBUGX
-#include <langapi/language_util.h>
 #include <iostream>
 #endif
 
@@ -2344,8 +2343,7 @@ bool simplify_exprt::simplify_node(exprt &expr)
      #endif
      )
   {
-    std::cout << "===== " << from_expr(ns, "", old)
-              << "\n ---> " << from_expr(ns, "", expr)
+    std::cout << "===== " << format(old) << "\n ---> " << format(expr)
               << "\n";
   }
   #endif
@@ -2417,12 +2415,12 @@ bool simplify_exprt::simplify(exprt &expr)
 {
 #ifdef DEBUG_ON_DEMAND
   if(debug_on)
-    std::cout << "TO-SIMP " << from_expr(ns, "", expr) << "\n";
+    std::cout << "TO-SIMP " << format(expr) << "\n";
 #endif
   bool res=simplify_rec(expr);
 #ifdef DEBUG_ON_DEMAND
   if(debug_on)
-    std::cout << "FULLSIMP " << from_expr(ns, "", expr) << "\n";
+    std::cout << "FULLSIMP " << format(expr) << "\n";
 #endif
   return res;
 }
diff --git a/src/util/type.h b/src/util/type.h
index 8bf58296c61..ddfcc77f1db 100644
--- a/src/util/type.h
+++ b/src/util/type.h
@@ -10,7 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_UTIL_TYPE_H
 #define CPROVER_UTIL_TYPE_H
 
-#include <util/source_location.h>
+#include "source_location.h"
 
 #define SUBTYPE_IN_GETSUB
 #define SUBTYPES_IN_GETSUB
diff --git a/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp b/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp
index a5aa7eb4028..128f5b0a04f 100644
--- a/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp
+++ b/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp
@@ -11,9 +11,13 @@
 #include <numeric>
 #include <java_bytecode/java_bytecode_language.h>
 #include <java_bytecode/java_types.h>
+
 #include <langapi/mode.h>
+#include <langapi/language_util.h>
+
 #include <solvers/refinement/string_constraint_instantiation.h>
 #include <solvers/sat/satcheck.h>
+
 #include <util/simplify_expr.h>
 #include <util/config.h>