From 3c7165780c981957dd76cc48543f3c6576f9eeda Mon Sep 17 00:00:00 2001 From: Matteo Date: Thu, 5 Oct 2017 14:07:11 +0200 Subject: [PATCH] Extend spacer with callback events Callback events allow the client of spacer to get events during exection. The events include new lemmas and unfolding. --- src/api/api_datalog.cpp | 17 ++++++- src/api/z3_fixedpoint.h | 10 ++++ src/muz/base/dl_context.h | 8 ++++ src/muz/base/dl_engine_base.h | 10 ++++ src/muz/base/fixedpoint_params.pyg | 4 +- src/muz/spacer/CMakeLists.txt | 1 + src/muz/spacer/spacer_callback.cpp | 38 +++++++++++++++ src/muz/spacer/spacer_callback.h | 65 ++++++++++++++++++++++++++ src/muz/spacer/spacer_context.cpp | 57 ++++++++++++++++++++-- src/muz/spacer/spacer_context.h | 39 +++++++++++++++- src/muz/spacer/spacer_dl_interface.cpp | 8 ++++ src/muz/spacer/spacer_dl_interface.h | 5 ++ 12 files changed, 254 insertions(+), 8 deletions(-) create mode 100644 src/muz/spacer/spacer_callback.cpp create mode 100644 src/muz/spacer/spacer_callback.h diff --git a/src/api/api_datalog.cpp b/src/api/api_datalog.cpp index 2bc3d01e1..7d2e38269 100644 --- a/src/api/api_datalog.cpp +++ b/src/api/api_datalog.cpp @@ -603,7 +603,22 @@ extern "C" { Z3_CATCH; } - + + void Z3_API Z3_fixedpoint_add_callback(Z3_context c, Z3_fixedpoint d, + void *state, + Z3_fixedpoint_new_lemma_eh new_lemma_eh, + Z3_fixedpoint_predecessor_eh predecessor_eh, + Z3_fixedpoint_unfold_eh unfold_eh){ + Z3_TRY; + // not logged + to_fixedpoint_ref(d)->ctx().add_callback(state, + reinterpret_cast(new_lemma_eh), + reinterpret_cast(predecessor_eh), + reinterpret_cast(unfold_eh)); + + Z3_CATCH; + } + #include "api_datalog_spacer.inc" }; diff --git a/src/api/z3_fixedpoint.h b/src/api/z3_fixedpoint.h index a651993ce..6836c4766 100644 --- a/src/api/z3_fixedpoint.h +++ b/src/api/z3_fixedpoint.h @@ -367,6 +367,16 @@ extern "C" { void Z3_API Z3_fixedpoint_set_reduce_app_callback( Z3_context c, Z3_fixedpoint d, Z3_fixedpoint_reduce_app_callback_fptr cb); + typedef void (*Z3_fixedpoint_new_lemma_eh)(void *state, Z3_ast *lemma, unsigned level); + typedef void (*Z3_fixedpoint_predecessor_eh)(void *state); + typedef void (*Z3_fixedpoint_unfold_eh)(void *state); + + /** \brief set export callback for lemmas */ + void Z3_API Z3_fixedpoint_add_callback(Z3_context ctx, Z3_fixedpoint f, void *state, + Z3_fixedpoint_new_lemma_eh new_lemma_eh, + Z3_fixedpoint_predecessor_eh predecessor_eh, + Z3_fixedpoint_unfold_eh unfold_eh); + /*@}*/ /*@}*/ diff --git a/src/muz/base/dl_context.h b/src/muz/base/dl_context.h index 865c746db..a8567637c 100644 --- a/src/muz/base/dl_context.h +++ b/src/muz/base/dl_context.h @@ -588,6 +588,14 @@ namespace datalog { rel_context_base* get_rel_context() { ensure_engine(); return m_rel; } + void add_callback(void *state, + const datalog::t_new_lemma_eh new_lemma_eh, + const datalog::t_predecessor_eh predecessor_eh, + const datalog::t_unfold_eh unfold_eh) { + ensure_engine(); + m_engine->add_callback(state, new_lemma_eh, predecessor_eh, unfold_eh); + } + private: /** diff --git a/src/muz/base/dl_engine_base.h b/src/muz/base/dl_engine_base.h index b9ac6e7b5..910dd2695 100644 --- a/src/muz/base/dl_engine_base.h +++ b/src/muz/base/dl_engine_base.h @@ -36,6 +36,10 @@ namespace datalog { LAST_ENGINE }; + typedef void (*t_new_lemma_eh)(void *state, expr *lemma, unsigned level); + typedef void (*t_predecessor_eh)(void *state); + typedef void (*t_unfold_eh)(void *state); + class engine_base { ast_manager& m; std::string m_name; @@ -102,6 +106,12 @@ namespace datalog { virtual proof_ref get_proof() { return proof_ref(m.mk_asserted(m.mk_true()), m); } + virtual void add_callback(void *state, + const t_new_lemma_eh new_lemma_eh, + const t_predecessor_eh predecessor_eh, + const t_unfold_eh unfold_eh) { + throw default_exception(std::string("add_lemma_exchange_callbacks is not supported for ") + m_name); + } virtual void updt_params() {} virtual void cancel() {} virtual void cleanup() {} diff --git a/src/muz/base/fixedpoint_params.pyg b/src/muz/base/fixedpoint_params.pyg index 277399b9f..07b555095 100644 --- a/src/muz/base/fixedpoint_params.pyg +++ b/src/muz/base/fixedpoint_params.pyg @@ -190,7 +190,9 @@ def_module_params('fixedpoint', ('spacer.simplify_pob', BOOL, False, 'simplify POBs by removing redundant constraints'), ('spacer.use_quant_generalizer', BOOL, False, 'use quantified lemma generalizer'), ('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"), +)) diff --git a/src/muz/spacer/CMakeLists.txt b/src/muz/spacer/CMakeLists.txt index 16ce3e4f9..a351ea353 100644 --- a/src/muz/spacer/CMakeLists.txt +++ b/src/muz/spacer/CMakeLists.txt @@ -23,6 +23,7 @@ z3_add_component(spacer spacer_term_graph.cpp spacer_sem_matcher.cpp spacer_quant_generalizer.cpp + spacer_callback.cpp COMPONENT_DEPENDENCIES arith_tactics core_tactics diff --git a/src/muz/spacer/spacer_callback.cpp b/src/muz/spacer/spacer_callback.cpp new file mode 100644 index 000000000..9c7c88ad9 --- /dev/null +++ b/src/muz/spacer/spacer_callback.cpp @@ -0,0 +1,38 @@ +/**++ +Copyright (c) 2017 Microsoft Corporation and Matteo Marescotti + +Module Name: + + spacer_callback.cpp + +Abstract: + + SPACER plugin for handling events + +Author: + + Matteo Marescotti + +Notes: + +--*/ + +#include "spacer_callback.h" +#include "muz/spacer/spacer_context.h" + + +namespace spacer { + + void user_callback::new_lemma_eh(expr *lemma, unsigned level) { + m_new_lemma_eh(m_state, lemma, level); + } + + void user_callback::predecessor_eh() { + m_predecessor_eh(m_state); + } + + void user_callback::unfold_eh() { + m_unfold_eh(m_state); + } + +} \ No newline at end of file diff --git a/src/muz/spacer/spacer_callback.h b/src/muz/spacer/spacer_callback.h new file mode 100644 index 000000000..d5b47b90e --- /dev/null +++ b/src/muz/spacer/spacer_callback.h @@ -0,0 +1,65 @@ +/**++ +Copyright (c) 2017 Microsoft Corporation and Matteo Marescotti + +Module Name: + + spacer_callback.h + +Abstract: + + SPACER plugin for handling events + +Author: + + Matteo Marescotti + +Notes: + +--*/ + +#ifndef _SPACER_CALLBACK_H_ +#define _SPACER_CALLBACK_H_ + +#include "muz/spacer/spacer_context.h" +#include "muz/base/dl_engine_base.h" + + +namespace spacer { + + class user_callback : public spacer_callback { + private: + void *m_state; + const datalog::t_new_lemma_eh m_new_lemma_eh; + const datalog::t_predecessor_eh m_predecessor_eh; + const datalog::t_unfold_eh m_unfold_eh; + + public: + user_callback(context &context, + void *state, + const datalog::t_new_lemma_eh new_lemma_eh, + const datalog::t_predecessor_eh predecessor_eh, + const datalog::t_unfold_eh unfold_eh) : + spacer_callback(context), + m_state(state), + m_new_lemma_eh(new_lemma_eh), + m_predecessor_eh(predecessor_eh), + m_unfold_eh(unfold_eh) {} + + inline bool new_lemma() override { return true; } + + void new_lemma_eh(expr *lemma, unsigned level) override; + + inline bool predecessor() override { return true; } + + void predecessor_eh() override; + + inline bool unfold() override { return true; } + + void unfold_eh() override; + + }; + +} + + +#endif //_SPACER_CALLBACK_H_ diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index eba51c793..726edadc1 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -1178,7 +1178,7 @@ 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_pob(nullptr) { + m_pob(nullptr), m_external(false) { SASSERT(m_body); normalize(m_body, m_body); } @@ -1187,7 +1187,7 @@ 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_pob(p) { + m_pob(p), m_external(false) { SASSERT(m_pob); m_pob->get_skolems(m_zks); add_binding(m_pob->get_binding()); @@ -1198,7 +1198,7 @@ lemma::lemma(pob_ref const &p, expr_ref_vector &cube, unsigned lvl) : m(p->get_ast_manager()), m_body(m), m_cube(m), m_zks(m), m_bindings(m), m_lvl(p->level()), - m_pob(p) + m_pob(p), m_external(false) { if (m_pob) { m_pob->get_skolems(m_zks); @@ -1408,6 +1408,10 @@ bool pred_transformer::frames::add_lemma(lemma *lem) m_lemmas.push_back(lem); m_sorted = false; m_pt.add_lemma_core(lem); + + if (!lem->external()) { + m_pt.get_context().new_lemma_eh(m_pt, lem); + } return true; } @@ -2726,6 +2730,11 @@ lbool context::solve_core (unsigned from_lvl) if (lvl > 0 && !get_params ().spacer_skip_propagate ()) if (propagate(m_expanded_lvl, lvl, UINT_MAX)) { return l_false; } + for (unsigned i = 0; i < m_callbacks.size(); i++){ + if (m_callbacks[i]->unfold()) + m_callbacks[i]->unfold_eh(); + } + m_pob_queue.inc_level (); lvl = m_pob_queue.max_level (); m_stats.m_max_depth = std::max(m_stats.m_max_depth, lvl); @@ -3009,6 +3018,11 @@ lbool context::expand_node(pob& n) tout << "This pob can be blocked by instantiation\n";); } + for (unsigned i = 0; i < m_callbacks.size(); i++){ + if(m_callbacks[i]->predecessor()) + m_callbacks[i]->predecessor_eh(); + } + lbool res = n.pt ().is_reachable (n, &cube, &model, uses_level, is_concrete, r, reach_pred_used, num_reuse_reach); checkpoint (); @@ -3480,6 +3494,9 @@ void context::collect_statistics(statistics& st) const // -- time in creating new predecessors st.update ("time.spacer.solve.reach.children", m_create_children_watch.get_seconds ()); + st.update("spacer.random_seed", m_params.spacer_random_seed()); + st.update("spacer.lemmas_imported", m_stats.m_num_lemmas_imported); + st.update("spacer.lemmas_discarded", m_stats.m_num_lemmas_discarded); m_pm.collect_statistics(st); for (unsigned i = 0; i < m_lemma_generalizers.size(); ++i) { @@ -3588,8 +3605,38 @@ void context::add_constraints (unsigned level, const expr_ref& c) if (m.is_implies(c, e1, e2)) { SASSERT (is_app (e1)); pred_transformer *r = nullptr; - if (m_rels.find (to_app (e1)->get_decl (), r)) - { r->add_lemma(e2, level); } + if (m_rels.find (to_app (e1)->get_decl (), r)){ + lemma_ref lem = alloc(lemma, m, e2, level); + lem.get()->set_external(true); + if (r->add_lemma(lem.get())) { + this->m_stats.m_num_lemmas_imported++; + } + else{ + this->m_stats.m_num_lemmas_discarded++; + } + } + } + } +} + +void context::new_lemma_eh(pred_transformer &pt, lemma *lem) { + bool handle=false; + for (unsigned i = 0; i < m_callbacks.size(); i++) { + handle|=m_callbacks[i]->new_lemma(); + } + if (!handle) + return; + if ((is_infty_level(lem->level()) && m_params.spacer_share_invariants()) || + (!is_infty_level(lem->level()) && m_params.spacer_share_lemmas())) { + expr_ref_vector args(m); + for (unsigned i = 0; i < pt.sig_size(); ++i) { + args.push_back(m.mk_const(pt.get_manager().o2n(pt.sig(i), 0))); + } + expr *app = m.mk_app(pt.head(), pt.sig_size(), args.c_ptr()); + expr *lemma = m.mk_implies(app, lem->get_expr()); + for (unsigned i = 0; i < m_callbacks.size(); i++) { + if (m_callbacks[i]->new_lemma()) + m_callbacks[i]->new_lemma_eh(lemma, lem->level()); } } } diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h index e909cd9ad..8b8055ad5 100644 --- a/src/muz/spacer/spacer_context.h +++ b/src/muz/spacer/spacer_context.h @@ -28,7 +28,7 @@ Notes: #undef max #endif #include - +#include "util/scoped_ptr_vector.h" #include "muz/spacer/spacer_manager.h" #include "muz/spacer/spacer_prop_solver.h" @@ -114,6 +114,7 @@ class lemma { app_ref_vector m_bindings; unsigned m_lvl; pob_ref m_pob; + bool m_external; void mk_expr_core(); void mk_cube_core(); @@ -135,6 +136,9 @@ public: void add_skolem(app *zk, app* b); + inline void set_external(bool ext){m_external = ext;} + inline bool external() { return m_external;} + unsigned level () const {return m_lvl;} void set_level (unsigned lvl) {m_lvl = lvl;} app_ref_vector& get_bindings() {return m_bindings;} @@ -685,6 +689,32 @@ public: }; +class spacer_callback { +protected: + context &m_context; + +public: + spacer_callback(context &context) : m_context(context) {} + + virtual ~spacer_callback() = default; + + context &get_context() { return m_context; } + + virtual inline bool new_lemma() { return false; } + + virtual void new_lemma_eh(expr *lemma, unsigned level) {} + + virtual inline bool predecessor() { return false; } + + virtual void predecessor_eh() {} + + virtual inline bool unfold() { return false; } + + virtual void unfold_eh() {} + +}; + + class context { struct stats { @@ -697,6 +727,8 @@ class context { unsigned m_expand_node_undef; unsigned m_num_lemmas; unsigned m_num_restarts; + unsigned m_num_lemmas_imported; + unsigned m_num_lemmas_discarded; stats() { reset(); } void reset() { memset(this, 0, sizeof(*this)); } }; @@ -731,6 +763,7 @@ class context { bool m_weak_abs; bool m_use_restarts; unsigned m_restart_initial_threshold; + scoped_ptr_vector m_callbacks; // Functions used by search. lbool solve_core (unsigned from_lvl = 0); @@ -850,6 +883,10 @@ public: expr_ref get_constraints (unsigned lvl); void add_constraints (unsigned lvl, const expr_ref& c); + + void new_lemma_eh(pred_transformer &pt, lemma *lem); + + scoped_ptr_vector &callbacks() {return m_callbacks;} }; inline bool pred_transformer::use_native_mbp () {return ctx.use_native_mbp ();} diff --git a/src/muz/spacer/spacer_dl_interface.cpp b/src/muz/spacer/spacer_dl_interface.cpp index 52209454d..571687e16 100644 --- a/src/muz/spacer/spacer_dl_interface.cpp +++ b/src/muz/spacer/spacer_dl_interface.cpp @@ -34,6 +34,7 @@ Revision History: #include "model/model_smt2_pp.h" #include "ast/scoped_proof.h" #include "muz/transforms/dl_transforms.h" +#include "muz/spacer/spacer_callback.h" using namespace spacer; @@ -352,3 +353,10 @@ proof_ref dl_interface::get_proof() { return m_context->get_proof(); } + +void dl_interface::add_callback(void *state, + const datalog::t_new_lemma_eh new_lemma_eh, + const datalog::t_predecessor_eh predecessor_eh, + const datalog::t_unfold_eh unfold_eh){ + m_context->callbacks().push_back(alloc(user_callback, *m_context, state, new_lemma_eh, predecessor_eh, unfold_eh)); +} diff --git a/src/muz/spacer/spacer_dl_interface.h b/src/muz/spacer/spacer_dl_interface.h index e5a41427d..fb5ac3803 100644 --- a/src/muz/spacer/spacer_dl_interface.h +++ b/src/muz/spacer/spacer_dl_interface.h @@ -79,6 +79,11 @@ public: proof_ref get_proof() override; + void add_callback(void *state, + const datalog::t_new_lemma_eh new_lemma_eh, + const datalog::t_predecessor_eh predecessor_eh, + const datalog::t_unfold_eh unfold_eh); + }; }