fix drat for lookahead, fixes for binary drat format

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/sat/sat_drat.cpp

@@ -43,6 +43,8 @@ namespace sat {
     }
 
     drat::~drat() {
+        if (m_out) m_out->flush();
+        if (m_bout) m_bout->flush();
         dealloc(m_out);
         dealloc(m_bout);
         for (unsigned i = 0; i < m_proof.size(); ++i) {
@@ -83,8 +85,8 @@ namespace sat {
     void drat::bdump(unsigned n, literal const* c, status st) {
         unsigned char ch = 0;
         switch (st) {
-        case status::asserted: UNREACHABLE(); return;
+        case status::asserted: return;
-        case status::external: UNREACHABLE(); return; // requires extension to drat format.
+        case status::external: return; 
         case status::learned: ch = 'a'; break;
         case status::deleted: ch = 'd'; break;
         default: UNREACHABLE(); break;
@@ -104,7 +106,7 @@ namespace sat {
             while (v);
         }
         ch = 0;
-        (*m_bout) << 0;
+        (*m_bout) << ch;
     }
 
     bool drat::is_cleaned(clause& c) const {
@@ -615,8 +617,7 @@ namespace sat {
         literal ls[2] = {l1, l2};
         if (m_out) dump(2, ls, status::deleted);
         if (m_bout) bdump(2, ls, status::deleted);
-        if (m_check) 
+        if (m_check) append(l1, l2, status::deleted);
-            append(l1, l2, status::deleted);
     }
 
     void drat::del(clause& c) {

src/sat/sat_lookahead.cpp

@@ -113,7 +113,7 @@ namespace sat {
         if (m_search_mode == lookahead_mode::searching) {
             m_assumptions.push_back(l1);
             m_assumptions.push_back(l2);
-            m_drat.add(m_assumptions);
+            m_s.m_drat.add(m_assumptions);
             m_assumptions.pop_back();
             m_assumptions.pop_back();
         }
@@ -1032,7 +1032,7 @@ namespace sat {
         for (unsigned i = 0; i < trail_sz; ++i) {
             literal l = m_s.m_trail[i];
             if (!m_s.was_eliminated(l.var())) {
-                if (m_s.m_config.m_drat) m_drat.add(l, false);
+                if (m_s.m_config.m_drat) m_s.m_drat.add(l, false);
                 assign(l);
             }
         }
@@ -1065,7 +1065,7 @@ namespace sat {
             case 3: add_ternary(c[0],c[1],c[2]); break;
             default: if (!learned) add_clause(c); break;
             }
-            if (m_s.m_config.m_drat) m_drat.add(c, false);
+            // if (m_s.m_config.m_drat) m_s.m_drat.add(c, false);
         }
     }
 
@@ -1927,7 +1927,7 @@ namespace sat {
     void lookahead::validate_assign(literal l) {
         if (m_s.m_config.m_drat && m_search_mode == lookahead_mode::searching) {
             m_assumptions.push_back(l);
-            m_drat.add(m_assumptions);
+            m_s.m_drat.add(m_assumptions);
             m_assumptions.pop_back();
         }
     }

src/sat/sat_lookahead.h

@@ -200,7 +200,6 @@ namespace sat {
         double                 m_delta_decrease;
         double                 m_delta_fraction;
 
-        drat                   m_drat;
         literal_vector         m_assumptions;
 
         literal_vector         m_trail;         // trail of units
@@ -565,7 +564,6 @@ namespace sat {
         lookahead(solver& s) : 
             m_s(s),
             m_num_vars(s.num_vars()),
-            m_drat(s),
             m_num_tc1(0),
             m_level(2),
             m_last_prefix_length(0),

src/solver/parallel_tactic.cpp

@@ -330,6 +330,7 @@ private:
     volatile bool m_has_undef;
     bool          m_allsat;
     unsigned      m_num_unsat;
+    unsigned      m_last_depth;
     int           m_exn_code;
     std::string   m_exn_msg;
 
@@ -340,7 +341,8 @@ private:
         m_has_undef = false;
         m_allsat = false;
         m_branches = 0;    
-        m_num_unsat = 0;    
+        m_num_unsat = 0;
+        m_last_depth = 0;
         m_backtrack_frequency = pp.conquer_backtrack_frequency();
         m_conquer_delay = pp.conquer_delay();
         m_exn_code = 0;
@@ -350,9 +352,10 @@ private:
 
     void log_branches(lbool status) {
         IF_VERBOSE(0, verbose_stream() << "(tactic.parallel :progress " << m_progress << "% ";
-                   if (status == l_true)  verbose_stream() << ":status sat ";
+                   if (status == l_true)  verbose_stream() << ":status sat";
-                   if (status == l_undef) verbose_stream() << ":status unknown ";
+                   if (status == l_undef) verbose_stream() << ":status unknown";
-                   verbose_stream() << ":closed " << m_num_unsat << " :open " << m_branches << ")\n";);
+                   if (m_num_unsat > 0) verbose_stream() << " :closed " << m_num_unsat << "@" << m_last_depth;
+                   verbose_stream() << " :open " << m_branches << ")\n";);
     }
 
     void add_branches(unsigned b) {
@@ -405,13 +408,14 @@ private:
         }
     }
 
-    void inc_unsat() {
+    void inc_unsat(solver_state& s) {
         std::lock_guard<std::mutex> lock(m_mutex);
         ++m_num_unsat;
+        m_last_depth = s.get_depth();
     }
 
     void report_unsat(solver_state& s) {        
-        inc_unsat();
+        inc_unsat(s);
         close_branch(s, l_false);
         if (s.has_assumptions()) {
             expr_ref_vector core(s.m());
@@ -489,7 +493,7 @@ private:
                     IF_VERBOSE(0, verbose_stream() << "(tactic.parallel :backtrack " << cutoff << " -> " << c.size() << ")\n");
                     cutoff = c.size();
                 }
-                inc_unsat();
+                inc_unsat(s);
                 log_branches(l_false);
                 break;