move smt2_format into separate file

Author: Daniel Kroening

src/solvers/Makefile

@@ -185,6 +185,7 @@ SRC = $(BOOLEFORCE_SRC) \
       sat/resolution_proof.cpp \
       smt2/smt2_conv.cpp \
       smt2/smt2_dec.cpp \
+      smt2/smt2_format.cpp \
       smt2/smt2_parser.cpp \
       smt2/smt2_tokenizer.cpp \
       smt2/smt2irep.cpp \

src/solvers/smt2/smt2_format.cpp

@@ -0,0 +1,27 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#include "smt2_format.h"
+
+#include <util/std_types.h>
+
+std::ostream &operator<<(std::ostream &out, const smt2_format &f)
+{
+  if(f.type.id() == ID_unsignedbv)
+    out << "(_ BitVec " << to_unsignedbv_type(f.type).get_width() << ')';
+  else if(f.type.id() == ID_bool)
+    out << "Bool";
+  else if(f.type.id() == ID_integer)
+    out << "Int";
+  else if(f.type.id() == ID_real)
+    out << "Real";
+  else
+    out << "? " << f.type.id();
+
+  return out;
+}

src/solvers/smt2/smt2_format.h

@@ -0,0 +1,25 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#ifndef CPROVER_SOLVERS_SMT2_SMT2_FORMAT_H
+#define CPROVER_SOLVERS_SMT2_SMT2_FORMAT_H
+
+#include <util/type.h>
+
+struct smt2_format
+{
+  explicit smt2_format(const typet &_type) : type(_type)
+  {
+  }
+
+  const typet &type;
+};
+
+std::ostream &operator<<(std::ostream &, const smt2_format &);
+
+#endif // CPROVER_SOLVERS_SMT2_SMT2_FORMAT_H

src/solvers/smt2/smt2_parser.cpp

@@ -8,23 +8,9 @@ Author: Daniel Kroening, [email protected]
 
 #include "smt2_parser.h"
 
-#include <util/arith_tools.h>
-
-std::ostream &operator<<(std::ostream &out, const smt2_parsert::smt2_format &f)
-{
-  if(f.type.id() == ID_unsignedbv)
-    out << "(_ BitVec " << to_unsignedbv_type(f.type).get_width() << ')';
-  else if(f.type.id() == ID_bool)
-    out << "Bool";
-  else if(f.type.id() == ID_integer)
-    out << "Int";
-  else if(f.type.id() == ID_real)
-    out << "Real";
-  else
-    out << "? " << f.type.id();
+#include "smt2_format.h"
 
-  return out;
-}
+#include <util/arith_tools.h>
 
 void smt2_parsert::command_sequence()
 {

src/solvers/smt2/smt2_parser.h

@@ -43,15 +43,6 @@ class smt2_parsert:public smt2_tokenizert
   using id_mapt=std::map<irep_idt, idt>;
   id_mapt id_map;
 
-  struct smt2_format
-  {
-    explicit smt2_format(const typet &_type) : type(_type)
-    {
-    }
-
-    const typet type;
-  };
-
 protected:
   bool exit;
   void command_sequence();
@@ -91,6 +82,4 @@ class smt2_parsert:public smt2_tokenizert
   exprt cast_bv_to_unsigned(const exprt &);
 };
 
-std::ostream &operator<<(std::ostream &, const smt2_parsert::smt2_format &);
-
 #endif // CPROVER_SOLVERS_SMT2_SMT2_PARSER_H