Adding stats to lackr.

src/ackr/lackr.cpp

@@ -73,7 +73,7 @@ struct simp_wrap {
 };
 
 
-lackr::lackr(ast_manager& m, params_ref p, expr_ref _f)
+lackr::lackr(ast_manager& m, params_ref p, lackr_stats& st, expr_ref _f)
     : m_m(m)
     , m_p(p)
     , m_fla(m)
@@ -83,6 +83,7 @@ lackr::lackr(ast_manager& m, params_ref p, expr_ref _f)
     , m_simp(m)
     , m_ackrs(m)
     , m_cancel(0)
+    , m_st(st)
 {
     m_fla = _f;
     updt_params(p);
@@ -157,7 +158,9 @@ bool lackr::ackr(app * const t1, app * const t2) {
     m_info->abstract(cg, cga);
     m_simp(cga);
     TRACE("lackr", tout << "ackr constr abs:" << mk_ismt2_pp(cga, m_m, 2) << "\n";);
-    if (!m_m.is_true(cga)) m_ackrs.push_back(cga);
+    if (m_m.is_true(cga)) return true;
+    m_st.m_ackrs_sz++;
+    m_ackrs.push_back(cga);
     return true;
 }
 
@@ -229,12 +232,12 @@ void lackr::add_term(app* a) {
 
 
 lbool lackr::eager() {
-    if (!eager_enc()) return l_undef;
     m_sat->assert_expr(m_abstr);
     TRACE("lackr", tout << "run sat 0\n"; );
     if (m_sat->check_sat(0, 0) == l_false)
         return l_false;
     checkpoint();
+    if (!eager_enc()) return l_undef;
     expr_ref all(m_m);
     all = m_m.mk_and(m_ackrs.size(), m_ackrs.c_ptr());
     m_simp(all);
@@ -247,12 +250,11 @@ lbool lackr::eager() {
 lbool lackr::lazy() {
     lackr_model_constructor mc(m_m, m_info);
     m_sat->assert_expr(m_abstr);
-    unsigned ackr_head = 0;
-    unsigned it = 0;
+    unsigned ackr_head = 0;    
     while (1) {
+        m_st.m_it++;
         checkpoint();
-        //std::cout << "it: " << ++it << "\n";
-        TRACE("lackr", tout << "lazy check\n";);
+        TRACE("lackr", tout << "lazy check: " << m_st.m_it << "\n";);
         const lbool r = m_sat->check_sat(0, 0);
         if (r == l_undef) return l_undef; // give up
         if (r == l_false) return l_false; // abstraction unsat

src/ackr/lackr.h

@@ -28,27 +28,36 @@
 #include"bv_decl_plugin.h"
 #include"cooperate.h"
 
+struct lackr_stats {
+    lackr_stats() : m_it(0), m_ackrs_sz(0) {}
+    void reset() { m_it = m_ackrs_sz = 0; }
+    unsigned    m_it;       // number of lazy iterations
+    unsigned    m_ackrs_sz; // number of congruence constraints
+};
+
 class lackr {
     public:
-        lackr(ast_manager& m, params_ref p, expr_ref _f);
-        lbool operator() ();
+        lackr(ast_manager& m, params_ref p,lackr_stats& st,
+            expr_ref _f);
         ~lackr();
-        inline ackr_info_ref get_info() { return m_info; }
-        inline model_ref get_model() { return m_model; }
-
         void updt_params(params_ref const & _p) {
             ackr_params p(_p);
             m_eager = p.eager();
             m_use_sat = p.sat_backend();
         }
+        lbool operator() ();
+
+        //
+        // getters
+        //
+        inline ackr_info_ref get_info() { return m_info; }
+        inline model_ref get_model() { return m_model; }
 
         //
         //  timeout mechanisms
         //
-
         void checkpoint() {
-            if (m_cancel)
-                throw tactic_exception(TACTIC_CANCELED_MSG);
+            if (m_cancel) throw tactic_exception(TACTIC_CANCELED_MSG);
             cooperate("lackr");
         }
 
@@ -78,6 +87,7 @@ class lackr {
         volatile bool                        m_cancel;
         bool                                 m_eager;
         bool                                 m_use_sat;
+        lackr_stats&                         m_st;
 
         bool init();
         void setup_sat();

src/ackr/lackr_tactic.cpp

@@ -28,6 +28,7 @@ Revision History:
 #include"model_smt2_pp.h"
 #include"cooperate.h"
 #include"lackr.h"
+#include"ackr_params.hpp"
 #include"lackr_model_converter.h"
 
 class lackr_tactic : public tactic {
@@ -56,7 +57,7 @@ public:
         expr_ref f(m);
         f = m.mk_and(flas.size(), flas.c_ptr());
         // running implementation
-        m_imp = alloc(lackr, m, m_p, f);
+        m_imp = alloc(lackr, m, m_p, m_st, f);
         const lbool o = m_imp->operator()();
         flas.reset();
         // report result
@@ -68,7 +69,7 @@ public:
             model_ref abstr_model = m_imp->get_model();
             mc = mk_lackr_model_converter(m, m_imp->get_info(), abstr_model);
         }
-        // clenup
+        // cleanup
         lackr * d = m_imp;
         #pragma omp critical (lackr)
         {
@@ -77,6 +78,14 @@ public:
         dealloc(d);
     }
 
+    virtual void collect_statistics(statistics & st) const {
+        ackr_params p(m_p);       
+        if (!p.eager()) st.update("lackr-its", m_st.m_it);
+        st.update("ackr-constraints", m_st.m_ackrs_sz);
+    }
+
+    virtual void reset_statistics() { m_st.reset(); }
+
     virtual void cleanup() { }
 
     virtual tactic* translate(ast_manager& m) {
@@ -91,6 +100,7 @@ private:
     ast_manager&                         m_m;
     params_ref                           m_p;
     lackr*                               m_imp;
+    lackr_stats                          m_st;
 };
 
 tactic * mk_lackr_tactic(ast_manager & m, params_ref const & p) {