mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-05 21:53:23 +00:00
Code Activity

fixing bugs in dealing with non-0 based cardinality constraints

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-02-07 20:59:28 -08:00
parent eaf845c2f4
commit 6b4aec9b74
2 changed files with 39 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

53
src/sat/card_extension.cpp
View file

@ -53,6 +53,7 @@ namespace sat {
if (c.lit().sign() == is_true) { if (c.lit().sign() == is_true) {
c.negate(); c.negate();
} }
TRACE("sat", display(tout << "init watch: ", c, true););
SASSERT(value(c.lit()) == l_true); SASSERT(value(c.lit()) == l_true);
unsigned j = 0, sz = c.size(), bound = c.k(); unsigned j = 0, sz = c.size(), bound = c.k();
if (bound == sz) { if (bound == sz) {
@ -131,7 +132,7 @@ namespace sat {
return TAG(ptr_vector<card>*, c, 1); return TAG(ptr_vector<card>*, c, 1);
} }
bool card_extension::is_tag_empty(ptr_vector<card>* c) { bool card_extension::is_tag_empty(ptr_vector<card> const* c) {
return !c || GET_TAG(c) == 1; return !c || GET_TAG(c) == 1;
} }
@ -255,9 +256,7 @@ namespace sat {
} }
int card_extension::get_abs_coeff(bool_var v) const { int card_extension::get_abs_coeff(bool_var v) const {
int coeff = get_coeff(v); return abs(get_coeff(v));
if (coeff < 0) coeff = -coeff;
return coeff;
} }
void card_extension::reset_coeffs() { void card_extension::reset_coeffs() {
@ -267,6 +266,13 @@ namespace sat {
m_active_vars.reset(); m_active_vars.reset();
} }
void card_extension::reset_marked_literals() {
for (unsigned i = 0; i < m_marked_literals.size(); ++i) {
s().unmark_lit(m_marked_literals[i]);
}
m_marked_literals.reset();
}
bool card_extension::resolve_conflict() { bool card_extension::resolve_conflict() {
if (0 == m_num_propagations_since_pop) if (0 == m_num_propagations_since_pop)
return false; return false;
@ -290,7 +296,8 @@ namespace sat {
unsigned num_steps = 0; unsigned num_steps = 0;
DEBUG_CODE(active2pb(m_A);); DEBUG_CODE(active2pb(m_A););
std::cout << m_num_marks << "\n"; unsigned init_marks = m_num_marks;
do { do {
if (offset == 0) { if (offset == 0) {
@ -298,7 +305,6 @@ namespace sat {
} }
// TBD: need proper check for overflow. // TBD: need proper check for overflow.
if (offset > (1 << 12)) { if (offset > (1 << 12)) {
std::cout << "Offset: " << offset << "\n";
goto bail_out; goto bail_out;
} }
@ -388,6 +394,7 @@ namespace sat {
v = consequent.var(); v = consequent.var();
if (s().is_marked(v)) break; if (s().is_marked(v)) break;
if (idx == 0) { if (idx == 0) {
std::cout << num_steps << " " << init_marks << "\n";
goto bail_out; goto bail_out;
} }
SASSERT(idx > 0); SASSERT(idx > 0);
@ -414,6 +421,7 @@ namespace sat {
SASSERT(validate_lemma()); SASSERT(validate_lemma());
normalize_active_coeffs(); normalize_active_coeffs();
reset_marked_literals();
if (consequent == null_literal) { if (consequent == null_literal) {
return false; return false;
@ -427,6 +435,7 @@ namespace sat {
consequent = null_literal; consequent = null_literal;
++idx; ++idx;
unsigned num_atoms = m_lemma.size();
while (0 <= slack) { while (0 <= slack) {
literal lit = lits[idx]; literal lit = lits[idx];
bool_var v = lit.var(); bool_var v = lit.var();
@ -447,11 +456,6 @@ namespace sat {
} }
else { else {
m_lemma.push_back(~lit); m_lemma.push_back(~lit);
if (lvl(lit) == m_conflict_lvl) {
TRACE("sat", tout << "Bail out on no progress " << lit << "\n";);
IF_VERBOSE(3, verbose_stream() << "(sat.card bail resolve)\n";);
return false;
}
} }
} }
} }
@ -459,10 +463,18 @@ namespace sat {
--idx; --idx;
} }
for (unsigned i = 1; i < std::min(m_lemma.size(), num_atoms + 1); ++i) {
if (lvl(m_lemma[i]) == m_conflict_lvl) {
TRACE("sat", tout << "Bail out on no progress " << lit << "\n";);
IF_VERBOSE(3, verbose_stream() << "(sat.card bail resolve)\n";);
return false;
}
}
SASSERT(slack < 0); SASSERT(slack < 0);
if (consequent == null_literal) { if (consequent == null_literal) {
if (!m_lemma.empty()) return false; if (!m_lemma.empty()) return false;
} }
else { else {
m_lemma[0] = consequent; m_lemma[0] = consequent;
@ -478,6 +490,7 @@ namespace sat {
s().m_lemma.reset(); s().m_lemma.reset();
s().m_lemma.append(m_lemma); s().m_lemma.append(m_lemma);
for (unsigned i = 1; i < m_lemma.size(); ++i) { for (unsigned i = 1; i < m_lemma.size(); ++i) {
CTRACE("sat", s().is_marked(m_lemma[i].var()), tout << "marked: " << m_lemma[i] << "\n";);
s().mark(m_lemma[i].var()); s().mark(m_lemma[i].var());
} }
m_stats.m_num_conflicts++; m_stats.m_num_conflicts++;
@ -485,6 +498,7 @@ namespace sat {
return true; return true;
bail_out: bail_out:
reset_marked_literals();
std::cout << "bail num marks: " << m_num_marks << " idx: " << idx << "\n"; std::cout << "bail num marks: " << m_num_marks << " idx: " << idx << "\n";
while (m_num_marks > 0 && idx >= 0) { while (m_num_marks > 0 && idx >= 0) {
bool_var v = lits[idx].var(); bool_var v = lits[idx].var();
@ -498,18 +512,21 @@ namespace sat {
} }
bool card_extension::process_card(card& c, int offset) { bool card_extension::process_card(card& c, int offset) {
SASSERT(c.k() <= c.size()); literal lit = c.lit();
SASSERT(value(c.lit()) == l_true); SASSERT(c.k() <= c.size());
SASSERT(value(lit) == l_true);
for (unsigned i = c.k(); i < c.size(); ++i) { for (unsigned i = c.k(); i < c.size(); ++i) {
process_antecedent(c[i], offset); process_antecedent(c[i], offset);
} }
for (unsigned i = 0; i < c.k(); ++i) { for (unsigned i = 0; i < c.k(); ++i) {
inc_coeff(c[i], offset); inc_coeff(c[i], offset);
} }
if (lvl(c.lit()) > 0) { if (lvl(lit) > 0 && !s().is_marked_lit(lit)) {
m_lemma.push_back(~c.lit()); m_lemma.push_back(~lit);
s().mark_lit(lit);
m_marked_literals.push_back(lit);
} }
return (lvl(c.lit()) <= m_conflict_lvl); return (lvl(lit) <= m_conflict_lvl);
} }
void card_extension::process_antecedent(literal l, int offset) { void card_extension::process_antecedent(literal l, int offset) {
@ -733,7 +750,7 @@ namespace sat {
void card_extension::display_watch(std::ostream& out, bool_var v, bool sign) const { void card_extension::display_watch(std::ostream& out, bool_var v, bool sign) const {
watch const* w = m_var_infos[v].m_lit_watch[sign]; watch const* w = m_var_infos[v].m_lit_watch[sign];
if (w && !w->empty()) { if (!is_tag_empty(w)) {
watch const& wl = *w; watch const& wl = *w;
out << literal(v, sign) << " |-> "; out << literal(v, sign) << " |-> ";
for (unsigned i = 0; i < wl.size(); ++i) { for (unsigned i = 0; i < wl.size(); ++i) {

6
src/sat/card_extension.h
View file

@ -76,8 +76,8 @@ namespace sat {
} }
}; };
ptr_vector<card>* set_tag_empty(ptr_vector<card>* c); static ptr_vector<card>* set_tag_empty(ptr_vector<card>* c);
bool is_tag_empty(ptr_vector<card>* c); static bool is_tag_empty(ptr_vector<card> const* c);
static ptr_vector<card>* set_tag_non_empty(ptr_vector<card>* c); static ptr_vector<card>* set_tag_non_empty(ptr_vector<card>* c);
solver* m_solver; solver* m_solver;
@ -99,6 +99,7 @@ namespace sat {
tracked_uint_set m_active_var_set; tracked_uint_set m_active_var_set;
literal_vector m_lemma; literal_vector m_lemma;
literal_vector m_literals; literal_vector m_literals;
literal_vector m_marked_literals;
unsigned m_num_propagations_since_pop; unsigned m_num_propagations_since_pop;
solver& s() const { return *m_solver; } solver& s() const { return *m_solver; }
@ -110,6 +111,7 @@ namespace sat {
void set_conflict(card& c, literal lit); void set_conflict(card& c, literal lit);
void clear_watch(card& c); void clear_watch(card& c);
void reset_coeffs(); void reset_coeffs();
void reset_marked_literals();
inline lbool value(literal lit) const { return m_solver->value(lit); } inline lbool value(literal lit) const { return m_solver->value(lit); }
inline unsigned lvl(literal lit) const { return m_solver->lvl(lit); } inline unsigned lvl(literal lit) const { return m_solver->lvl(lit); }