mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 09:55:19 +00:00
Code Activity

build fix

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-09-02 12:35:12 -07:00
parent daf7e9e3ef
commit 7c2fe46eb7
7 changed files with 46 additions and 49 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

44
src/sat/sat_drat.cpp
View file

@ -76,11 +76,11 @@ namespace sat {
else if (st.is_asserted()) else if (st.is_asserted())
out << "a"; out << "a";
switch (st.orig) { if (st.is_ba())
case status::orig::ba: return out << " ba"; out << " ba";
case status::orig::euf: return out << " euf"; else if (st.is_euf())
default: return out; out << " euf";
} return out;
} }
void drat::dump(unsigned n, literal const* c, status st) { void drat::dump(unsigned n, literal const* c, status st) {
@ -94,32 +94,25 @@ namespace sat {
char* lastd = digits + sizeof(digits); char* lastd = digits + sizeof(digits);
unsigned len = 0; unsigned len = 0;
switch (st.st) { if (st.is_asserted()) {
case status::st::asserted:
buffer[len++] = 'a'; buffer[len++] = 'a';
buffer[len++] = ' '; buffer[len++] = ' ';
break; }
case status::st::deleted: else if (st.is_deleted()) {
buffer[len++] = 'd'; buffer[len++] = 'd';
buffer[len++] = ' '; buffer[len++] = ' ';
break;
default:
break;
} }
switch (st.orig) {
case status::orig::euf: if (st.is_euf()) {
buffer[len++] = 'e'; buffer[len++] = 'e';
buffer[len++] = 'u'; buffer[len++] = 'u';
buffer[len++] = 'f'; buffer[len++] = 'f';
buffer[len++] = ' '; buffer[len++] = ' ';
break; }
case status::orig::ba: else if (st.is_ba()) {
buffer[len++] = 'b'; buffer[len++] = 'b';
buffer[len++] = 'a'; buffer[len++] = 'a';
buffer[len++] = ' '; buffer[len++] = ' ';
break;
default:
break;
} }
for (unsigned i = 0; i < n; ++i) { for (unsigned i = 0; i < n; ++i) {
literal lit = c[i]; literal lit = c[i];
@ -160,12 +153,11 @@ namespace sat {
void drat::bdump(unsigned n, literal const* c, status st) { void drat::bdump(unsigned n, literal const* c, status st) {
unsigned char ch = 0; unsigned char ch = 0;
switch (st.st) { if (st.is_redundant())
case status::st::asserted: return; ch = 'a';
case status::st::redundant: ch = 'a'; break; else if (st.is_deleted())
case status::st::deleted: ch = 'd'; break; ch = 'd';
default: UNREACHABLE(); break; else return;
}
char buffer[10000]; char buffer[10000];
int len = 0; int len = 0;
buffer[len++] = ch; buffer[len++] = ch;
@ -497,7 +489,7 @@ namespace sat {
clause& c = *m_proof[i]; clause& c = *m_proof[i];
unsigned j = 0; unsigned j = 0;
for (; j < c.size() && c[j] != ~l; ++j) {} 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(j, c.begin());
lits.append(c.size() - j - 1, c.begin() + j + 1); lits.append(c.size() - j - 1, c.begin() + j + 1);
if (!is_drup(lits.size(), lits.c_ptr())) if (!is_drup(lits.size(), lits.c_ptr()))

2
src/sat/sat_solver.cpp
View file

@ -501,7 +501,7 @@ namespace sat {
clause * solver::mk_nary_clause(unsigned num_lits, literal * lits, sat::status st) { clause * solver::mk_nary_clause(unsigned num_lits, literal * lits, sat::status st) {
m_stats.m_mk_clause++; m_stats.m_mk_clause++;
clause * r = alloc_clause(num_lits, lits, st.is_redundant()); 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); bool reinit = attach_nary_clause(*r);
if (reinit && !st.is_redundant()) push_reinit_stack(*r); if (reinit && !st.is_redundant()) push_reinit_stack(*r);
if (st.is_redundant()) { if (st.is_redundant()) {

27
src/sat/sat_types.h
View file

@ -254,26 +254,31 @@ namespace sat {
class status { class status {
public: public:
enum class st { asserted, redundant, deleted } st; enum class st { asserted, redundant, deleted };
enum class orig { sat, ba, euf } orig; enum class orig { sat, ba, euf };
status(enum st s, enum orig o) : st(s), orig(o) {}; st m_st;
status(status const& s) : st(s.st), orig(s.orig) {} orig m_orig;
status(status&& s) noexcept { st = st::asserted; orig = orig::sat; std::swap(st, s.st); std::swap(orig, s.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 redundant() { return status(status::st::redundant, status::orig::sat); }
static status asserted() { return status(status::st::asserted, 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 deleted() { return status(status::st::deleted, status::orig::sat); }
static status euf_learned() { return status(status::st::redundant, status::orig::euf); } static status euf(bool redundant) { return status(redundant ? st::redundant : st::asserted, orig::euf); }
static status euf_asserted() { return status(status::st::asserted, status::orig::euf); }
static status ba(bool redundant) { return redundant ? ba_redundant() : ba_asserted(); } 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_redundant() { return status(status::st::redundant, status::orig::ba); }
static status ba_asserted() { return status(status::st::asserted, 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_redundant() const { return st::redundant == m_st; }
bool is_asserted() const { return st::asserted == st; } bool is_asserted() const { return st::asserted == m_st; }
bool is_deleted() const { return st::deleted == st; } bool is_deleted() const { return st::deleted == m_st; }
bool operator==(status const& s) const { return s.orig == orig && s.st == 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; }
}; };

6
src/sat/smt/ba_solver.cpp
View file

@ -1598,7 +1598,7 @@ namespace sat {
TRACE("ba", tout << m_lemma << "\n";); TRACE("ba", tout << m_lemma << "\n";);
if (get_config().m_drat && m_solver) { 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(); s().m_lemma.reset();
@ -2140,7 +2140,7 @@ namespace sat {
for (literal lit : r) for (literal lit : r)
lits.push_back(~lit); lits.push_back(~lit);
lits.push_back(l); 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 (all_units && sz < k) {
if (c.lit() == null_literal) { if (c.lit() == null_literal) {
s().mk_clause(0, nullptr, status::ba_redundant()); s().mk_clause(0, nullptr, status::ba(c.learned()));
} }
else { else {
literal lit = ~c.lit(); literal lit = ~c.lit();

4
src/sat/smt/euf_ackerman.cpp
View file

@ -194,7 +194,7 @@ namespace euf {
} }
expr_ref eq(m.mk_eq(a, b), m); expr_ref eq(m.mk_eq(a, b), m);
lits.push_back(s.internalize(eq, false, false, true)); 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) { 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[0] = s.internalize(eq1, true, false, true);
lits[1] = s.internalize(eq2, true, false, true); lits[1] = s.internalize(eq2, true, false, true);
lits[2] = s.internalize(eq3, false, 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));
} }
} }

10
src/sat/smt/euf_internalize.cpp
View file

@ -103,8 +103,8 @@ namespace euf {
if (lit.sign()) { if (lit.sign()) {
sat::bool_var v = si.add_bool_var(n->get_owner()); sat::bool_var v = si.add_bool_var(n->get_owner());
sat::literal lit2 = literal(v, false); sat::literal lit2 = literal(v, false);
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_asserted()); s().mk_clause(lit, ~lit2, sat::status::euf(false));
lit = lit2; lit = lit2;
} }
sat::bool_var v = lit.var(); sat::bool_var v = lit.var();
@ -132,7 +132,7 @@ namespace euf {
if (sz <= 1) if (sz <= 1)
return; 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; static const unsigned distinct_max_args = 32;
if (sz <= distinct_max_args) { if (sz <= distinct_max_args) {
sat::literal_vector lits; sat::literal_vector lits;
@ -175,7 +175,7 @@ namespace euf {
SASSERT(m.is_distinct(e)); SASSERT(m.is_distinct(e));
static const unsigned distinct_max_args = 32; static const unsigned distinct_max_args = 32;
unsigned sz = e->get_num_args(); 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) { if (sz <= 1) {
s().mk_clause(0, nullptr, st); s().mk_clause(0, nullptr, st);
return; return;
@ -209,7 +209,7 @@ namespace euf {
void solver::axiomatize_basic(enode* n) { void solver::axiomatize_basic(enode* n) {
expr* e = n->get_owner(); 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)) { if (m.is_ite(e)) {
app* a = to_app(e); app* a = to_app(e);
expr* c = a->get_arg(0); expr* c = a->get_arg(0);

2
src/sat/smt/euf_proof.cpp
View file

@ -49,7 +49,7 @@ namespace euf {
for (literal lit : r) lits.push_back(~lit); for (literal lit : r) lits.push_back(~lit);
if (l != sat::null_literal) if (l != sat::null_literal)
lits.push_back(l); lits.push_back(l);
s().get_drat().add(lits, sat::status::euf_learned()); s().get_drat().add(lits, sat::status::euf(true));
} }
} }