From d5db868770e8f21fb6469df83d9e7e846c72db3c Mon Sep 17 00:00:00 2001
From: Daniel Kroening <kroening@cs.ox.ac.uk>
Date: Sat, 24 Nov 2018 21:24:32 +0000
Subject: [PATCH] smt2_format can now format symbols and constants

---
 src/solvers/smt2/smt2_format.cpp | 58 ++++++++++++++++++++++++++++----
 src/solvers/smt2/smt2_format.h   | 25 +++++++++++---
 2 files changed, 71 insertions(+), 12 deletions(-)

diff --git a/src/solvers/smt2/smt2_format.cpp b/src/solvers/smt2/smt2_format.cpp
index 592aa779b9..9f94357459 100644
--- a/src/solvers/smt2/smt2_format.cpp
+++ b/src/solvers/smt2/smt2_format.cpp
@@ -8,20 +8,64 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "smt2_format.h"
 
+#include <util/arith_tools.h>
+#include <util/std_expr.h>
 #include <util/std_types.h>
 
-std::ostream &operator<<(std::ostream &out, const smt2_format &f)
+std::ostream &smt2_format_rec(std::ostream &out, const typet &type)
 {
-  if(f.type.id() == ID_unsignedbv)
-    out << "(_ BitVec " << to_unsignedbv_type(f.type).get_width() << ')';
-  else if(f.type.id() == ID_bool)
+  if(type.id() == ID_unsignedbv)
+    out << "(_ BitVec " << to_unsignedbv_type(type).get_width() << ')';
+  else if(type.id() == ID_bool)
     out << "Bool";
-  else if(f.type.id() == ID_integer)
+  else if(type.id() == ID_integer)
     out << "Int";
-  else if(f.type.id() == ID_real)
+  else if(type.id() == ID_real)
     out << "Real";
   else
-    out << "? " << f.type.id();
+    out << "? " << type.id();
+
+  return out;
+}
+
+std::ostream &smt2_format_rec(std::ostream &out, const exprt &expr)
+{
+  if(expr.id() == ID_constant)
+  {
+    const auto &value = to_constant_expr(expr).get_value();
+
+    const typet &expr_type = expr.type();
+
+    if(expr_type.id() == ID_unsignedbv)
+    {
+      const std::size_t width = to_unsignedbv_type(expr_type).get_width();
+
+      const auto value = numeric_cast_v<mp_integer>(expr);
+
+      out << "(_ bv" << value << " " << width << ")";
+    }
+    else if(expr_type.id() == ID_bool)
+    {
+      if(expr.is_true())
+        out << "true";
+      else if(expr.is_false())
+        out << "false";
+      else
+        DATA_INVARIANT(false, "unknown Boolean constant");
+    }
+    else if(expr_type.id() == ID_integer)
+    {
+      out << value;
+    }
+    else
+      DATA_INVARIANT(false, "unhandled constant: " + expr_type.id_string());
+  }
+  else if(expr.id() == ID_symbol)
+  {
+    out << to_symbol_expr(expr).get_identifier();
+  }
+  else
+    out << "? " << expr.id();
 
   return out;
 }
diff --git a/src/solvers/smt2/smt2_format.h b/src/solvers/smt2/smt2_format.h
index b11eb42a05..d2eaa2412c 100644
--- a/src/solvers/smt2/smt2_format.h
+++ b/src/solvers/smt2/smt2_format.h
@@ -9,17 +9,32 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_SOLVERS_SMT2_SMT2_FORMAT_H
 #define CPROVER_SOLVERS_SMT2_SMT2_FORMAT_H
 
-#include <util/type.h>
+#include <util/expr.h>
 
-struct smt2_format
+template <typename T>
+struct smt2_format_containert
 {
-  explicit smt2_format(const typet &_type) : type(_type)
+  explicit smt2_format_containert(const T &_o) : o(_o)
   {
   }
 
-  const typet &type;
+  const T &o;
 };
 
-std::ostream &operator<<(std::ostream &, const smt2_format &);
+template <typename T>
+static inline smt2_format_containert<T> smt2_format(const T &_o)
+{
+  return smt2_format_containert<T>(_o);
+}
+
+template <typename T>
+static inline std::ostream &
+operator<<(std::ostream &out, const smt2_format_containert<T> &c)
+{
+  return smt2_format_rec(out, c.o);
+}
+
+std::ostream &smt2_format_rec(std::ostream &, const exprt &);
+std::ostream &smt2_format_rec(std::ostream &, const typet &);
 
 #endif // CPROVER_SOLVERS_SMT2_SMT2_FORMAT_H