From 70f7846af5e736032daed9c6becb50257a2c98c0 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 24 Oct 2017 03:18:59 -0700
Subject: [PATCH] move spacer_marshal to under parsers/smt2

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/muz/spacer/CMakeLists.txt                 |  1 -
 src/parsers/smt2/CMakeLists.txt               |  1 +
 .../smt2/marshal.cpp}                         | 22 +++++++------------
 .../smt2/marshal.h}                           |  5 +----
 4 files changed, 10 insertions(+), 19 deletions(-)
 rename src/{muz/spacer/spacer_marshal.cpp => parsers/smt2/marshal.cpp} (71%)
 rename src/{muz/spacer/spacer_marshal.h => parsers/smt2/marshal.h} (91%)

diff --git a/src/muz/spacer/CMakeLists.txt b/src/muz/spacer/CMakeLists.txt
index 94e429171..97c991e2a 100644
--- a/src/muz/spacer/CMakeLists.txt
+++ b/src/muz/spacer/CMakeLists.txt
@@ -7,7 +7,6 @@ z3_add_component(spacer
   spacer_farkas_learner.cpp
   spacer_generalizers.cpp
   spacer_manager.cpp
-  spacer_marshal.cpp
   spacer_prop_solver.cpp
   spacer_smt_context_manager.cpp
   spacer_sym_mux.cpp
diff --git a/src/parsers/smt2/CMakeLists.txt b/src/parsers/smt2/CMakeLists.txt
index 1467d95c6..022cce2f2 100644
--- a/src/parsers/smt2/CMakeLists.txt
+++ b/src/parsers/smt2/CMakeLists.txt
@@ -1,5 +1,6 @@
 z3_add_component(smt2parser
   SOURCES
+    marshal.cpp
     smt2parser.cpp
     smt2scanner.cpp
   COMPONENT_DEPENDENCIES
diff --git a/src/muz/spacer/spacer_marshal.cpp b/src/parsers/smt2/marshal.cpp
similarity index 71%
rename from src/muz/spacer/spacer_marshal.cpp
rename to src/parsers/smt2/marshal.cpp
index 68c90bd33..ae144e491 100644
--- a/src/muz/spacer/spacer_marshal.cpp
+++ b/src/parsers/smt2/marshal.cpp
@@ -2,14 +2,14 @@
 Copyright (c) 2017 Arie Gurfinkel
 Module Name:
 
-   spacer_marshal.cpp
+   marshal.cpp
 
 Abstract:
 
    marshaling and unmarshaling of expressions
 
    --*/
-#include "muz/spacer/spacer_marshal.h"
+#include "parsers/smt2/marshal.h"
 
 #include <sstream>
 
@@ -18,39 +18,33 @@ Abstract:
 #include "util/vector.h"
 #include "ast/ast_smt_pp.h"
 #include "ast/ast_pp.h"
+#include "ast/ast_util.h"
 
-namespace spacer {
-std::ostream &marshal(std::ostream &os, expr_ref e, ast_manager &m)
-{
+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::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)
-{
+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();
-    if (it == end) { return expr_ref(m.mk_true(), m); }
     unsigned size = static_cast<unsigned>(end - it);
-    return expr_ref(m.mk_and(size, it), m);
+    return expr_ref(mk_and(m, size, it), m);
 }
 
-expr_ref unmarshal(std::string s, ast_manager &m)
-{
+expr_ref unmarshal(std::string s, ast_manager &m) {
     std::istringstream is(s);
     return unmarshal(is, m);
 }
-}
diff --git a/src/muz/spacer/spacer_marshal.h b/src/parsers/smt2/marshal.h
similarity index 91%
rename from src/muz/spacer/spacer_marshal.h
rename to src/parsers/smt2/marshal.h
index 95cb8f26a..ebc2c0426 100644
--- a/src/muz/spacer/spacer_marshal.h
+++ b/src/parsers/smt2/marshal.h
@@ -2,7 +2,7 @@
 Copyright (c) 2017 Arie Gurfinkel
 Module Name:
 
-   spacer_marshal.h
+   marshal.h
 
 Abstract:
 
@@ -17,14 +17,11 @@ Abstract:
 
 #include "ast/ast.h"
 
-namespace spacer {
 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