smt2_format can now format symbols and constants

Author: Daniel Kroening

src/solvers/smt2/smt2_format.cpp

@@ -8,20 +8,65 @@ Author: Daniel Kroening, [email protected]
 
 #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;
 }

src/solvers/smt2/smt2_format.h

@@ -9,17 +9,31 @@ Author: Daniel Kroening, [email protected]
 #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