From ef6542823b400b98db192282a49ae932ad880980 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 28 Sep 2020 20:01:33 -0700
Subject: [PATCH] unit optimization

---
 src/sat/smt/sat_dual_solver.cpp | 8 ++++++--
 src/sat/smt/sat_dual_solver.h   | 4 ++--
 2 files changed, 8 insertions(+), 4 deletions(-)

diff --git a/src/sat/smt/sat_dual_solver.cpp b/src/sat/smt/sat_dual_solver.cpp
index deb1fe4db..e80bb0301 100644
--- a/src/sat/smt/sat_dual_solver.cpp
+++ b/src/sat/smt/sat_dual_solver.cpp
@@ -26,17 +26,20 @@ namespace sat {
         m_solver.user_push(); 
         m_roots_lim.push_back(m_roots.size());     
         m_tracked_lim.push_back(m_tracked_stack.size());
+        m_units_lim.push_back(m_units.size());
     }
 
     void dual_solver::pop(unsigned num_scopes) {
         m_solver.user_pop(num_scopes);
         unsigned old_sz = m_roots_lim.size() - num_scopes;
-        m_roots.shrink(m_roots_lim[old_sz]);
-        m_roots_lim.shrink(old_sz);
         for (unsigned v = m_tracked_stack.size(); v-- > m_tracked_lim[old_sz]; ) 
             m_is_tracked[v] = false; 
+        m_roots.shrink(m_roots_lim[old_sz]);
         m_tracked_stack.shrink(m_tracked_lim[old_sz]);
+        m_units.shrink(m_units_lim[old_sz]);
+        m_roots_lim.shrink(old_sz);
         m_tracked_lim.shrink(old_sz);
+        m_units_lim.shrink(old_sz);
     }
 
     bool_var dual_solver::ext2var(bool_var v) {
@@ -87,6 +90,7 @@ namespace sat {
             m_lits.push_back(literal(v, l_false == s.value(m_var2ext[v])));
         lbool is_sat = m_solver.check(m_lits.size(), m_lits.c_ptr());
         m_core.reset();
+        m_core.append(m_units);
         if (is_sat == l_false) 
             for (literal lit : m_solver.get_core())
                 m_core.push_back(lit2ext(lit));
diff --git a/src/sat/smt/sat_dual_solver.h b/src/sat/smt/sat_dual_solver.h
index 76197c234..4133dfeb3 100644
--- a/src/sat/smt/sat_dual_solver.h
+++ b/src/sat/smt/sat_dual_solver.h
@@ -21,12 +21,12 @@ namespace sat {
 
     class dual_solver {
         solver          m_solver;
-        literal_vector  m_roots, m_lits, m_core;
+        literal_vector  m_roots, m_lits, m_core, m_units;
         bool_var_vector m_is_tracked;
         unsigned_vector m_tracked_stack;
         unsigned_vector m_ext2var;
         unsigned_vector m_var2ext;
-        unsigned_vector m_roots_lim, m_tracked_lim;
+        unsigned_vector m_roots_lim, m_tracked_lim, m_units_lim;
         void add_literal(literal lit);
 
         bool_var ext2var(bool_var v);