diff --git a/src/ast/rewriter/pb2bv_rewriter.cpp b/src/ast/rewriter/pb2bv_rewriter.cpp index 6ba55d12a..4c8f5d665 100644 --- a/src/ast/rewriter/pb2bv_rewriter.cpp +++ b/src/ast/rewriter/pb2bv_rewriter.cpp @@ -355,6 +355,7 @@ struct pb2bv_rewriter::imp { SASSERT(f->get_family_id() == pb.get_family_id()); std::cout << "card: " << m_enable_card << "\n"; if (is_or(f)) { + if (m_enable_card) return false; result = m.mk_or(sz, args); } else if (pb.is_at_most_k(f) && pb.get_k(f).is_unsigned()) { diff --git a/src/sat/card_extension.cpp b/src/sat/card_extension.cpp index ac11e2f71..1950a8d84 100644 --- a/src/sat/card_extension.cpp +++ b/src/sat/card_extension.cpp @@ -159,23 +159,19 @@ namespace sat { } void card_extension::set_conflict(card& c, literal lit) { - std::cout << "conflict\n"; SASSERT(validate_conflict(c)); - m_stats.m_num_conflicts++; if (!resolve_conflict(c, lit)) { - - literal_vector& lits = get_literals(); - SASSERT(value(lit) == l_false); - SASSERT(value(c.lit()) == l_true); - lits.push_back(~c.lit()); - lits.push_back(lit); + + m_conflict.reset(); + m_conflict.push_back(~c.lit()); unsigned sz = c.size(); for (unsigned i = c.k(); i < sz; ++i) { - SASSERT(value(c[i]) == l_false); - lits.push_back(c[i]); + m_conflict.push_back(c[i]); } - s().mk_clause_core(lits.size(), lits.c_ptr(), true); + m_conflict.push_back(lit); + SASSERT(validate_conflict(m_conflict)); + s().assign(lit, justification::mk_ext_justification(0)); } SASSERT(s().inconsistent()); } @@ -242,7 +238,7 @@ namespace sat { bool_var v; m_conflict_lvl = 0; - for (unsigned i = 0; i < c.size(); ++i) { + for (unsigned i = c.k(); i < c.size(); ++i) { literal lit = c[i]; SASSERT(value(lit) == l_false); m_conflict_lvl = std::max(m_conflict_lvl, lvl(lit)); @@ -276,6 +272,7 @@ namespace sat { } SASSERT(validate_lemma()); + SASSERT(offset > 0); js = s().m_justification[v]; @@ -284,17 +281,22 @@ namespace sat { int bound = 1; switch(js.get_kind()) { case justification::NONE: + //std::cout << "NONE\n"; + inc_coeff(consequent, offset); break; case justification::BINARY: + //std::cout << "BINARY\n"; inc_coeff(consequent, offset); - process_antecedent(~(js.get_literal()), offset); + process_antecedent((js.get_literal()), offset); break; case justification::TERNARY: + //std::cout << "TERNARY\n"; inc_coeff(consequent, offset); - process_antecedent(~(js.get_literal1()), offset); - process_antecedent(~(js.get_literal2()), offset); + process_antecedent((js.get_literal1()), offset); + process_antecedent((js.get_literal2()), offset); break; case justification::CLAUSE: { + //std::cout << "CLAUSE\n"; inc_coeff(consequent, offset); clause & c = *(s().m_cls_allocator.get_clause(js.get_clause_offset())); unsigned i = 0; @@ -303,15 +305,16 @@ namespace sat { i = 1; } else { - process_antecedent(~c[0], offset); + process_antecedent(c[0], offset); i = 2; } - unsigned sz = c.size(); + unsigned sz = c.size(); for (; i < sz; i++) - process_antecedent(~c[i], offset); + process_antecedent(c[i], offset); break; } case justification::EXT_JUSTIFICATION: { + //std::cout << "CARDINALITY\n"; unsigned index = js.get_ext_justification_idx(); card& c2 = *m_constraints[index]; process_card(c2, offset); @@ -365,7 +368,6 @@ namespace sat { alit = get_asserting_literal(~consequent); slack -= get_abs_coeff(alit.var()); - m_conflict.push_back(alit); for (unsigned i = lits.size(); 0 <= slack && i > 0; ) { --i; @@ -383,10 +385,13 @@ namespace sat { } } } + m_conflict.push_back(alit); SASSERT(slack < 0); SASSERT(validate_conflict(m_conflict)); - s().mk_clause_core(m_conflict.size(), m_conflict.c_ptr(), true); + // std::cout << alit << ": " << m_conflict << "\n"; + s().assign(alit, justification::mk_ext_justification(0)); + // s().mk_clause_core(m_conflict.size(), m_conflict.c_ptr(), true); return true; bail_out: @@ -444,6 +449,7 @@ namespace sat { card_extension::card_extension(): m_solver(0) { TRACE("sat", tout << this << "\n";); + m_constraints.push_back(0); // dummy constraint for conflicts } card_extension::~card_extension() { @@ -469,20 +475,29 @@ namespace sat { } void card_extension::get_antecedents(literal l, ext_justification_idx idx, literal_vector & r) { - card& c = *m_constraints[idx]; - - DEBUG_CODE( - bool found = false; - for (unsigned i = 0; !found && i < c.k(); ++i) { - found = c[i] == l; + if (idx == 0) { + SASSERT(m_conflict.back() == l); + for (unsigned i = 0; i + 1 < m_conflict.size(); ++i) { + SASSERT(value(m_conflict[i]) == l_false); + r.push_back(~m_conflict[i]); + } + } + else { + card& c = *m_constraints[idx]; + + DEBUG_CODE( + bool found = false; + for (unsigned i = 0; !found && i < c.k(); ++i) { + found = c[i] == l; + } + SASSERT(found);); + + r.push_back(c.lit()); + SASSERT(value(c.lit()) == l_true); + for (unsigned i = c.k(); i < c.size(); ++i) { + SASSERT(value(c[i]) == l_false); + r.push_back(~c[i]); } - SASSERT(found);); - - r.push_back(c.lit()); - SASSERT(value(c.lit()) == l_true); - for (unsigned i = c.k(); i < c.size(); ++i) { - SASSERT(value(c[i]) == l_false); - r.push_back(~c[i]); } } @@ -613,7 +628,8 @@ namespace sat { extension* card_extension::copy(solver* s) { card_extension* result = alloc(card_extension); result->set_solver(s); - for (unsigned i = 0; i < m_constraints.size(); ++i) { + result->m_constraints.push_back(0); + for (unsigned i = 1; i < m_constraints.size(); ++i) { literal_vector lits; card& c = *m_constraints[i]; for (unsigned i = 0; i < c.size(); ++i) { @@ -626,7 +642,6 @@ namespace sat { if (v != null_bool_var) { card* c = m_var_infos[v].m_card; card* c2 = m_constraints[c->index()]; - result->m_var_trail.reserve(v + 10); NOT_IMPLEMENTED_YET(); } } @@ -646,6 +661,13 @@ namespace sat { } } + void card_extension::display(std::ostream& out, ineq& ineq) const { + for (unsigned i = 0; i < ineq.m_lits.size(); ++i) { + out << ineq.m_coeffs[i] << "*" << ineq.m_lits[i] << " "; + } + out << ">= " << ineq.m_k << "\n"; + } + void card_extension::display(std::ostream& out, card& c, bool values) const { out << c.lit(); if (c.lit() != null_literal && values) { @@ -740,25 +762,26 @@ namespace sat { void card_extension::justification2pb(justification const& js, literal lit, unsigned offset, ineq& p) { switch (js.get_kind()) { case justification::NONE: - p.reset(0); + p.reset(offset); + p.push(lit, offset); break; case justification::BINARY: p.reset(offset); p.push(lit, offset); - p.push(~js.get_literal(), offset); + p.push(js.get_literal(), offset); break; case justification::TERNARY: p.reset(offset); p.push(lit, offset); - p.push(~(js.get_literal1()), offset); - p.push(~(js.get_literal2()), offset); + p.push(js.get_literal1(), offset); + p.push(js.get_literal2(), offset); break; case justification::CLAUSE: { p.reset(offset); clause & c = *(s().m_cls_allocator.get_clause(js.get_clause_offset())); unsigned sz = c.size(); for (unsigned i = 0; i < sz; i++) - p.push(~c[i], offset); + p.push(c[i], offset); break; } case justification::EXT_JUSTIFICATION: { @@ -822,6 +845,15 @@ namespace sat { coeffs.remove(lit.index()); } } + if (!coeffs.empty() || m_C.m_k > k) { + display(std::cout, m_A); + display(std::cout, m_B); + display(std::cout, m_C); + u_map::iterator it = coeffs.begin(), end = coeffs.end(); + for (; it != end; ++it) { + std::cout << to_literal(it->m_key) << ": " << it->m_value << "\n"; + } + } SASSERT(coeffs.empty()); SASSERT(m_C.m_k <= k); return true; diff --git a/src/sat/card_extension.h b/src/sat/card_extension.h index e1ed197d1..947f6e5d3 100644 --- a/src/sat/card_extension.h +++ b/src/sat/card_extension.h @@ -138,6 +138,7 @@ namespace sat { void justification2pb(justification const& j, literal lit, unsigned offset, ineq& p); bool validate_resolvent(); + void display(std::ostream& out, ineq& p) const; void display(std::ostream& out, card& c, bool values) const; void display_watch(std::ostream& out, bool_var v, bool sign) const; public: diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index ec224e6b8..3d36e0b53 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -565,7 +565,7 @@ namespace sat { while (m_qhead < m_trail.size()) { checkpoint(); m_cleaner.dec(); - SASSERT(!m_inconsistent); + if (m_inconsistent) return false; l = m_trail[m_qhead]; TRACE("sat_propagate", tout << "propagating: " << l << " " << m_justification[l.var()] << "\n";); m_qhead++; @@ -1682,7 +1682,7 @@ namespace sat { m_conflicts_since_restart++; m_conflicts_since_gc++; - m_conflict_lvl = get_max_lvl(m_not_l, m_conflict); + m_conflict_lvl = get_max_lvl(m_not_l == literal() ? m_not_l : ~m_not_l, m_conflict); TRACE("sat", tout << "conflict detected at level " << m_conflict_lvl << " for "; if (m_not_l == literal()) tout << "null literal\n"; else tout << m_not_l << "\n";); @@ -1710,7 +1710,7 @@ namespace sat { process_antecedent(m_not_l, num_marks); } - literal consequent = m_not_l; + literal consequent = m_not_l == null_literal ? m_not_l : ~m_not_l; justification js = m_conflict; do { @@ -2033,7 +2033,7 @@ namespace sat { } } - literal consequent = m_not_l; + literal consequent = m_not_l == null_literal ? m_not_l : ~m_not_l; justification js = m_conflict;