mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 12:23:38 +00:00
Code Activity

revert some changes that coincide with breaking macos build

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-08-25 11:22:25 -07:00
parent a628e4c4e5
commit 5f2387b3be
3 changed files with 10 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/sat/sat_config.cpp
View file

@ -32,7 +32,7 @@ namespace sat {
void config::updt_params(params_ref const & _p) { void config::updt_params(params_ref const & _p) {
sat_params p(_p); sat_params p(_p);
solver_params sp(_p); // solver_params sp(_p);
m_max_memory = megabytes_to_bytes(p.max_memory()); 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_unsat = p.drat_check_unsat();
m_drat_check_sat = p.drat_check_sat(); m_drat_check_sat = p.drat_check_sat();
m_drat_file = p.drat_file(); 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_binary = p.drat_binary();
m_drat_activity = p.drat_activity(); m_drat_activity = p.drat_activity();
m_drup_trim = p.drup_trim(); m_drup_trim = p.drup_trim();

14
src/sat/sat_drat.cpp
View file

@ -35,7 +35,7 @@ namespace sat {
if (s.get_config().m_drat_binary) if (s.get_config().m_drat_binary)
std::swap(m_out, m_bout); std::swap(m_out, m_bout);
} }
m_print_clause = nullptr; // m_print_clause = nullptr;
} }
drat::~drat() { drat::~drat() {
@ -691,7 +691,7 @@ namespace sat {
if (m_out) dump(1, &l, st); if (m_out) dump(1, &l, st);
if (m_bout) bdump(1, &l, st); if (m_bout) bdump(1, &l, st);
if (m_check) append(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) { void drat::add(literal l1, literal l2, status st) {
if (st.is_deleted()) if (st.is_deleted())
@ -702,7 +702,7 @@ namespace sat {
if (m_out) dump(2, ls, st); if (m_out) dump(2, ls, st);
if (m_bout) bdump(2, ls, st); if (m_bout) bdump(2, ls, st);
if (m_check) append(l1, l2, 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) { void drat::add(clause& c, status st) {
if (st.is_deleted()) if (st.is_deleted())
@ -712,7 +712,7 @@ namespace sat {
if (m_out) dump(c.size(), c.begin(), st); if (m_out) dump(c.size(), c.begin(), st);
if (m_bout) bdump(c.size(), c.begin(), st); if (m_bout) bdump(c.size(), c.begin(), st);
if (m_check) append(mk_clause(c), 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) { void drat::add(literal_vector const& lits, status st) {
@ -734,8 +734,7 @@ namespace sat {
if (m_out) if (m_out)
dump(sz, lits, st); dump(sz, lits, st);
if (m_print_clause) //if (m_print_clause) m_print_clause(sz, lits, st);
m_print_clause(sz, lits, st);
} }
void drat::add(literal_vector const& c) { void drat::add(literal_vector const& c) {
@ -755,8 +754,7 @@ namespace sat {
} }
} }
} }
if (m_print_clause) // if (m_print_clause) m_print_clause(c.size(), c.data(), status::redundant());
m_print_clause(c.size(), c.data(), status::redundant());
} }
void drat::del(literal l) { void drat::del(literal l) {

4
src/sat/sat_drat.h
View file

@ -73,7 +73,7 @@ namespace sat {
watched_clause(clause* c, literal l1, literal l2): watched_clause(clause* c, literal l1, literal l2):
m_clause(c), m_l1(l1), m_l2(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; svector<watched_clause> m_watched_clauses;
typedef svector<unsigned> watch; typedef svector<unsigned> watch;
solver& s; solver& s;
@ -141,7 +141,7 @@ namespace sat {
void add(unsigned sz, literal const* lits, status st); void add(unsigned sz, literal const* lits, status st);
void set_print_clause(std::function<void(unsigned, literal const*, status)>& print_clause) { 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 // support for SMT - connect Boolean variables with AST nodes