From 3248f57434c84ad4e310aad0bbb3d8ce9d51283c Mon Sep 17 00:00:00 2001 From: Matteo Marescotti Date: Thu, 15 Mar 2018 16:31:22 -0400 Subject: [PATCH] Add support for printing spacer pobs in JSON --- src/muz/spacer/CMakeLists.txt | 1 + src/muz/spacer/spacer_json.cpp | 155 +++++++++++++++++++++++++++++++++ src/muz/spacer/spacer_json.h | 68 +++++++++++++++ 3 files changed, 224 insertions(+) create mode 100644 src/muz/spacer/spacer_json.cpp create mode 100644 src/muz/spacer/spacer_json.h diff --git a/src/muz/spacer/CMakeLists.txt b/src/muz/spacer/CMakeLists.txt index a351ea353..50e0c9382 100644 --- a/src/muz/spacer/CMakeLists.txt +++ b/src/muz/spacer/CMakeLists.txt @@ -24,6 +24,7 @@ z3_add_component(spacer spacer_sem_matcher.cpp spacer_quant_generalizer.cpp spacer_callback.cpp + spacer_json.cpp COMPONENT_DEPENDENCIES arith_tactics core_tactics diff --git a/src/muz/spacer/spacer_json.cpp b/src/muz/spacer/spacer_json.cpp new file mode 100644 index 000000000..0bfa091c1 --- /dev/null +++ b/src/muz/spacer/spacer_json.cpp @@ -0,0 +1,155 @@ +/**++ +Copyright (c) 2017 Microsoft Corporation and Matteo Marescotti + +Module Name: + + spacer_json.cpp + +Abstract: + + SPACER json marshalling support + +Author: + + Matteo Marescotti + +Notes: + +--*/ + +#include +#include "spacer_context.h" +#include "spacer_json.h" +#include "spacer_util.h" + +namespace spacer { + + std::ostream &json_marshal(std::ostream &out, ast *t, ast_manager &m) { + + mk_epp pp = mk_epp(t, m); + std::ostringstream ss; + ss << pp; + out << "\""; + for (auto &c:ss.str()) { + switch (c) { + case '"': + out << "\\\""; + break; + case '\\': + out << "\\\\"; + break; + case '\b': + out << "\\b"; + break; + case '\f': + out << "\\f"; + break; + case '\n': + out << "\\n"; + break; + case '\r': + out << "\\r"; + break; + case '\t': + out << "\\t"; + break; + default: + if ('\x00' <= c && c <= '\x1f') { + out << "\\u" + << std::hex << std::setw(4) << std::setfill('0') << (int) c; + } else { + out << c; + } + } + } + out << "\""; + return out; + } + + std::ostream &json_marshal(std::ostream &out, lemma *l) { + out << R"({"level":")" << l->level() << R"(", "expr":)"; + json_marshal(out, l->get_expr(), l->get_ast_manager()); + out << "}"; + return out; + } + + std::ostream &json_marshal(std::ostream &out, const lemma_ref_vector lemmas) { + + std::ostringstream ls; + for (auto &l:lemmas) { + ls << (ls.tellp() == 0 ? "" : ","); + json_marshal(ls, l); + } + out << "[" << ls.str() << "]"; + return out; + } + + + void json_marshaller::pob_blocked_by_lemma_eh(pob *p, lemma *l) { + //if(m_ctx->get_params().spacer_pr) + m_relations[p][p->depth()].push_back(l); + } + + void json_marshaller::new_pob_eh(pob *p) { + m_relations[p]; + } + + std::ostream &spacer::json_marshaller::marshal(std::ostream &out) const { + std::ostringstream nodes; + std::ostringstream edges; + std::ostringstream lemmas; + + unsigned pob_id = 0; + for (auto &pob_map:m_relations) { + std::ostringstream pob_lemmas; + for (auto &depth_lemmas : pob_map.second) { + pob_lemmas << (pob_lemmas.tellp() == 0 ? "" : ",") << "\"" << depth_lemmas.first << "\":"; + json_marshal(pob_lemmas, depth_lemmas.second); + } + if (pob_lemmas.tellp()) { + lemmas << (lemmas.tellp() == 0 ? "" : ",\n"); + lemmas << "\"" << pob_id << "\":{" << pob_lemmas.str() << "}"; + } + } + + unsigned depth = 0; + while (true) { + double root_expand_time = m_ctx->get_root().get_expand_time(depth); + bool a = false; + unsigned i = 0; + for (auto &pob_map:m_relations) { + pob_ref n = pob_map.first; + double expand_time = n->get_expand_time(depth); + if (expand_time > 0) { + a = true; + std::ostringstream pob_expr; + json_marshal(pob_expr, n->post(), n->get_ast_manager()); + + nodes << (nodes.tellp() == 0 ? "" : ",\n") << + "{\"id\":\"" << depth << n << + "\",\"relative_time\":\"" << expand_time / root_expand_time << + "\",\"absolute_time\":\"" << std::setprecision(2) << expand_time << + "\",\"predicate\":\"" << n->pt().head()->get_name() << + "\",\"expr_id\":\"" << n->post()->get_id() << + "\",\"pob_id\":\"" << i << + "\",\"depth\":\"" << depth << + "\",\"expr\":" << pob_expr.str() << "}"; + if (n->parent()) { + edges << (edges.tellp() == 0 ? "" : ",\n") << + "{\"from\":\"" << depth << n->parent() << + "\",\"to\":\"" << depth << n << "\"}"; + } + } + } + if (!a) { + break; + } + depth++; + } + out << "{\n\"nodes\":[\n" << nodes.str() << "\n],\n"; + out << "\"edges\":[\n" << edges.str() << "\n],\n"; + out << "\"lemmas\":{\n" << lemmas.str() << "\n}\n}\n"; + return out; + } + +} diff --git a/src/muz/spacer/spacer_json.h b/src/muz/spacer/spacer_json.h new file mode 100644 index 000000000..dc411f67c --- /dev/null +++ b/src/muz/spacer/spacer_json.h @@ -0,0 +1,68 @@ +/**++ +Copyright (c) 2017 Microsoft Corporation and Matteo Marescotti + +Module Name: + + spacer_json.h + +Abstract: + + SPACER json marshalling support + +Author: + + Matteo Marescotti + +Notes: + +--*/ + +#ifndef Z3_SPACER_JSON_H +#define Z3_SPACER_JSON_H + +#include +#include +#include "ref.h" +#include "ref_vector.h" + +class ast; + +class ast_manager; + +namespace spacer { + + class lemma; + + typedef sref_vector lemma_ref_vector; + + class context; + + class pob; + + typedef ref pob_ref; + + std::ostream &json_marshal(std::ostream &out, ast *t, ast_manager &m); + + std::ostream &json_marshal(std::ostream &out, lemma *l); + + std::ostream &json_marshal(std::ostream &out, lemma_ref_vector &lemmas); + + + class json_marshaller { + context *m_ctx; + std::map> m_relations; + + public: + json_marshaller(context *ctx) : m_ctx(ctx) {} + + void pob_blocked_by_lemma_eh(pob *p, lemma *l); + + void new_pob_eh(pob *p); + + std::ostream &marshal(std::ostream &out) const; + }; + +} + + +#endif //Z3_SPACER_JSON_H