revert some changes that coincide with breaking macos build

Z3Prover · Aug 25, 2022 · 5f2387b · 5f2387b
1 parent a628e4c
commit 5f2387b
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 12 deletions.
diff --git 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
@@ -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
@@ -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