move spacer_marshal to under parsers/smt2

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/parsers/smt2/CMakeLists.txt

@@ -1,5 +1,6 @@
 z3_add_component(smt2parser
   SOURCES
+    marshal.cpp
     smt2parser.cpp
     smt2scanner.cpp
   COMPONENT_DEPENDENCIES

src/parsers/smt2/marshal.cpp

@@ -0,0 +1,50 @@
+/*++
+Copyright (c) 2017 Arie Gurfinkel
+Module Name:
+
+   marshal.cpp
+
+Abstract:
+
+   marshaling and unmarshaling of expressions
+
+   --*/
+#include "parsers/smt2/marshal.h"
+
+#include <sstream>
+
+#include "cmd_context/cmd_context.h"
+#include "parsers/smt2/smt2parser.h"
+#include "util/vector.h"
+#include "ast/ast_smt_pp.h"
+#include "ast/ast_pp.h"
+#include "ast/ast_util.h"
+
+std::ostream &marshal(std::ostream &os, expr_ref e, ast_manager &m) {
+    ast_smt_pp pp(m);
+    pp.display_smt2(os, e);
+    return os;
+}
+
+std::string marshal(expr_ref e, ast_manager &m) {
+    std::stringstream ss;
+    marshal(ss, e, m);
+    return ss.str();
+}
+
+
+expr_ref unmarshal(std::istream &is, ast_manager &m) {
+    cmd_context ctx(false, &m);
+    ctx.set_ignore_check(true);
+    if (!parse_smt2_commands(ctx, is)) { return expr_ref(0, m); }
+
+    ptr_vector<expr>::const_iterator it  = ctx.begin_assertions();
+    ptr_vector<expr>::const_iterator end = ctx.end_assertions();
+    unsigned size = static_cast<unsigned>(end - it);
+    return expr_ref(mk_and(m, size, it), m);
+}
+
+expr_ref unmarshal(std::string s, ast_manager &m) {
+    std::istringstream is(s);
+    return unmarshal(is, m);
+}

src/parsers/smt2/marshal.h

@@ -0,0 +1,27 @@
+/*++
+Copyright (c) 2017 Arie Gurfinkel
+Module Name:
+
+   marshal.h
+
+Abstract:
+
+   marshaling and unmarshaling of expressions
+
+   --*/
+#ifndef _SPACER_MARSHAL_H_
+#define _SPACER_MARSHAL_H_
+
+#include <string>
+#include <iostream>
+
+#include "ast/ast.h"
+
+std::ostream &marshal(std::ostream &os, expr_ref e, ast_manager &m);
+std::string marshal(expr_ref e, ast_manager &m);
+expr_ref unmarshal(std::string s, ast_manager &m);
+expr_ref unmarshal(std::istream &is, ast_manager &m);
+
+
+
+#endif