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

@@ -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<datalog::t_new_lemma_eh>(new_lemma_eh),
+                                                     reinterpret_cast<datalog::t_predecessor_eh>(predecessor_eh),
+                                                     reinterpret_cast<datalog::t_unfold_eh>(unfold_eh));
+
+        Z3_CATCH;
+    }
+
 #include "api_datalog_spacer.inc"
 
 };

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);
+
     /*@}*/
     /*@}*/
 

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:
 
         /**

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() {}

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"),
+))
 
 
 

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

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);
+    }
+
+}

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_

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))
+            if (m_rels.find (to_app (e1)->get_decl (), r)){
-            { r->add_lemma(e2, level); }
+                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());
         }
     }
 }

src/muz/spacer/spacer_context.h

@@ -28,7 +28,7 @@ Notes:
 #undef max
 #endif
 #include <queue>
-
+#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<spacer_callback> 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<spacer_callback> &callbacks() {return m_callbacks;}
 };
 
 inline bool pred_transformer::use_native_mbp () {return ctx.use_native_mbp ();}

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));
+}

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);
+
 };
 }