diff --git a/src/muz/base/fixedpoint_params.pyg b/src/muz/base/fixedpoint_params.pyg index dc051bd71..74903baf1 100644 --- a/src/muz/base/fixedpoint_params.pyg +++ b/src/muz/base/fixedpoint_params.pyg @@ -192,7 +192,8 @@ def_module_params('fixedpoint', ('spacer.quic_gen_normalize', BOOL, True, 'normalize cube before quantified generalization'), ('spacer.share_lemmas', BOOL, False, "Share frame lemmas"), ('spacer.share_invariants', BOOL, False, "Share invariants lemmas"), - ('spacer.from_level', UINT, 0, 'starting level to explore') + ('spacer.from_level', UINT, 0, 'starting level to explore'), + ('spacer.print_json', SYMBOL, '', 'print pobs tree in JSON format to a given file') )) diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index a4faf88cf..75a9d7d81 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -1353,6 +1353,14 @@ void lemma::instantiate(expr * const * exprs, expr_ref &result, expr *e) { vs(body, num_decls, exprs, result); } +void lemma::set_level (unsigned lvl) { + if(m_pob){ + m_pob->blocked_at(lvl); + } + m_lvl = lvl; +} + + void lemma::mk_insts(expr_ref_vector &out, expr* e) { expr *lem = e == nullptr ? get_expr() : e; @@ -1376,6 +1384,7 @@ bool pred_transformer::frames::add_lemma(lemma *lem) for (unsigned i = 0, sz = m_lemmas.size(); i < sz; ++i) { if (m_lemmas [i]->get_expr() == lem->get_expr()) { + m_pt.get_context().new_lemma_eh(m_pt, lem); // extend bindings if needed if (!lem->get_bindings().empty()) { m_lemmas [i]->add_binding(lem->get_bindings()); @@ -1879,7 +1888,8 @@ pob::pob (pob* parent, pred_transformer& pt, m_binding(m_pt.get_ast_manager()), m_new_post (m_pt.get_ast_manager ()), m_level (level), m_depth (depth), - m_open (true), m_use_farkas (true), m_weakness(0) { + m_open (true), m_use_farkas (true), m_weakness(0), + m_blocked_lvl(0) { if(add_to_parent && m_parent) { m_parent->add_child(*this); } @@ -1994,6 +2004,11 @@ void pob_queue::reset() if (m_root) { m_obligations.push(m_root); } } +void pob_queue::push(pob &n) { + m_obligations.push (&n); + n.get_context().new_pob_eh(&n); +} + // ---------------- // context @@ -2015,7 +2030,8 @@ context::context(fixedpoint_params const& params, m_use_qlemmas (params.spacer_qlemmas ()), m_weak_abs(params.spacer_weak_abs()), m_use_restarts(params.spacer_restarts()), - m_restart_initial_threshold(params.spacer_restart_initial_threshold()) + m_restart_initial_threshold(params.spacer_restart_initial_threshold()), + m_json_marshaller(this) {} context::~context() @@ -2728,7 +2744,13 @@ lbool context::solve_core (unsigned from_lvl) if (check_reachability()) { return l_true; } if (lvl > 0 && !get_params ().spacer_skip_propagate ()) - if (propagate(m_expanded_lvl, lvl, UINT_MAX)) { return l_false; } + if (propagate(m_expanded_lvl, lvl, UINT_MAX)) { dump_json(); return l_false; } + + dump_json(); + + if (is_inductive()){ + return l_false; + } for (unsigned i = 0; i < m_callbacks.size(); i++){ if (m_callbacks[i]->unfold()) @@ -2963,6 +2985,7 @@ bool context::is_reachable(pob &n) //this processes a goal and creates sub-goal lbool context::expand_node(pob& n) { + pob::on_expand_event _evt(n); TRACE ("spacer", tout << "expand-node: " << n.pt().head()->get_name() << " level: " << n.level() @@ -3613,6 +3636,8 @@ void context::add_constraint (unsigned level, const expr_ref& c) } void context::new_lemma_eh(pred_transformer &pt, lemma *lem) { + if (m_params.spacer_print_json().size()) + m_json_marshaller.register_lemma(lem); bool handle=false; for (unsigned i = 0; i < m_callbacks.size(); i++) { handle|=m_callbacks[i]->new_lemma(); @@ -3634,6 +3659,18 @@ void context::new_lemma_eh(pred_transformer &pt, lemma *lem) { } } +void context::new_pob_eh(pob *p) { + if (m_params.spacer_print_json().size()) + m_json_marshaller.register_pob(p); +} + +bool context::is_inductive() { + // check that inductive level (F infinity) of the query predicate + // contains a constant false + + return false; +} + inline bool pob_lt::operator() (const pob *pn1, const pob *pn2) const { SASSERT (pn1); diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h index 9d6d8d0a5..ff0e90cfa 100644 --- a/src/muz/spacer/spacer_context.h +++ b/src/muz/spacer/spacer_context.h @@ -31,6 +31,7 @@ Notes: #include "util/scoped_ptr_vector.h" #include "muz/spacer/spacer_manager.h" #include "muz/spacer/spacer_prop_solver.h" +#include "muz/spacer/spacer_json.h" #include "muz/base/fixedpoint_params.hpp" @@ -140,7 +141,7 @@ public: inline bool external() { return m_external;} unsigned level () const {return m_lvl;} - void set_level (unsigned lvl) {m_lvl = lvl;} + void set_level (unsigned lvl); app_ref_vector& get_bindings() {return m_bindings;} bool has_binding(app_ref_vector const &binding); void add_binding(app_ref_vector const &binding); @@ -475,6 +476,10 @@ class pob { scoped_ptr m_derivation; ptr_vector m_kids; + + // depth -> watch + std::map m_expand_watches; + unsigned m_blocked_lvl; public: pob (pob* parent, pred_transformer& pt, unsigned level, unsigned depth=0, bool add_to_parent=true); @@ -504,6 +509,8 @@ public: unsigned level () const { return m_level; } unsigned depth () const {return m_depth;} + unsigned width () const {return m_kids.size();} + unsigned blocked_at(unsigned lvl=0){return (m_blocked_lvl = std::max(lvl, m_blocked_lvl)); } bool use_farkas_generalizer () const {return m_use_farkas;} void set_farkas_generalizer (bool v) {m_use_farkas = v;} @@ -537,6 +544,10 @@ public: */ void get_skolems(app_ref_vector& v); + void on_expand() { m_expand_watches[m_depth].start(); if(m_parent.get()){m_parent.get()->on_expand();} } + void off_expand() { m_expand_watches[m_depth].stop(); if(m_parent.get()){m_parent.get()->off_expand();} }; + double get_expand_time(unsigned depth) { return m_expand_watches[depth].get_seconds();} + void inc_ref () {++m_ref_count;} void dec_ref () { @@ -544,6 +555,13 @@ public: if(m_ref_count == 0) { dealloc(this); } } + class on_expand_event + { + pob &m_p; + public: + on_expand_event(pob &p) : m_p(p) {m_p.on_expand();} + ~on_expand_event() {m_p.off_expand();} + }; }; @@ -653,7 +671,7 @@ public: void reset(); pob * top (); void pop () {m_obligations.pop ();} - void push (pob &n) {m_obligations.push (&n);} + void push (pob &n); void inc_level () { @@ -712,6 +730,10 @@ public: virtual void unfold_eh() {} + virtual inline bool propagate() { return false; } + + virtual void propagate_eh() {} + }; @@ -764,6 +786,7 @@ class context { bool m_use_restarts; unsigned m_restart_initial_threshold; scoped_ptr_vector m_callbacks; + json_marshaller m_json_marshaller; // Functions used by search. lbool solve_core (unsigned from_lvl = 0); @@ -803,6 +826,15 @@ class context { unsigned get_cex_depth (); + void dump_json() { + if(m_params.spacer_print_json().size()) { + std::ofstream of; + of.open(m_params.spacer_print_json().bare_str()); + m_json_marshaller.marshal(of); + of.close(); + } + } + public: /** Initial values of predicates are stored in corresponding relations in dctx. @@ -887,6 +919,10 @@ public: void new_lemma_eh(pred_transformer &pt, lemma *lem); scoped_ptr_vector &callbacks() {return m_callbacks;} + + void new_pob_eh(pob *p); + + bool is_inductive(); }; inline bool pred_transformer::use_native_mbp () {return ctx.use_native_mbp ();} diff --git a/src/muz/spacer/spacer_json.cpp b/src/muz/spacer/spacer_json.cpp index 0bfa091c1..8b7a0878e 100644 --- a/src/muz/spacer/spacer_json.cpp +++ b/src/muz/spacer/spacer_json.cpp @@ -73,10 +73,10 @@ namespace spacer { return out; } - std::ostream &json_marshal(std::ostream &out, const lemma_ref_vector lemmas) { + std::ostream &json_marshal(std::ostream &out, const lemma_ref_vector &lemmas) { std::ostringstream ls; - for (auto &l:lemmas) { + for (auto l:lemmas) { ls << (ls.tellp() == 0 ? "" : ","); json_marshal(ls, l); } @@ -85,12 +85,13 @@ namespace spacer { } - 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::register_lemma(lemma *l) { + if (l->has_pob()) { + m_relations[&*l->get_pob()][l->get_pob()->depth()].push_back(l); + } } - void json_marshaller::new_pob_eh(pob *p) { + void json_marshaller::register_pob(pob *p) { m_relations[p]; } @@ -110,15 +111,16 @@ namespace spacer { lemmas << (lemmas.tellp() == 0 ? "" : ",\n"); lemmas << "\"" << pob_id << "\":{" << pob_lemmas.str() << "}"; } + pob_id++; } unsigned depth = 0; while (true) { double root_expand_time = m_ctx->get_root().get_expand_time(depth); bool a = false; - unsigned i = 0; + pob_id = 0; for (auto &pob_map:m_relations) { - pob_ref n = pob_map.first; + pob *n = pob_map.first; double expand_time = n->get_expand_time(depth); if (expand_time > 0) { a = true; @@ -131,7 +133,7 @@ namespace spacer { "\",\"absolute_time\":\"" << std::setprecision(2) << expand_time << "\",\"predicate\":\"" << n->pt().head()->get_name() << "\",\"expr_id\":\"" << n->post()->get_id() << - "\",\"pob_id\":\"" << i << + "\",\"pob_id\":\"" << pob_id << "\",\"depth\":\"" << depth << "\",\"expr\":" << pob_expr.str() << "}"; if (n->parent()) { @@ -140,6 +142,7 @@ namespace spacer { "\",\"to\":\"" << depth << n << "\"}"; } } + pob_id++; } if (!a) { break; diff --git a/src/muz/spacer/spacer_json.h b/src/muz/spacer/spacer_json.h index dc411f67c..c75110371 100644 --- a/src/muz/spacer/spacer_json.h +++ b/src/muz/spacer/spacer_json.h @@ -39,8 +39,6 @@ namespace spacer { 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); @@ -50,14 +48,14 @@ namespace spacer { class json_marshaller { context *m_ctx; - std::map> m_relations; + std::map> m_relations; public: json_marshaller(context *ctx) : m_ctx(ctx) {} - void pob_blocked_by_lemma_eh(pob *p, lemma *l); + void register_lemma(lemma *l); - void new_pob_eh(pob *p); + void register_pob(pob *p); std::ostream &marshal(std::ostream &out) const; };