format_expr now does index, c_bool constants, string constants

Author: Daniel Kroening

src/util/format_expr.cpp

@@ -17,6 +17,7 @@ Author: Daniel Kroening, [email protected]
 #include "format_type.h"
 #include "ieee_float.h"
 #include "invariant.h"
+#include "lispexpr.h"
 #include "mp_arith.h"
 #include "rational.h"
 #include "rational_tools.h"
@@ -128,12 +129,18 @@ static std::ostream &format_rec(
     else
       return os << src.pretty();
   }
-  else if(type == ID_unsignedbv || type == ID_signedbv)
+  else if(type == ID_unsignedbv ||
+          type == ID_signedbv ||
+          type == ID_c_bool)
     return os << *numeric_cast<mp_integer>(src);
   else if(type == ID_integer)
     return os << src.get_value();
+  else if(type == ID_string)
+    return os << '"' << escape(id2string(src.get_value())) << '"';
   else if(type == ID_floatbv)
     return os << ieee_floatt(src);
+  else if(type == ID_pointer && src.is_zero())
+    return os << src.get_value();
   else
     return os << src.pretty();
 }
@@ -165,6 +172,12 @@ std::ostream &format_rec(
               << to_member_expr(expr).get_component_name();
   else if(id == ID_symbol)
     return os << to_symbol_expr(expr).get_identifier();
+  else if(id == ID_index)
+  {
+    const auto &index_expr=to_index_expr(expr);
+    return os << format(index_expr.array()) << '['
+              << format(index_expr.index()) << ']';
+  }
   else if(id == ID_type)
     return format_rec(os, expr.type());
   else if(id == ID_forall || id == ID_exists)

src/util/json.h

@@ -112,9 +112,9 @@ class jsont
 
   static const jsont null_json_object;
 
-protected:
   static void escape_string(const std::string &, std::ostream &);
 
+protected:
   explicit jsont(kindt _kind):kind(_kind)
   {
   }