From bfa472faece8e9ca356848adc99db2d5cc98f96f Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Tue, 29 May 2018 22:11:52 -0700 Subject: [PATCH] New style of json dump based on lemmas at pob --- src/muz/spacer/spacer_context.cpp | 6 +- src/muz/spacer/spacer_context.h | 4 +- src/muz/spacer/spacer_json.cpp | 234 +++++++++++++++++------------- src/muz/spacer/spacer_json.h | 39 +++-- 4 files changed, 156 insertions(+), 127 deletions(-) diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index 3d7e9a921..491349a4e 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -441,7 +441,7 @@ void derivation::premise::set_summary (expr * summary, bool must, lemma::lemma (ast_manager &manager, expr * body, unsigned lvl) : m_ref_count(0), m(manager), m_body(body, m), m_cube(m), - m_zks(m), m_bindings(m), m_lvl(lvl), + m_zks(m), m_bindings(m), m_lvl(lvl), m_init_lvl(m_lvl), m_pob(nullptr), m_ctp(nullptr), m_external(false) { SASSERT(m_body); normalize(m_body, m_body); @@ -450,7 +450,7 @@ lemma::lemma (ast_manager &manager, expr * body, unsigned lvl) : lemma::lemma(pob_ref const &p) : m_ref_count(0), m(p->get_ast_manager()), m_body(m), m_cube(m), - m_zks(m), m_bindings(m), m_lvl(p->level()), + m_zks(m), m_bindings(m), m_lvl(p->level()), m_init_lvl(m_lvl), m_pob(p), m_ctp(nullptr), m_external(false) { SASSERT(m_pob); m_pob->get_skolems(m_zks); @@ -461,7 +461,7 @@ lemma::lemma(pob_ref const &p, expr_ref_vector &cube, unsigned lvl) : m_ref_count(0), m(p->get_ast_manager()), m_body(m), m_cube(m), - m_zks(m), m_bindings(m), m_lvl(p->level()), + m_zks(m), m_bindings(m), m_lvl(p->level()), m_init_lvl(m_lvl), m_pob(p), m_ctp(nullptr), m_external(false) { if (m_pob) { diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h index 2adf23007..c28f69d8b 100644 --- a/src/muz/spacer/spacer_context.h +++ b/src/muz/spacer/spacer_context.h @@ -114,7 +114,8 @@ class lemma { expr_ref_vector m_cube; app_ref_vector m_zks; app_ref_vector m_bindings; - unsigned m_lvl; + unsigned m_lvl; // current level of the lemma + unsigned m_init_lvl; // level at which lemma was created pob_ref m_pob; model_ref m_ctp; // counter-example to pushing bool m_external; @@ -150,6 +151,7 @@ public: bool is_inductive() const {return is_infty_level(m_lvl);} unsigned level () const {return m_lvl;} + unsigned init_level() const {return m_init_lvl;} void set_level (unsigned lvl); app_ref_vector& get_bindings() {return m_bindings;} bool has_binding(app_ref_vector const &binding); diff --git a/src/muz/spacer/spacer_json.cpp b/src/muz/spacer/spacer_json.cpp index c1094f192..cf36eb899 100644 --- a/src/muz/spacer/spacer_json.cpp +++ b/src/muz/spacer/spacer_json.cpp @@ -24,56 +24,59 @@ Notes: namespace spacer { - std::ostream &json_marshal(std::ostream &out, ast *t, ast_manager &m) { +static 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; - } + 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; } + 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; - } +static std::ostream &json_marshal(std::ostream &out, lemma *l) { + out << "{" + << R"("init_level":")" << l->init_level() + << 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) { +static std::ostream &json_marshal(std::ostream &out, const lemma_ref_vector &lemmas) { std::ostringstream ls; for (auto l:lemmas) { @@ -85,74 +88,103 @@ namespace spacer { } - void json_marshaller::register_lemma(lemma *l) { - if (l->has_pob()) { - m_relations[&*l->get_pob()][l->get_pob()->depth()].push_back(l); +void json_marshaller::register_lemma(lemma *l) { + if (l->has_pob()) { + m_relations[&*l->get_pob()][l->get_pob()->depth()].push_back(l); + } +} + +void json_marshaller::register_pob(pob *p) { + m_relations[p]; +} + +void json_marshaller::marshal_lemmas_old(std::ostream &out) const { + unsigned pob_id = 0; + for (auto &pob_map:m_relations) { + std::ostringstream pob_lemmas; + for (auto &depth_lemmas : pob_map.second) { + pob_lemmas << ((unsigned)pob_lemmas.tellp() == 0 ? "" : ",") + << "\"" << depth_lemmas.first << "\":"; + json_marshal(pob_lemmas, depth_lemmas.second); } + if (pob_lemmas.tellp()) { + out << ((unsigned)out.tellp() == 0 ? "" : ",\n"); + out << "\"" << pob_id << "\":{" << pob_lemmas.str() << "}"; + } + pob_id++; } +} +void json_marshaller::marshal_lemmas_new(std::ostream &out) const { + unsigned pob_id = 0; + for (auto &pob_map:m_relations) { + std::ostringstream pob_lemmas; + pob *n = pob_map.first; + for (auto *l : n->lemmas()) { + pob_lemmas << ((unsigned)pob_lemmas.tellp() == 0 ? "" : ",") + << "\"0\":"; + lemma_ref_vector lemmas_vec; + lemmas_vec.push_back(l); + json_marshal(pob_lemmas, lemmas_vec); + } - void json_marshaller::register_pob(pob *p) { - m_relations[p]; + if (pob_lemmas.tellp()) { + out << ((unsigned)out.tellp() == 0 ? "" : ",\n"); + out << "\"" << pob_id << "\":{" << pob_lemmas.str() << "}"; + } + pob_id++; } +} - std::ostream &spacer::json_marshaller::marshal(std::ostream &out) const { - std::ostringstream nodes; - std::ostringstream edges; - std::ostringstream lemmas; +std::ostream &json_marshaller::marshal(std::ostream &out) const { + std::ostringstream nodes; + std::ostringstream edges; + std::ostringstream lemmas; - unsigned pob_id = 0; + if (m_old_style) + marshal_lemmas_old(lemmas); + else + marshal_lemmas_new(lemmas); + + unsigned pob_id = 0; + unsigned depth = 0; + while (true) { + double root_expand_time = m_ctx->get_root().get_expand_time(depth); + bool a = false; + pob_id = 0; for (auto &pob_map:m_relations) { - std::ostringstream pob_lemmas; - for (auto &depth_lemmas : pob_map.second) { - pob_lemmas << ((unsigned)pob_lemmas.tellp() == 0 ? "" : ",") << "\"" << depth_lemmas.first << "\":"; - json_marshal(pob_lemmas, depth_lemmas.second); - } - if (pob_lemmas.tellp()) { - lemmas << ((unsigned)lemmas.tellp() == 0 ? "" : ",\n"); - lemmas << "\"" << pob_id << "\":{" << pob_lemmas.str() << "}"; + pob *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 << ((unsigned)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\":\"" << pob_id << + "\",\"depth\":\"" << depth << + "\",\"expr\":" << pob_expr.str() << "}"; + if (n->parent()) { + edges << ((unsigned)edges.tellp() == 0 ? "" : ",\n") << + "{\"from\":\"" << depth << n->parent() << + "\",\"to\":\"" << depth << n << "\"}"; + } } pob_id++; } - - unsigned depth = 0; - while (true) { - double root_expand_time = m_ctx->get_root().get_expand_time(depth); - bool a = false; - pob_id = 0; - for (auto &pob_map:m_relations) { - pob *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 << ((unsigned)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\":\"" << pob_id << - "\",\"depth\":\"" << depth << - "\",\"expr\":" << pob_expr.str() << "}"; - if (n->parent()) { - edges << ((unsigned)edges.tellp() == 0 ? "" : ",\n") << - "{\"from\":\"" << depth << n->parent() << - "\",\"to\":\"" << depth << n << "\"}"; - } - } - pob_id++; - } - if (!a) { - break; - } - depth++; + if (!a) { + break; } - 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; + 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 index b100a87dc..131e72678 100644 --- a/src/muz/spacer/spacer_json.h +++ b/src/muz/spacer/spacer_json.h @@ -31,34 +31,29 @@ class ast_manager; namespace spacer { - class lemma; - - typedef sref_vector lemma_ref_vector; - - class context; - - class pob; - - 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 lemma; +typedef sref_vector lemma_ref_vector; +class context; +class pob; - class json_marshaller { - context *m_ctx; - std::map> m_relations; +class json_marshaller { + context *m_ctx; + bool m_old_style; + std::map> m_relations; - public: - json_marshaller(context *ctx) : m_ctx(ctx) {} + void marshal_lemmas_old(std::ostream &out) const; + void marshal_lemmas_new(std::ostream &out) const; +public: + json_marshaller(context *ctx, bool old_style = false) : + m_ctx(ctx), m_old_style(old_style) {} - void register_lemma(lemma *l); + void register_lemma(lemma *l); - void register_pob(pob *p); + void register_pob(pob *p); - std::ostream &marshal(std::ostream &out) const; - }; + std::ostream &marshal(std::ostream &out) const; +}; }