From c8e655830f59785aae19710282292cf6ca8b57ac Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 1 Dec 2017 10:13:54 -0800
Subject: [PATCH] add statistics to cubing

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/sat_lookahead.cpp | 12 ++++++++++--
 src/sat/sat_lookahead.h   | 10 +++++++++-
 src/sat/sat_solver.cpp    |  1 +
 3 files changed, 20 insertions(+), 3 deletions(-)

diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp
index 7464c4156..2a2da1c90 100644
--- a/src/sat/sat_lookahead.cpp
+++ b/src/sat/sat_lookahead.cpp
@@ -2013,6 +2013,11 @@ namespace sat {
         return true;
     }
 
+    void lookahead::update_cube_statistics(statistics& st) {
+        st.update("lh cube cutoffs", m_cube_state.m_cutoffs);
+        st.update("lh cube conflicts", m_cube_state.m_conflicts);        
+    }
+
     lbool lookahead::cube(bool_var_vector const& vars, literal_vector& lits, unsigned backtrack_level) {
         scoped_ext _scoped_ext(*this);
         lits.reset();
@@ -2031,6 +2036,7 @@ namespace sat {
         unsigned depth = 0;
         unsigned init_trail = m_trail.size();
         
+        m_cube_state.reset_stats();
         if (!is_first) {
             goto pick_up_work;
         }
@@ -2041,8 +2047,9 @@ namespace sat {
             inc_istamp();
             if (inconsistent()) {
                 TRACE("sat", tout << "inconsistent: " << m_cube_state.m_cube << "\n";);
-                m_cube_state.m_freevars_threshold = m_freevars.size();                
-                if (!backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision)) return l_false;
+                m_cube_state.m_freevars_threshold = m_freevars.size();               
+                m_cube_state.inc_conflict();
+                if (!backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision)) return l_false;                
                 continue;
             }
         pick_up_work:
@@ -2059,6 +2066,7 @@ namespace sat {
                 (m_config.m_cube_cutoff == 0 && m_freevars.size() < m_cube_state.m_freevars_threshold)) {
                 m_cube_state.m_freevars_threshold *= (1.0 - pow(m_config.m_cube_fraction, depth));
                 set_conflict();
+                m_cube_state.inc_cutoff();
 #if 0
                 // return cube of all literals, not just the ones in the main cube
                 lits.append(m_trail.size() - init_trail, m_trail.c_ptr() + init_trail);
diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h
index 6f0c256a7..2f62c932d 100644
--- a/src/sat/sat_lookahead.h
+++ b/src/sat/sat_lookahead.h
@@ -167,13 +167,19 @@ namespace sat {
             svector<bool>  m_is_decision;
             literal_vector m_cube;
             double         m_freevars_threshold;
+            unsigned       m_conflicts;
+            unsigned       m_cutoffs;
             cube_state() { reset(); }
             void reset() { 
                 m_first = true;
                 m_is_decision.reset(); 
                 m_cube.reset(); 
-                m_freevars_threshold = 0; 
+                m_freevars_threshold = 0;
+                reset_stats();
             }
+            void reset_stats() { m_conflicts = 0; m_cutoffs = 0; }
+            void inc_conflict() { ++m_conflicts; }
+            void inc_cutoff() { ++m_cutoffs; }
         };
 
         config                 m_config;
@@ -572,6 +578,8 @@ namespace sat {
 
         lbool cube(bool_var_vector const& vars, literal_vector& lits, unsigned backtrack_level);
 
+        void update_cube_statistics(statistics& st);
+
         literal select_lookahead(literal_vector const& assumptions, bool_var_vector const& vars);
         /**
            \brief simplify set of clauses by extracting units from a lookahead at base level.
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 89acdc408..5a7e234e9 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -859,6 +859,7 @@ namespace sat {
             m_cuber = alloc(lookahead, *this);
         }
         lbool result = m_cuber->cube(vars, lits, backtrack_level);
+        m_cuber->update_cube_statistics(m_aux_stats);
         if (result == l_false) {
             dealloc(m_cuber);
             m_cuber = nullptr;