mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
working on card for sat
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
a412a554eb
commit
92e2d920fd
|
|
@ -1,5 +1,6 @@
|
|||
z3_add_component(sat
|
||||
SOURCES
|
||||
card_extension.cpp
|
||||
dimacs.cpp
|
||||
sat_asymm_branch.cpp
|
||||
sat_clause.cpp
|
||||
|
|
|
|||
686
src/sat/card_extension.cpp
Normal file
686
src/sat/card_extension.cpp
Normal file
|
|
@ -0,0 +1,686 @@
|
|||
/*++
|
||||
Copyright (c) 2017 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
card_extension.cpp
|
||||
|
||||
Abstract:
|
||||
|
||||
Extension for cardinality reasoning.
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2017-01-30
|
||||
|
||||
Revision History:
|
||||
|
||||
--*/
|
||||
|
||||
#include"card_extension.h"
|
||||
#include"sat_types.h"
|
||||
|
||||
namespace sat {
|
||||
|
||||
card_extension::card::card(unsigned index, literal lit, literal_vector const& lits, unsigned k):
|
||||
m_index(index),
|
||||
m_lit(lit),
|
||||
m_k(k),
|
||||
m_size(lits.size()),
|
||||
m_lits(lits) {
|
||||
}
|
||||
|
||||
void card_extension::card::negate() {
|
||||
m_lit.neg();
|
||||
for (unsigned i = 0; i < m_size; ++i) {
|
||||
m_lits[i].neg();
|
||||
}
|
||||
m_k = m_size - m_k + 1;
|
||||
SASSERT(m_size >= m_k && m_k > 0);
|
||||
}
|
||||
|
||||
void card_extension::init_watch(bool_var v) {
|
||||
if (m_var_infos.size() <= static_cast<unsigned>(v)) {
|
||||
m_var_infos.resize(static_cast<unsigned>(v)+100);
|
||||
}
|
||||
}
|
||||
|
||||
void card_extension::init_watch(card& c, bool is_true) {
|
||||
clear_watch(c);
|
||||
if (c.lit().sign() == is_true) {
|
||||
c.negate();
|
||||
}
|
||||
SASSERT(s().value(c.lit()) == l_true);
|
||||
unsigned j = 0, sz = c.size(), bound = c.k();
|
||||
if (bound == sz) {
|
||||
for (unsigned i = 0; i < sz && !s().inconsistent(); ++i) {
|
||||
assign(c, c[i]);
|
||||
}
|
||||
return;
|
||||
}
|
||||
// put the non-false literals into the head.
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
if (s().value(c[i]) != l_false) {
|
||||
if (j != i) {
|
||||
c.swap(i, j);
|
||||
}
|
||||
++j;
|
||||
}
|
||||
}
|
||||
DEBUG_CODE(
|
||||
bool is_false = false;
|
||||
for (unsigned k = 0; k < sz; ++k) {
|
||||
SASSERT(!is_false || s().value(c[k]) == l_false);
|
||||
is_false = s().value(c[k]) == l_false;
|
||||
});
|
||||
|
||||
// j is the number of non-false, sz - j the number of false.
|
||||
if (j < bound) {
|
||||
SASSERT(0 < bound && bound < sz);
|
||||
literal alit = c[j];
|
||||
|
||||
//
|
||||
// we need the assignment level of the asserting literal to be maximal.
|
||||
// such that conflict resolution can use the asserting literal as a starting
|
||||
// point.
|
||||
//
|
||||
|
||||
for (unsigned i = bound; i < sz; ++i) {
|
||||
if (s().lvl(alit) < s().lvl(c[i])) {
|
||||
c.swap(i, j);
|
||||
alit = c[j];
|
||||
}
|
||||
}
|
||||
set_conflict(c, alit);
|
||||
}
|
||||
else if (j == bound) {
|
||||
for (unsigned i = 0; i < bound && !s().inconsistent(); ++i) {
|
||||
assign(c, c[i]);
|
||||
}
|
||||
}
|
||||
else {
|
||||
for (unsigned i = 0; i <= bound; ++i) {
|
||||
watch_literal(c, c[i]);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void card_extension::clear_watch(card& c) {
|
||||
unsigned sz = std::min(c.k() + 1, c.size());
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
unwatch_literal(c[i], &c);
|
||||
}
|
||||
}
|
||||
|
||||
void card_extension::unwatch_literal(literal lit, card* c) {
|
||||
if (m_var_infos.size() <= static_cast<unsigned>(lit.var())) {
|
||||
return;
|
||||
}
|
||||
ptr_vector<card>* cards = m_var_infos[lit.var()].m_lit_watch[lit.sign()];
|
||||
if (cards) {
|
||||
remove(*cards, c);
|
||||
}
|
||||
}
|
||||
|
||||
void card_extension::remove(ptr_vector<card>& cards, card* c) {
|
||||
for (unsigned j = 0; j < cards.size(); ++j) {
|
||||
if (cards[j] == c) {
|
||||
std::swap(cards[j], cards[cards.size()-1]);
|
||||
cards.pop_back();
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void card_extension::assign(card& c, literal lit) {
|
||||
if (s().value(lit) == l_true) {
|
||||
return;
|
||||
}
|
||||
m_stats.m_num_propagations++;
|
||||
//TRACE("sat", tout << "#prop: " << m_stats.m_num_propagations << " - " << c.lit() << " => " << lit << "\n";);
|
||||
SASSERT(validate_unit_propagation(c));
|
||||
s().assign(lit, justification::mk_ext_justification(c.index()));
|
||||
|
||||
}
|
||||
|
||||
void card_extension::watch_literal(card& c, literal lit) {
|
||||
init_watch(lit.var());
|
||||
ptr_vector<card>* cards = m_var_infos[lit.var()].m_lit_watch[lit.sign()];
|
||||
if (cards == 0) {
|
||||
cards = alloc(ptr_vector<card>);
|
||||
m_var_infos[lit.var()].m_lit_watch[lit.sign()] = cards;
|
||||
}
|
||||
cards->push_back(&c);
|
||||
}
|
||||
|
||||
void card_extension::set_conflict(card& c, literal lit) {
|
||||
SASSERT(validate_conflict(c));
|
||||
literal_vector& lits = get_literals();
|
||||
SASSERT(s().value(lit) == l_false);
|
||||
SASSERT(s().value(c.lit()) == l_true);
|
||||
lits.push_back(~c.lit());
|
||||
lits.push_back(lit);
|
||||
unsigned sz = c.size();
|
||||
for (unsigned i = c.k(); i < sz; ++i) {
|
||||
SASSERT(s().value(c[i]) == l_false);
|
||||
lits.push_back(c[i]);
|
||||
}
|
||||
|
||||
m_stats.m_num_conflicts++;
|
||||
if (!resolve_conflict(c, lits)) {
|
||||
s().mk_clause_core(lits.size(), lits.c_ptr(), true);
|
||||
}
|
||||
SASSERT(s().inconsistent());
|
||||
}
|
||||
|
||||
void card_extension::normalize_active_coeffs() {
|
||||
while (!m_active_var_set.empty()) m_active_var_set.erase();
|
||||
unsigned i = 0, j = 0, sz = m_active_vars.size();
|
||||
for (; i < sz; ++i) {
|
||||
bool_var v = m_active_vars[i];
|
||||
if (!m_active_var_set.contains(v) && get_coeff(v) != 0) {
|
||||
m_active_var_set.insert(v);
|
||||
if (j != i) {
|
||||
m_active_vars[j] = m_active_vars[i];
|
||||
}
|
||||
++j;
|
||||
}
|
||||
}
|
||||
sz = j;
|
||||
m_active_vars.shrink(sz);
|
||||
}
|
||||
|
||||
void card_extension::inc_coeff(literal l, int offset) {
|
||||
SASSERT(offset > 0);
|
||||
bool_var v = l.var();
|
||||
SASSERT(v != null_bool_var);
|
||||
if (static_cast<bool_var>(m_coeffs.size()) <= v) {
|
||||
m_coeffs.resize(v + 1, 0);
|
||||
}
|
||||
int coeff0 = m_coeffs[v];
|
||||
if (coeff0 == 0) {
|
||||
m_active_vars.push_back(v);
|
||||
}
|
||||
|
||||
int inc = l.sign() ? -offset : offset;
|
||||
int coeff1 = inc + coeff0;
|
||||
m_coeffs[v] = coeff1;
|
||||
|
||||
if (coeff0 > 0 && inc < 0) {
|
||||
m_bound -= coeff0 - std::max(0, coeff1);
|
||||
}
|
||||
else if (coeff0 < 0 && inc > 0) {
|
||||
m_bound -= std::min(0, coeff1) - coeff0;
|
||||
}
|
||||
}
|
||||
|
||||
int card_extension::get_coeff(bool_var v) const {
|
||||
return m_coeffs.get(v, 0);
|
||||
}
|
||||
|
||||
int card_extension::get_abs_coeff(bool_var v) const {
|
||||
int coeff = get_coeff(v);
|
||||
if (coeff < 0) coeff = -coeff;
|
||||
return coeff;
|
||||
}
|
||||
|
||||
void card_extension::reset_coeffs() {
|
||||
for (unsigned i = 0; i < m_active_vars.size(); ++i) {
|
||||
m_coeffs[m_active_vars[i]] = 0;
|
||||
}
|
||||
m_active_vars.reset();
|
||||
}
|
||||
|
||||
bool card_extension::resolve_conflict(card& c, literal_vector const& conflict_clause) {
|
||||
|
||||
bool_var v;
|
||||
m_conflict_lvl = 0;
|
||||
for (unsigned i = 0; i < c.size(); ++i) {
|
||||
literal lit = c[i];
|
||||
SASSERT(s().value(lit) == l_false);
|
||||
m_conflict_lvl = std::max(m_conflict_lvl, s().lvl(lit));
|
||||
}
|
||||
if (m_conflict_lvl < s().lvl(c.lit()) || m_conflict_lvl == 0) {
|
||||
return false;
|
||||
}
|
||||
|
||||
reset_coeffs();
|
||||
m_num_marks = 0;
|
||||
m_bound = c.k();
|
||||
m_conflict.reset();
|
||||
literal_vector const& lits = s().m_trail;
|
||||
unsigned idx = lits.size()-1;
|
||||
justification js;
|
||||
literal consequent = ~conflict_clause[1];
|
||||
process_card(c, 1);
|
||||
literal alit;
|
||||
|
||||
while (m_num_marks > 0) {
|
||||
|
||||
v = consequent.var();
|
||||
|
||||
int offset = get_abs_coeff(v);
|
||||
|
||||
if (offset == 0) {
|
||||
goto process_next_resolvent;
|
||||
}
|
||||
if (offset > 1000) {
|
||||
goto bail_out;
|
||||
}
|
||||
|
||||
SASSERT(offset > 0);
|
||||
|
||||
js = s().m_justification[v];
|
||||
|
||||
int bound = 1;
|
||||
switch(js.get_kind()) {
|
||||
case justification::NONE:
|
||||
break;
|
||||
case justification::BINARY:
|
||||
inc_coeff(consequent, offset);
|
||||
process_antecedent(~(js.get_literal()), offset);
|
||||
break;
|
||||
case justification::TERNARY:
|
||||
inc_coeff(consequent, offset);
|
||||
process_antecedent(~(js.get_literal1()), offset);
|
||||
process_antecedent(~(js.get_literal2()), offset);
|
||||
break;
|
||||
case justification::CLAUSE: {
|
||||
inc_coeff(consequent, offset);
|
||||
clause & c = *(s().m_cls_allocator.get_clause(js.get_clause_offset()));
|
||||
unsigned i = 0;
|
||||
if (consequent != null_literal) {
|
||||
SASSERT(c[0] == consequent || c[1] == consequent);
|
||||
if (c[0] == consequent) {
|
||||
i = 1;
|
||||
}
|
||||
else {
|
||||
process_antecedent(~c[0], offset);
|
||||
i = 2;
|
||||
}
|
||||
}
|
||||
unsigned sz = c.size();
|
||||
for (; i < sz; i++)
|
||||
process_antecedent(~c[i], offset);
|
||||
break;
|
||||
}
|
||||
case justification::EXT_JUSTIFICATION: {
|
||||
unsigned index = js.get_ext_justification_idx();
|
||||
card& c2 = *m_constraints[index];
|
||||
process_card(c2, offset);
|
||||
bound = c2.k();
|
||||
break;
|
||||
}
|
||||
default:
|
||||
UNREACHABLE();
|
||||
break;
|
||||
}
|
||||
m_bound += offset * bound;
|
||||
|
||||
// cut();
|
||||
|
||||
process_next_resolvent:
|
||||
|
||||
// find the next marked variable in the assignment stack
|
||||
//
|
||||
while (true) {
|
||||
consequent = lits[idx];
|
||||
v = consequent.var();
|
||||
if (s().is_marked(v)) break;
|
||||
SASSERT(idx > 0);
|
||||
--idx;
|
||||
}
|
||||
|
||||
SASSERT(s().lvl(v) == m_conflict_lvl);
|
||||
s().reset_mark(v);
|
||||
--idx;
|
||||
--m_num_marks;
|
||||
}
|
||||
|
||||
SASSERT(validate_lemma());
|
||||
|
||||
normalize_active_coeffs();
|
||||
|
||||
if (m_bound > 0 && m_active_vars.empty()) {
|
||||
return false;
|
||||
}
|
||||
|
||||
int slack = -m_bound;
|
||||
for (unsigned i = 0; i < m_active_vars.size(); ++i) {
|
||||
bool_var v = m_active_vars[i];
|
||||
slack += get_abs_coeff(v);
|
||||
}
|
||||
|
||||
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;
|
||||
literal lit = lits[i];
|
||||
bool_var v = lit.var();
|
||||
if (m_active_var_set.contains(v) && v != alit.var()) {
|
||||
int coeff = get_coeff(v);
|
||||
if (coeff < 0 && !lit.sign()) {
|
||||
slack += coeff;
|
||||
m_conflict.push_back(~lit);
|
||||
}
|
||||
else if (coeff > 0 && lit.sign()) {
|
||||
slack -= coeff;
|
||||
m_conflict.push_back(~lit);
|
||||
}
|
||||
}
|
||||
}
|
||||
SASSERT(slack < 0);
|
||||
SASSERT(validate_conflict(m_conflict));
|
||||
|
||||
s().mk_clause_core(m_conflict.size(), m_conflict.c_ptr(), true);
|
||||
return true;
|
||||
|
||||
bail_out:
|
||||
while (m_num_marks > 0 && idx > 0) {
|
||||
v = lits[idx].var();
|
||||
if (s().is_marked(v)) {
|
||||
s().reset_mark(v);
|
||||
}
|
||||
--idx;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
void card_extension::process_card(card& c, int offset) {
|
||||
SASSERT(c.k() <= c.size());
|
||||
SASSERT(s().value(c.lit()) == l_true);
|
||||
for (unsigned i = c.k(); i < c.size(); ++i) {
|
||||
process_antecedent(c[i], offset);
|
||||
}
|
||||
for (unsigned i = 0; i < c.k(); ++i) {
|
||||
inc_coeff(c[i], offset);
|
||||
}
|
||||
if (s().lvl(c.lit()) > 0) {
|
||||
m_conflict.push_back(~c.lit());
|
||||
}
|
||||
}
|
||||
|
||||
void card_extension::process_antecedent(literal l, int offset) {
|
||||
SASSERT(s().value(l) == l_false);
|
||||
bool_var v = l.var();
|
||||
unsigned lvl = s().lvl(v);
|
||||
|
||||
if (lvl > 0 && !s().is_marked(v) && lvl == m_conflict_lvl) {
|
||||
s().mark(v);
|
||||
++m_num_marks;
|
||||
}
|
||||
inc_coeff(l, offset);
|
||||
}
|
||||
|
||||
literal card_extension::get_asserting_literal(literal p) {
|
||||
if (get_abs_coeff(p.var()) != 0) {
|
||||
return p;
|
||||
}
|
||||
unsigned lvl = 0;
|
||||
for (unsigned i = 0; i < m_active_vars.size(); ++i) {
|
||||
bool_var v = m_active_vars[i];
|
||||
literal lit(v, get_coeff(v) < 0);
|
||||
if (s().value(lit) == l_false && s().lvl(lit) > lvl) {
|
||||
p = lit;
|
||||
}
|
||||
}
|
||||
return p;
|
||||
}
|
||||
|
||||
card_extension::card_extension(): m_solver(0) {}
|
||||
|
||||
card_extension::~card_extension() {
|
||||
for (unsigned i = 0; i < m_var_infos.size(); ++i) {
|
||||
m_var_infos[i].reset();
|
||||
}
|
||||
m_var_trail.reset();
|
||||
m_var_lim.reset();
|
||||
m_stats.reset();
|
||||
}
|
||||
|
||||
void card_extension::add_at_least(bool_var v, literal_vector const& lits, unsigned k) {
|
||||
unsigned index = m_constraints.size();
|
||||
card* c = alloc(card, index, literal(v, false), lits, k);
|
||||
m_constraints.push_back(c);
|
||||
init_watch(v);
|
||||
m_var_infos[v].m_card = c;
|
||||
m_var_trail.push_back(v);
|
||||
}
|
||||
|
||||
void card_extension::propagate(literal l, ext_constraint_idx idx, bool & keep) {
|
||||
UNREACHABLE();
|
||||
}
|
||||
|
||||
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;
|
||||
}
|
||||
SASSERT(found););
|
||||
|
||||
for (unsigned i = c.k(); i < c.size(); ++i) {
|
||||
SASSERT(s().value(c[i]) == l_false);
|
||||
r.push_back(c[i]);
|
||||
}
|
||||
}
|
||||
|
||||
lbool card_extension::add_assign(card& c, literal alit) {
|
||||
// literal is assigned to false.
|
||||
unsigned sz = c.size();
|
||||
unsigned bound = c.k();
|
||||
TRACE("pb", tout << "assign: " << c.lit() << " " << ~alit << " " << bound << "\n";);
|
||||
|
||||
SASSERT(0 < bound && bound < sz);
|
||||
SASSERT(s().value(alit) == l_false);
|
||||
SASSERT(s().value(c.lit()) == l_true);
|
||||
unsigned index = 0;
|
||||
for (index = 0; index <= bound; ++index) {
|
||||
if (c[index] == alit) {
|
||||
break;
|
||||
}
|
||||
}
|
||||
if (index == bound + 1) {
|
||||
// literal is no longer watched.
|
||||
return l_undef;
|
||||
}
|
||||
SASSERT(index <= bound);
|
||||
SASSERT(c[index] == alit);
|
||||
|
||||
// find a literal to swap with:
|
||||
for (unsigned i = bound + 1; i < sz; ++i) {
|
||||
literal lit2 = c[i];
|
||||
if (s().value(lit2) != l_false) {
|
||||
c.swap(index, i);
|
||||
watch_literal(c, lit2);
|
||||
return l_undef;
|
||||
}
|
||||
}
|
||||
|
||||
// conflict
|
||||
if (bound != index && s().value(c[bound]) == l_false) {
|
||||
TRACE("sat", tout << "conflict " << c[bound] << " " << alit << "\n";);
|
||||
set_conflict(c, alit);
|
||||
return l_false;
|
||||
}
|
||||
|
||||
TRACE("pb", tout << "no swap " << index << " " << alit << "\n";);
|
||||
// there are no literals to swap with,
|
||||
// prepare for unit propagation by swapping the false literal into
|
||||
// position bound. Then literals in positions 0..bound-1 have to be
|
||||
// assigned l_true.
|
||||
if (index != bound) {
|
||||
c.swap(index, bound);
|
||||
}
|
||||
SASSERT(validate_unit_propagation(c));
|
||||
|
||||
for (unsigned i = 0; i < bound && !s().inconsistent(); ++i) {
|
||||
assign(c, c[i]);
|
||||
}
|
||||
|
||||
return s().inconsistent() ? l_false : l_true;
|
||||
}
|
||||
|
||||
void card_extension::asserted(literal l) {
|
||||
bool_var v = l.var();
|
||||
ptr_vector<card>* cards = m_var_infos[v].m_lit_watch[!l.sign()];
|
||||
if (cards != 0 && !cards->empty() && !s().inconsistent()) {
|
||||
ptr_vector<card>::iterator it = cards->begin(), it2 = it, end = cards->end();
|
||||
for (; it != end; ++it) {
|
||||
card& c = *(*it);
|
||||
if (s().value(c.lit()) != l_true) {
|
||||
continue;
|
||||
}
|
||||
switch (add_assign(c, l)) {
|
||||
case l_false: // conflict
|
||||
for (; it != end; ++it, ++it2) {
|
||||
*it2 = *it;
|
||||
}
|
||||
SASSERT(s().inconsistent());
|
||||
cards->set_end(it2);
|
||||
return;
|
||||
case l_undef: // watch literal was swapped
|
||||
break;
|
||||
case l_true: // unit propagation, keep watching the literal
|
||||
if (it2 != it) {
|
||||
*it2 = *it;
|
||||
}
|
||||
++it2;
|
||||
break;
|
||||
}
|
||||
}
|
||||
cards->set_end(it2);
|
||||
}
|
||||
|
||||
card* crd = m_var_infos[v].m_card;
|
||||
if (crd != 0 && !s().inconsistent()) {
|
||||
init_watch(*crd, !l.sign());
|
||||
}
|
||||
}
|
||||
|
||||
check_result card_extension::check() { return CR_DONE; }
|
||||
|
||||
void card_extension::push() {
|
||||
m_var_lim.push_back(m_var_trail.size());
|
||||
}
|
||||
|
||||
void card_extension::pop(unsigned n) {
|
||||
unsigned new_lim = m_var_lim.size() - n;
|
||||
unsigned sz = m_var_lim[new_lim];
|
||||
while (m_var_trail.size() > sz) {
|
||||
bool_var v = m_var_trail.back();
|
||||
m_var_trail.pop_back();
|
||||
if (v != null_bool_var) {
|
||||
card* c = m_var_infos[v].m_card;
|
||||
clear_watch(*c);
|
||||
m_var_infos[v].m_card = 0;
|
||||
dealloc(c);
|
||||
}
|
||||
}
|
||||
m_var_lim.resize(new_lim);
|
||||
}
|
||||
|
||||
void card_extension::simplify() {}
|
||||
void card_extension::clauses_modifed() {}
|
||||
lbool card_extension::get_phase(bool_var v) { return l_undef; }
|
||||
|
||||
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];
|
||||
if (w) {
|
||||
watch const& wl = *w;
|
||||
out << "watch: " << literal(v, sign) << " |-> ";
|
||||
for (unsigned i = 0; i < wl.size(); ++i) {
|
||||
out << wl[i]->lit() << " ";
|
||||
}
|
||||
out << "\n";
|
||||
}
|
||||
}
|
||||
|
||||
void card_extension::display(std::ostream& out, card& c, bool values) const {
|
||||
out << c.lit();
|
||||
if (c.lit() != null_literal) {
|
||||
if (values) {
|
||||
out << "@(" << s().value(c.lit());
|
||||
if (s().value(c.lit()) != l_undef) {
|
||||
out << ":" << s().lvl(c.lit());
|
||||
}
|
||||
out << ")";
|
||||
}
|
||||
out << c.lit() << "\n";
|
||||
}
|
||||
else {
|
||||
out << " ";
|
||||
}
|
||||
for (unsigned i = 0; i < c.size(); ++i) {
|
||||
literal l = c[i];
|
||||
out << l;
|
||||
if (values) {
|
||||
out << "@(" << s().value(l);
|
||||
if (s().value(l) != l_undef) {
|
||||
out << ":" << s().lvl(l);
|
||||
}
|
||||
out << ") ";
|
||||
}
|
||||
}
|
||||
out << " >= " << c.k() << "\n";
|
||||
}
|
||||
|
||||
std::ostream& card_extension::display(std::ostream& out) const {
|
||||
for (unsigned vi = 0; vi < m_var_infos.size(); ++vi) {
|
||||
display_watch(out, vi, false);
|
||||
display_watch(out, vi, true);
|
||||
}
|
||||
for (unsigned vi = 0; vi < m_var_infos.size(); ++vi) {
|
||||
card* c = m_var_infos[vi].m_card;
|
||||
if (c) {
|
||||
display(out, *c, true);
|
||||
}
|
||||
}
|
||||
return out;
|
||||
}
|
||||
|
||||
void card_extension::collect_statistics(statistics& st) const {
|
||||
st.update("card propagations", m_stats.m_num_propagations);
|
||||
st.update("card conflicts", m_stats.m_num_conflicts);
|
||||
}
|
||||
|
||||
bool card_extension::validate_conflict(card& c) {
|
||||
if (!validate_unit_propagation(c)) return false;
|
||||
for (unsigned i = 0; i < c.k(); ++i) {
|
||||
if (s().value(c[i]) == l_false) return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
bool card_extension::validate_unit_propagation(card const& c) {
|
||||
for (unsigned i = c.k(); i < c.size(); ++i) {
|
||||
if (s().value(c[i]) != l_false) return false;
|
||||
}
|
||||
return true;
|
||||
}
|
||||
bool card_extension::validate_lemma() {
|
||||
int value = -m_bound;
|
||||
normalize_active_coeffs();
|
||||
for (unsigned i = 0; i < m_active_vars.size(); ++i) {
|
||||
bool_var v = m_active_vars[i];
|
||||
int coeff = get_coeff(v);
|
||||
SASSERT(coeff != 0);
|
||||
if (coeff < 0 && s().value(v) != l_true) {
|
||||
value -= coeff;
|
||||
}
|
||||
else if (coeff > 0 && s().value(v) != l_false) {
|
||||
value += coeff;
|
||||
}
|
||||
}
|
||||
return value < 0;
|
||||
}
|
||||
|
||||
bool card_extension::validate_assign(literal_vector const& lits, literal lit) { return true; }
|
||||
bool card_extension::validate_conflict(literal_vector const& lits) { return true; }
|
||||
|
||||
|
||||
};
|
||||
|
||||
142
src/sat/card_extension.h
Normal file
142
src/sat/card_extension.h
Normal file
|
|
@ -0,0 +1,142 @@
|
|||
/*++
|
||||
Copyright (c) 2017 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
card_extension.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Cardinality extensions.
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2017-01-30
|
||||
|
||||
Revision History:
|
||||
|
||||
--*/
|
||||
#ifndef CARD_EXTENSION_H_
|
||||
#define CARD_EXTENSION_H_
|
||||
|
||||
#include"sat_extension.h"
|
||||
#include"sat_solver.h"
|
||||
|
||||
namespace sat {
|
||||
|
||||
class card_extension : public extension {
|
||||
struct stats {
|
||||
unsigned m_num_propagations;
|
||||
unsigned m_num_conflicts;
|
||||
stats() { reset(); }
|
||||
void reset() { memset(this, 0, sizeof(*this)); }
|
||||
};
|
||||
|
||||
class card {
|
||||
unsigned m_index;
|
||||
literal m_lit;
|
||||
unsigned m_k;
|
||||
unsigned m_size;
|
||||
literal_vector m_lits;
|
||||
public:
|
||||
card(unsigned index, literal lit, literal_vector const& lits, unsigned k);
|
||||
unsigned index() const { return m_index; }
|
||||
literal lit() const { return m_lit; }
|
||||
literal operator[](unsigned i) const { return m_lits[i]; }
|
||||
unsigned k() const { return m_k; }
|
||||
unsigned size() const { return m_size; }
|
||||
void swap(unsigned i, unsigned j) { std::swap(m_lits[i], m_lits[j]); }
|
||||
void negate();
|
||||
};
|
||||
|
||||
typedef ptr_vector<card> watch;
|
||||
struct var_info {
|
||||
watch* m_lit_watch[2];
|
||||
card* m_card;
|
||||
var_info(): m_card(0) {
|
||||
m_lit_watch[0] = 0;
|
||||
m_lit_watch[1] = 0;
|
||||
}
|
||||
void reset() {
|
||||
dealloc(m_card);
|
||||
dealloc(m_lit_watch[0]);
|
||||
dealloc(m_lit_watch[1]);
|
||||
}
|
||||
};
|
||||
|
||||
|
||||
solver* m_solver;
|
||||
stats m_stats;
|
||||
|
||||
ptr_vector<card> m_constraints;
|
||||
|
||||
// watch literals
|
||||
svector<var_info> m_var_infos;
|
||||
unsigned_vector m_var_trail;
|
||||
unsigned_vector m_var_lim;
|
||||
|
||||
// conflict resolution
|
||||
unsigned m_num_marks;
|
||||
unsigned m_conflict_lvl;
|
||||
svector<int> m_coeffs;
|
||||
svector<bool_var> m_active_vars;
|
||||
int m_bound;
|
||||
tracked_uint_set m_active_var_set;
|
||||
literal_vector m_conflict;
|
||||
literal_vector m_literals;
|
||||
|
||||
solver& s() const { return *m_solver; }
|
||||
void init_watch(card& c, bool is_true);
|
||||
void init_watch(bool_var v);
|
||||
void assign(card& c, literal lit);
|
||||
lbool add_assign(card& c, literal lit);
|
||||
void watch_literal(card& c, literal lit);
|
||||
void set_conflict(card& c, literal lit);
|
||||
void clear_watch(card& c);
|
||||
void reset_coeffs();
|
||||
|
||||
void unwatch_literal(literal w, card* c);
|
||||
void remove(ptr_vector<card>& cards, card* c);
|
||||
|
||||
void normalize_active_coeffs();
|
||||
void inc_coeff(literal l, int offset);
|
||||
int get_coeff(bool_var v) const;
|
||||
int get_abs_coeff(bool_var v) const;
|
||||
|
||||
literal_vector& get_literals() { m_literals.reset(); return m_literals; }
|
||||
literal get_asserting_literal(literal conseq);
|
||||
bool resolve_conflict(card& c, literal_vector const& conflict_clause);
|
||||
void process_antecedent(literal l, int offset);
|
||||
void process_card(card& c, int offset);
|
||||
void cut();
|
||||
|
||||
// validation utilities
|
||||
bool validate_conflict(card& c);
|
||||
bool validate_assign(literal_vector const& lits, literal lit);
|
||||
bool validate_lemma();
|
||||
bool validate_unit_propagation(card const& c);
|
||||
bool validate_conflict(literal_vector const& lits);
|
||||
|
||||
void display(std::ostream& out, card& c, bool values) const;
|
||||
void display_watch(std::ostream& out, bool_var v, bool sign) const;
|
||||
public:
|
||||
card_extension();
|
||||
virtual ~card_extension();
|
||||
void set_solver(solver* s) { m_solver = s; }
|
||||
void add_at_least(bool_var v, literal_vector const& lits, unsigned k);
|
||||
virtual void propagate(literal l, ext_constraint_idx idx, bool & keep);
|
||||
virtual void get_antecedents(literal l, ext_justification_idx idx, literal_vector & r);
|
||||
virtual void asserted(literal l);
|
||||
virtual check_result check();
|
||||
virtual void push();
|
||||
virtual void pop(unsigned n);
|
||||
virtual void simplify();
|
||||
virtual void clauses_modifed();
|
||||
virtual lbool get_phase(bool_var v);
|
||||
virtual std::ostream& display(std::ostream& out) const;
|
||||
virtual void collect_statistics(statistics& st) const;
|
||||
};
|
||||
|
||||
};
|
||||
|
||||
#endif
|
||||
|
|
@ -21,6 +21,7 @@ Revision History:
|
|||
|
||||
#include"sat_types.h"
|
||||
#include"params.h"
|
||||
#include"statistics.h"
|
||||
|
||||
namespace sat {
|
||||
|
||||
|
|
@ -30,6 +31,7 @@ namespace sat {
|
|||
|
||||
class extension {
|
||||
public:
|
||||
virtual ~extension() {}
|
||||
virtual void propagate(literal l, ext_constraint_idx idx, bool & keep) = 0;
|
||||
virtual void get_antecedents(literal l, ext_justification_idx idx, literal_vector & r) = 0;
|
||||
virtual void asserted(literal l) = 0;
|
||||
|
|
@ -39,6 +41,8 @@ namespace sat {
|
|||
virtual void simplify() = 0;
|
||||
virtual void clauses_modifed() = 0;
|
||||
virtual lbool get_phase(bool_var v) = 0;
|
||||
virtual std::ostream& display(std::ostream& out) const = 0;
|
||||
virtual void collect_statistics(statistics& st) const = 0;
|
||||
};
|
||||
|
||||
};
|
||||
|
|
|
|||
|
|
@ -33,7 +33,7 @@ namespace sat {
|
|||
explicit justification(literal l):m_val1(l.to_uint()), m_val2(BINARY) {}
|
||||
justification(literal l1, literal l2):m_val1(l1.to_uint()), m_val2(TERNARY + (l2.to_uint() << 3)) {}
|
||||
explicit justification(clause_offset cls_off):m_val1(cls_off), m_val2(CLAUSE) {}
|
||||
justification mk_ext_justification(ext_justification_idx idx) { return justification(idx, EXT_JUSTIFICATION); }
|
||||
static justification mk_ext_justification(ext_justification_idx idx) { return justification(idx, EXT_JUSTIFICATION); }
|
||||
|
||||
kind get_kind() const { return static_cast<kind>(m_val2 & 7); }
|
||||
|
||||
|
|
|
|||
|
|
@ -2752,6 +2752,7 @@ namespace sat {
|
|||
m_scc.collect_statistics(st);
|
||||
m_asymm_branch.collect_statistics(st);
|
||||
m_probing.collect_statistics(st);
|
||||
if (m_ext) m_ext->collect_statistics(st);
|
||||
}
|
||||
|
||||
void solver::reset_statistics() {
|
||||
|
|
@ -2856,6 +2857,9 @@ namespace sat {
|
|||
display_units(out);
|
||||
display_binary(out);
|
||||
out << m_clauses << m_learned;
|
||||
if (m_ext) {
|
||||
m_ext->display(out);
|
||||
}
|
||||
out << ")\n";
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -145,6 +145,7 @@ namespace sat {
|
|||
friend class probing;
|
||||
friend class iff3_finder;
|
||||
friend class mus;
|
||||
friend class card_extension;
|
||||
friend struct mk_stat;
|
||||
public:
|
||||
solver(params_ref const & p, reslimit& l, extension * ext);
|
||||
|
|
|
|||
|
|
@ -250,16 +250,6 @@ namespace smt {
|
|||
typedef map<arg_t, bool_var, arg_t::hash, arg_t::eq> arg_map;
|
||||
|
||||
|
||||
struct row_info {
|
||||
unsigned m_slack; // slack variable in simplex tableau
|
||||
numeral m_bound; // bound
|
||||
arg_t m_rep; // representative
|
||||
row_info(theory_var slack, numeral const& b, arg_t const& r):
|
||||
m_slack(slack), m_bound(b), m_rep(r) {}
|
||||
row_info(): m_slack(0) {}
|
||||
};
|
||||
|
||||
|
||||
struct var_info {
|
||||
ineq_watch* m_lit_watch[2];
|
||||
ineq_watch* m_var_watch;
|
||||
|
|
@ -290,7 +280,6 @@ namespace smt {
|
|||
theory_pb_params m_params;
|
||||
|
||||
svector<var_info> m_var_infos;
|
||||
unsynch_mpq_inf_manager m_mpq_inf_mgr; // Simplex: manage inf_mpq numerals
|
||||
mutable unsynch_mpz_manager m_mpz_mgr; // Simplex: manager mpz numerals
|
||||
unsigned_vector m_ineqs_trail;
|
||||
unsigned_vector m_ineqs_lim;
|
||||
|
|
|
|||
Loading…
Reference in a new issue