From 7c2fe46eb72ebaed1614af71cd0ae58dd724de8f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 2 Sep 2020 12:35:12 -0700 Subject: [PATCH] build fix --- src/sat/sat_drat.cpp | 44 ++++++++++++++------------------- src/sat/sat_solver.cpp | 2 +- src/sat/sat_types.h | 27 +++++++++++--------- src/sat/smt/ba_solver.cpp | 6 ++--- src/sat/smt/euf_ackerman.cpp | 4 +-- src/sat/smt/euf_internalize.cpp | 10 ++++---- src/sat/smt/euf_proof.cpp | 2 +- 7 files changed, 46 insertions(+), 49 deletions(-) diff --git a/src/sat/sat_drat.cpp b/src/sat/sat_drat.cpp index a3e5fb0ee..f3557c14f 100644 --- a/src/sat/sat_drat.cpp +++ b/src/sat/sat_drat.cpp @@ -76,11 +76,11 @@ namespace sat { else if (st.is_asserted()) out << "a"; - switch (st.orig) { - case status::orig::ba: return out << " ba"; - case status::orig::euf: return out << " euf"; - default: return out; - } + if (st.is_ba()) + out << " ba"; + else if (st.is_euf()) + out << " euf"; + return out; } void drat::dump(unsigned n, literal const* c, status st) { @@ -94,32 +94,25 @@ namespace sat { char* lastd = digits + sizeof(digits); unsigned len = 0; - switch (st.st) { - case status::st::asserted: + if (st.is_asserted()) { buffer[len++] = 'a'; buffer[len++] = ' '; - break; - case status::st::deleted: + } + else if (st.is_deleted()) { buffer[len++] = 'd'; buffer[len++] = ' '; - break; - default: - break; } - switch (st.orig) { - case status::orig::euf: + + if (st.is_euf()) { buffer[len++] = 'e'; buffer[len++] = 'u'; buffer[len++] = 'f'; buffer[len++] = ' '; - break; - case status::orig::ba: + } + else if (st.is_ba()) { buffer[len++] = 'b'; buffer[len++] = 'a'; buffer[len++] = ' '; - break; - default: - break; } for (unsigned i = 0; i < n; ++i) { literal lit = c[i]; @@ -160,12 +153,11 @@ namespace sat { void drat::bdump(unsigned n, literal const* c, status st) { unsigned char ch = 0; - switch (st.st) { - case status::st::asserted: return; - case status::st::redundant: ch = 'a'; break; - case status::st::deleted: ch = 'd'; break; - default: UNREACHABLE(); break; - } + if (st.is_redundant()) + ch = 'a'; + else if (st.is_deleted()) + ch = 'd'; + else return; char buffer[10000]; int len = 0; buffer[len++] = ch; @@ -497,7 +489,7 @@ namespace sat { clause& c = *m_proof[i]; unsigned j = 0; for (; j < c.size() && c[j] != ~l; ++j) {} - if (st.orig == status::orig::sat && j != c.size()) { + if (st.is_sat() && j != c.size()) { lits.append(j, c.begin()); lits.append(c.size() - j - 1, c.begin() + j + 1); if (!is_drup(lits.size(), lits.c_ptr())) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 101a44968..3474fb2b7 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -501,7 +501,7 @@ namespace sat { clause * solver::mk_nary_clause(unsigned num_lits, literal * lits, sat::status st) { m_stats.m_mk_clause++; clause * r = alloc_clause(num_lits, lits, st.is_redundant()); - SASSERT(!st.is_learned() || r->is_learned()); + SASSERT(!st.is_redundant() || r->is_learned()); bool reinit = attach_nary_clause(*r); if (reinit && !st.is_redundant()) push_reinit_stack(*r); if (st.is_redundant()) { diff --git a/src/sat/sat_types.h b/src/sat/sat_types.h index 258875ea9..18bc0e90b 100644 --- a/src/sat/sat_types.h +++ b/src/sat/sat_types.h @@ -254,26 +254,31 @@ namespace sat { class status { public: - enum class st { asserted, redundant, deleted } st; - enum class orig { sat, ba, euf } orig; - status(enum st s, enum orig o) : st(s), orig(o) {}; - status(status const& s) : st(s.st), orig(s.orig) {} - status(status&& s) noexcept { st = st::asserted; orig = orig::sat; std::swap(st, s.st); std::swap(orig, s.orig); } + enum class st { asserted, redundant, deleted }; + enum class orig { sat, ba, euf }; + st m_st; + orig m_orig; + public: + status(enum st s, enum orig o) : m_st(s), m_orig(o) {}; + status(status const& s) : m_st(s.m_st), m_orig(s.m_orig) {} + status(status&& s) noexcept { m_st = st::asserted; m_orig = orig::sat; std::swap(m_st, s.m_st); std::swap(m_orig, s.m_orig); } static status redundant() { return status(status::st::redundant, status::orig::sat); } static status asserted() { return status(status::st::asserted, status::orig::sat); } static status deleted() { return status(status::st::deleted, status::orig::sat); } - static status euf_learned() { return status(status::st::redundant, status::orig::euf); } - static status euf_asserted() { return status(status::st::asserted, status::orig::euf); } + static status euf(bool redundant) { return status(redundant ? st::redundant : st::asserted, orig::euf); } static status ba(bool redundant) { return redundant ? ba_redundant() : ba_asserted(); } static status ba_redundant() { return status(status::st::redundant, status::orig::ba); } static status ba_asserted() { return status(status::st::asserted, status::orig::ba); } - bool is_redundant() const { return st::redundant == st; } - bool is_asserted() const { return st::asserted == st; } - bool is_deleted() const { return st::deleted == st; } - bool operator==(status const& s) const { return s.orig == orig && s.st == st; } + bool is_redundant() const { return st::redundant == m_st; } + bool is_asserted() const { return st::asserted == m_st; } + bool is_deleted() const { return st::deleted == m_st; } + + bool is_sat() const { return orig::sat == m_orig; } + bool is_ba() const { return orig::ba == m_orig; } + bool is_euf() const { return orig::euf == m_orig; } }; diff --git a/src/sat/smt/ba_solver.cpp b/src/sat/smt/ba_solver.cpp index da6f9ae0e..642a6fb88 100644 --- a/src/sat/smt/ba_solver.cpp +++ b/src/sat/smt/ba_solver.cpp @@ -1598,7 +1598,7 @@ namespace sat { TRACE("ba", tout << m_lemma << "\n";); if (get_config().m_drat && m_solver) { - s().m_drat.add(m_lemma, sat::status::ba_redundant()); + s().m_drat.add(m_lemma, sat::status::ba(true)); } s().m_lemma.reset(); @@ -2140,7 +2140,7 @@ namespace sat { for (literal lit : r) lits.push_back(~lit); lits.push_back(l); - s().m_drat.add(lits, sat::status::ba_redundant()); + s().m_drat.add(lits, sat::status::ba(true)); } } @@ -2923,7 +2923,7 @@ namespace sat { } if (all_units && sz < k) { if (c.lit() == null_literal) { - s().mk_clause(0, nullptr, status::ba_redundant()); + s().mk_clause(0, nullptr, status::ba(c.learned())); } else { literal lit = ~c.lit(); diff --git a/src/sat/smt/euf_ackerman.cpp b/src/sat/smt/euf_ackerman.cpp index 6c8266459..ba85fb8c3 100644 --- a/src/sat/smt/euf_ackerman.cpp +++ b/src/sat/smt/euf_ackerman.cpp @@ -194,7 +194,7 @@ namespace euf { } expr_ref eq(m.mk_eq(a, b), m); lits.push_back(s.internalize(eq, false, false, true)); - s.s().mk_clause(lits, sat::status::euf_learned()); + s.s().mk_clause(lits, sat::status::euf(true)); } void ackerman::add_eq(expr* a, expr* b, expr* c) { @@ -205,6 +205,6 @@ namespace euf { lits[0] = s.internalize(eq1, true, false, true); lits[1] = s.internalize(eq2, true, false, true); lits[2] = s.internalize(eq3, false, false, true); - s.s().mk_clause(3, lits, sat::status::euf_learned()); + s.s().mk_clause(3, lits, sat::status::euf(true)); } } diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp index 5d615590a..8514d87ee 100644 --- a/src/sat/smt/euf_internalize.cpp +++ b/src/sat/smt/euf_internalize.cpp @@ -103,8 +103,8 @@ namespace euf { if (lit.sign()) { sat::bool_var v = si.add_bool_var(n->get_owner()); sat::literal lit2 = literal(v, false); - s().mk_clause(~lit, lit2, sat::status::euf_asserted()); - s().mk_clause(lit, ~lit2, sat::status::euf_asserted()); + s().mk_clause(~lit, lit2, sat::status::euf(false)); + s().mk_clause(lit, ~lit2, sat::status::euf(false)); lit = lit2; } sat::bool_var v = lit.var(); @@ -132,7 +132,7 @@ namespace euf { if (sz <= 1) return; - sat::status st = m_is_redundant ? sat::status::euf_learned() : sat::status::euf_asserted(); + sat::status st = sat::status::euf(m_is_redundant); static const unsigned distinct_max_args = 32; if (sz <= distinct_max_args) { sat::literal_vector lits; @@ -175,7 +175,7 @@ namespace euf { SASSERT(m.is_distinct(e)); static const unsigned distinct_max_args = 32; unsigned sz = e->get_num_args(); - sat::status st = m_is_redundant ? sat::status::euf_learned() : sat::status::euf_asserted(); + sat::status st = sat::status::euf(m_is_redundant); if (sz <= 1) { s().mk_clause(0, nullptr, st); return; @@ -209,7 +209,7 @@ namespace euf { void solver::axiomatize_basic(enode* n) { expr* e = n->get_owner(); - sat::status st = m_is_redundant ? sat::status::euf_learned() : sat::status::euf_asserted(); + sat::status st = sat::status::euf(m_is_redundant); if (m.is_ite(e)) { app* a = to_app(e); expr* c = a->get_arg(0); diff --git a/src/sat/smt/euf_proof.cpp b/src/sat/smt/euf_proof.cpp index d50314eba..9e983eb55 100644 --- a/src/sat/smt/euf_proof.cpp +++ b/src/sat/smt/euf_proof.cpp @@ -49,7 +49,7 @@ namespace euf { for (literal lit : r) lits.push_back(~lit); if (l != sat::null_literal) lits.push_back(l); - s().get_drat().add(lits, sat::status::euf_learned()); + s().get_drat().add(lits, sat::status::euf(true)); } }