From 9d0aa4d02d3c2fb5c33abbffa55358bed8e65f33 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 1 Oct 2018 20:22:02 -0700
Subject: [PATCH] update empty cube case for sat/undef cases

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/sat_lookahead.cpp             | 20 ++++++++++----------
 src/sat/sat_lookahead.h               |  2 ++
 src/sat/sat_solver.cpp                |  1 +
 src/sat/sat_solver/inc_sat_solver.cpp | 25 +++++++++++++++++--------
 4 files changed, 30 insertions(+), 18 deletions(-)

diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp
index bbc1106bb..a6ff6a3b0 100644
--- a/src/sat/sat_lookahead.cpp
+++ b/src/sat/sat_lookahead.cpp
@@ -2057,6 +2057,15 @@ namespace sat {
         return h;
     }
 
+    bool lookahead::should_cutoff(unsigned depth) {
+        return depth > 0 && 
+            ((m_config.m_cube_cutoff == depth_cutoff && depth == m_config.m_cube_depth) ||
+             (m_config.m_cube_cutoff == freevars_cutoff && m_freevars.size() <= m_init_freevars * m_config.m_cube_freevars) ||
+             (m_config.m_cube_cutoff == psat_cutoff && psat_heur() >= m_config.m_cube_psat_trigger) ||
+             (m_config.m_cube_cutoff == adaptive_freevars_cutoff && m_freevars.size() < m_cube_state.m_freevars_threshold) ||
+             (m_config.m_cube_cutoff == adaptive_psat_cutoff && psat_heur() >= m_cube_state.m_psat_threshold));
+    }
+
     lbool lookahead::cube(bool_var_vector& vars, literal_vector& lits, unsigned backtrack_level) {
         scoped_ext _scoped_ext(*this);
         lits.reset();
@@ -2102,22 +2111,13 @@ namespace sat {
             }
             backtrack_level = UINT_MAX;
             depth = m_cube_state.m_cube.size();
-            if ((m_config.m_cube_cutoff == depth_cutoff && depth == m_config.m_cube_depth) ||
-                (m_config.m_cube_cutoff == freevars_cutoff && m_freevars.size() <= m_init_freevars * m_config.m_cube_freevars) ||
-                (m_config.m_cube_cutoff == psat_cutoff && psat_heur() >= m_config.m_cube_psat_trigger) ||
-                (m_config.m_cube_cutoff == adaptive_freevars_cutoff && m_freevars.size() < m_cube_state.m_freevars_threshold) ||
-                (m_config.m_cube_cutoff == adaptive_psat_cutoff && psat_heur() >= m_cube_state.m_psat_threshold)) {
+            if (should_cutoff(depth)) {
                 double dec = (1.0 - pow(m_config.m_cube_fraction, depth));
                 m_cube_state.m_freevars_threshold *= dec;
                 m_cube_state.m_psat_threshold *= 2.0 - dec;
                 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);
-#else
                 lits.append(m_cube_state.m_cube);
-#endif
                 vars.reset();
                 for (auto v : m_freevars) if (in_reduced_clause(v)) vars.push_back(v);
                 backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision);
diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h
index df954bdf1..c2282e779 100644
--- a/src/sat/sat_lookahead.h
+++ b/src/sat/sat_lookahead.h
@@ -558,6 +558,8 @@ namespace sat {
 
         double psat_heur();
 
+        bool should_cutoff(unsigned depth);
+
     public:
         lookahead(solver& s) : 
             m_s(s),
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index b58d2296b..b65abd41c 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -1030,6 +1030,7 @@ namespace sat {
             }
             break;
         case l_true: {
+            lits.reset();
             pop_to_base_level();
             model const& mdl = m_cuber->get_model();
             for (bool_var v = 0; v < mdl.size(); ++v) {
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index 5de64b496..7a77e3b4e 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -308,6 +308,12 @@ public:
         return nullptr;
     }
 
+    expr_ref_vector last_cube() {
+        expr_ref_vector result(m);
+        result.push_back(m.mk_false());
+        return result;
+    }
+
     expr_ref_vector cube(expr_ref_vector& vs, unsigned backtrack_level) override {
         if (!is_internalized()) {
             lbool r = internalize_formulas();
@@ -326,15 +332,18 @@ public:
         }
         sat::literal_vector lits;
         lbool result = m_solver.cube(vars, lits, backtrack_level);
-        if (result == l_false || lits.empty()) {
-            expr_ref_vector result(m);
-            result.push_back(m.mk_false());
-            return result;
-        }
-        if (result == l_true) {
-            IF_VERBOSE(1, verbose_stream() << "formulas are SAT\n");
+        switch (result) {
+        case l_true:
             return expr_ref_vector(m);
-        }        
+        case l_false: 
+            return last_cube();
+        default: 
+            SASSERT(!lits.empty());
+            if (lits.empty()) {
+                IF_VERBOSE(0, verbose_stream() << "empty cube for undef\n";);
+            }
+            break;
+        }
         expr_ref_vector fmls(m);
         expr_ref_vector lit2expr(m);
         lit2expr.resize(m_solver.num_vars() * 2);