From 5f2387b3be9ea974bd95b17899d099fd7344c293 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 25 Aug 2022 11:22:25 -0700
Subject: [PATCH] revert some changes that coincide with breaking macos build

---
 src/sat/sat_config.cpp |  4 ++--
 src/sat/sat_drat.cpp   | 14 ++++++--------
 src/sat/sat_drat.h     |  4 ++--
 3 files changed, 10 insertions(+), 12 deletions(-)

diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp
index b911ee971b1..b3bd11999bc 100644
--- a/src/sat/sat_config.cpp
+++ b/src/sat/sat_config.cpp
@@ -32,7 +32,7 @@ namespace sat {
 
     void config::updt_params(params_ref const & _p) {
         sat_params p(_p);
-        solver_params sp(_p);
+        // solver_params sp(_p);
 
         m_max_memory  = megabytes_to_bytes(p.max_memory());
 
@@ -197,7 +197,7 @@ namespace sat {
         m_drat_check_unsat  = p.drat_check_unsat();
         m_drat_check_sat  = p.drat_check_sat();
         m_drat_file       = p.drat_file();
-        m_drat            = !p.drat_disable() && (sp.lemmas2console() || m_drat_check_unsat || m_drat_file.is_non_empty_string() || m_drat_check_sat) && p.threads() == 1;
+        m_drat            = !p.drat_disable() && (/*sp.lemmas2console() || */ m_drat_check_unsat || m_drat_file.is_non_empty_string() || m_drat_check_sat) && p.threads() == 1;
         m_drat_binary     = p.drat_binary();
         m_drat_activity   = p.drat_activity();
         m_drup_trim       = p.drup_trim();
diff --git a/src/sat/sat_drat.cpp b/src/sat/sat_drat.cpp
index 0130676db33..3b52b0f7f81 100644
--- a/src/sat/sat_drat.cpp
+++ b/src/sat/sat_drat.cpp
@@ -35,7 +35,7 @@ namespace sat {
             if (s.get_config().m_drat_binary) 
                 std::swap(m_out, m_bout);            
         }
-        m_print_clause = nullptr;
+        // m_print_clause = nullptr;
     }
 
     drat::~drat() {
@@ -691,7 +691,7 @@ namespace sat {
         if (m_out) dump(1, &l, st);
         if (m_bout) bdump(1, &l, st);
         if (m_check) append(l, st);
-        if (m_print_clause) m_print_clause(1, &l, st);
+        //if (m_print_clause) m_print_clause(1, &l, st);
     }
     void drat::add(literal l1, literal l2, status st) {
         if (st.is_deleted())
@@ -702,7 +702,7 @@ namespace sat {
         if (m_out) dump(2, ls, st);
         if (m_bout) bdump(2, ls, st);
         if (m_check) append(l1, l2, st);
-        if (m_print_clause) m_print_clause(2, ls, st);
+        //if (m_print_clause) m_print_clause(2, ls, st);
     }
     void drat::add(clause& c, status st) {
         if (st.is_deleted())
@@ -712,7 +712,7 @@ namespace sat {
         if (m_out) dump(c.size(), c.begin(), st);
         if (m_bout) bdump(c.size(), c.begin(), st);
         if (m_check) append(mk_clause(c), st);
-        if (m_print_clause) m_print_clause(c.size(), c.begin(), st);
+        //if (m_print_clause) m_print_clause(c.size(), c.begin(), st);
     }
     
     void drat::add(literal_vector const& lits, status st) {
@@ -734,8 +734,7 @@ namespace sat {
         if (m_out)
             dump(sz, lits, st);
 
-        if (m_print_clause) 
-            m_print_clause(sz, lits, st);
+        //if (m_print_clause) m_print_clause(sz, lits, st);
     }
 
     void drat::add(literal_vector const& c) {
@@ -755,8 +754,7 @@ namespace sat {
             }
             }
         }
-        if (m_print_clause)
-            m_print_clause(c.size(), c.data(), status::redundant());
+        // if (m_print_clause) m_print_clause(c.size(), c.data(), status::redundant());
     }
 
     void drat::del(literal l) {
diff --git a/src/sat/sat_drat.h b/src/sat/sat_drat.h
index d48833099db..04c639b073c 100644
--- a/src/sat/sat_drat.h
+++ b/src/sat/sat_drat.h
@@ -73,7 +73,7 @@ namespace sat {
             watched_clause(clause* c, literal l1, literal l2):
                 m_clause(c), m_l1(l1), m_l2(l2) {}
         };
-        std::function<void(unsigned, literal const*, status)> m_print_clause;
+        // std::function<void(unsigned, literal const*, status)> m_print_clause;
         svector<watched_clause>   m_watched_clauses;
         typedef svector<unsigned> watch;
         solver& s;
@@ -141,7 +141,7 @@ namespace sat {
         void add(unsigned sz, literal const* lits, status st);
 
         void set_print_clause(std::function<void(unsigned, literal const*, status)>& print_clause) {
-            m_print_clause = print_clause;
+            // m_print_clause = print_clause;
         }
 
         // support for SMT - connect Boolean variables with AST nodes