mirror of
https://github.com/Z3Prover/z3
synced 2025-04-24 01:25:31 +00:00
adding pb
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
8205b45839
commit
0ba7c9c39b
3 changed files with 487 additions and 69 deletions
|
|
@ -45,9 +45,11 @@ namespace sat {
|
|||
m_index(index),
|
||||
m_lit(lit),
|
||||
m_k(k),
|
||||
m_size(wlits.size()) {
|
||||
m_size(wlits.size()),
|
||||
m_max_sum(0) {
|
||||
for (unsigned i = 0; i < wlits.size(); ++i) {
|
||||
m_wlits[i] = wlits[i];
|
||||
m_max_sum += wlits[i].first;
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -212,14 +214,355 @@ namespace sat {
|
|||
}
|
||||
|
||||
// pb:
|
||||
void card_extension::init_watch(pb& p, bool is_true) {
|
||||
NOT_IMPLEMENTED_YET();
|
||||
|
||||
void card_extension::copy_pb(card_extension& result) {
|
||||
for (unsigned i = 0; i < m_pbs.size(); ++i) {
|
||||
svector<wliteral> wlits;
|
||||
pb& p = *m_pbs[i];
|
||||
for (unsigned i = 0; i < p.size(); ++i) {
|
||||
wlits.push_back(p[i]);
|
||||
}
|
||||
bool_var v = p.lit() == null_literal ? null_bool_var : p.lit().var();
|
||||
result.add_pb_ge(v, wlits, p.k());
|
||||
}
|
||||
}
|
||||
|
||||
// watch a prefix of literals, such that the slack of these is >= k
|
||||
void card_extension::init_watch(pb& p, bool is_true) {
|
||||
clear_watch(p);
|
||||
if (p.lit() != null_literal && p.lit().sign() == is_true) {
|
||||
p.negate();
|
||||
}
|
||||
|
||||
TRACE("sat", display(tout << "init watch: ", p, true););
|
||||
SASSERT(p.lit() == null_literal || value(p.lit()) == l_true);
|
||||
unsigned sz = p.size(), bound = p.k();
|
||||
|
||||
// put the non-false literals into the head.
|
||||
unsigned slack = 0, num_watch = 0, j = 0;
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
if (value(p[i].second) != l_false) {
|
||||
if (j != i) {
|
||||
p.swap(i, j);
|
||||
}
|
||||
if (slack < bound) {
|
||||
slack += p[i].first;
|
||||
++num_watch;
|
||||
}
|
||||
++j;
|
||||
}
|
||||
}
|
||||
DEBUG_CODE(
|
||||
bool is_false = false;
|
||||
for (unsigned k = 0; k < sz; ++k) {
|
||||
SASSERT(!is_false || value(p[k].second) == l_false);
|
||||
SASSERT(k < j == (value(p[k].second) != l_false));
|
||||
is_false = value(p[k].second) == l_false;
|
||||
});
|
||||
|
||||
if (slack < bound) {
|
||||
literal lit = p[j].second;
|
||||
SASSERT(value(p[j].second) == l_false);
|
||||
for (unsigned i = j + 1; j < sz; ++i) {
|
||||
if (lvl(lit) < lvl(p[i].second)) {
|
||||
lit = p[i].second;
|
||||
}
|
||||
}
|
||||
set_conflict(p, lit);
|
||||
}
|
||||
else {
|
||||
for (unsigned i = 0; i < num_watch; ++i) {
|
||||
watch_literal(p, p[i]);
|
||||
}
|
||||
p.set_slack(slack);
|
||||
p.set_num_watch(num_watch);
|
||||
}
|
||||
}
|
||||
|
||||
/*
|
||||
Chai Kuhlmann:
|
||||
Lw - set of watched literals
|
||||
Lu - set of unwatched literals that are not false
|
||||
|
||||
Lw = Lw \ { alit }
|
||||
Sw -= value
|
||||
a_max = max { a | l in Lw u Lu, l = undef }
|
||||
while (Sw < k + a_max & Lu != 0) {
|
||||
a_s = max { a | l in Lu }
|
||||
Sw += a_s
|
||||
Lw = Lw u {l_s}
|
||||
Lu = Lu \ {l_s}
|
||||
}
|
||||
if (Sw < bound) conflict
|
||||
while (Sw < k + a_max) {
|
||||
assign (l_max)
|
||||
a_max = max { ai | li in Lw, li = undef }
|
||||
}
|
||||
ASSERT(Sw >= bound)
|
||||
return no-conflict
|
||||
|
||||
a_max index: index of non-false literal with maximal weight.
|
||||
|
||||
|
||||
*/
|
||||
lbool card_extension::add_assign(pb& p, literal alit) {
|
||||
unsigned sz = p.size();
|
||||
unsigned bound = p.k();
|
||||
unsigned num_watch = p.num_watch();
|
||||
unsigned slack = p.slack();
|
||||
SASSERT(value(alit) == l_false);
|
||||
SASSERT(p.lit() == null_literal || value(p.lit()) == l_true);
|
||||
SASSERT(num_watch <= sz);
|
||||
unsigned index = 0;
|
||||
unsigned a_max = 0;
|
||||
unsigned max_index = 0;
|
||||
m_pb_undef.reset();
|
||||
for (; index < num_watch; ++index) {
|
||||
literal lit = p[index].second;
|
||||
if (lit == alit) {
|
||||
break;
|
||||
}
|
||||
if (value(lit) == l_undef) {
|
||||
m_pb_undef.push_back(index);
|
||||
if (p[index].first > a_max) {
|
||||
a_max = p[index].first;
|
||||
max_index = index;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
for (unsigned j = index + 1; a_max == 0 && j < num_watch; ++j) {
|
||||
literal lit = p[j].second;
|
||||
if (value(lit) == l_undef) {
|
||||
m_pb_undef.push_back(j);
|
||||
a_max = p[j].first;
|
||||
max_index = j;
|
||||
}
|
||||
}
|
||||
for (unsigned j = num_watch; a_max == 0 && j < sz; ++j) {
|
||||
literal lit = p[j].second;
|
||||
if (value(lit) == l_undef) {
|
||||
p.swap(j, num_watch);
|
||||
m_pb_undef.push_back(num_watch);
|
||||
a_max = p[num_watch].first;
|
||||
max_index = num_watch;
|
||||
}
|
||||
}
|
||||
|
||||
unsigned val = p[index].first;
|
||||
SASSERT(num_watch > 0);
|
||||
SASSERT(index < num_watch);
|
||||
SASSERT(value(p[index].second) == l_false);
|
||||
SASSERT(val <= slack);
|
||||
slack -= val;
|
||||
// find literals to swap with:
|
||||
for (unsigned j = num_watch; j < sz && slack < bound + a_max; ++j) {
|
||||
if (value(p[j].second) != l_false) {
|
||||
slack += p[j].first;
|
||||
watch_literal(p, p[j]);
|
||||
p.swap(num_watch, j);
|
||||
if (value(p[num_watch].second) == l_undef && a_max < p[num_watch].first) {
|
||||
m_pb_undef.push_back(num_watch);
|
||||
a_max = p[num_watch].first;
|
||||
max_index = num_watch;
|
||||
}
|
||||
++num_watch;
|
||||
}
|
||||
}
|
||||
|
||||
if (slack < bound) {
|
||||
// maintain watching the literal
|
||||
slack += val;
|
||||
p.set_slack(slack);
|
||||
p.set_num_watch(num_watch);
|
||||
SASSERT(bound <= slack);
|
||||
TRACE("sat", tout << "conflict " << alit << "\n";);
|
||||
set_conflict(p, alit);
|
||||
return l_false;
|
||||
}
|
||||
|
||||
// swap out the watched literal.
|
||||
p.set_slack(slack);
|
||||
--num_watch;
|
||||
SASSERT(num_watch > 0);
|
||||
p.set_num_watch(num_watch);
|
||||
p.swap(num_watch, index);
|
||||
if (num_watch == max_index) {
|
||||
max_index = index;
|
||||
}
|
||||
|
||||
SASSERT(max_index < sz);
|
||||
while (slack < bound + a_max && !s().inconsistent()) {
|
||||
// variable at max-index must be assigned to true.
|
||||
assign(p, p[max_index].second);
|
||||
|
||||
a_max = 0;
|
||||
// find the next a_max among m_pb_undef
|
||||
while (!m_pb_undef.empty() && l_undef != value(p[m_pb_undef.back()].second)) {
|
||||
m_pb_undef.pop_back();
|
||||
}
|
||||
if (m_pb_undef.empty()) {
|
||||
break;
|
||||
}
|
||||
max_index = m_pb_undef.back();
|
||||
a_max = p[max_index].first;
|
||||
m_pb_undef.pop_back();
|
||||
}
|
||||
|
||||
return s().inconsistent() ? l_false : l_true;
|
||||
}
|
||||
|
||||
void card_extension::watch_literal(pb& p, wliteral l) {
|
||||
literal lit = l.second;
|
||||
init_watch(lit.var());
|
||||
ptr_vector<pb>* pbs = m_var_infos[lit.var()].m_pb_watch[lit.sign()];
|
||||
if (pbs == 0) {
|
||||
pbs = alloc(ptr_vector<pb>);
|
||||
m_var_infos[lit.var()].m_pb_watch[lit.sign()] = pbs;
|
||||
}
|
||||
else if (is_tag_empty(pbs)) {
|
||||
pbs = set_tag_non_empty(pbs);
|
||||
m_var_infos[lit.var()].m_pb_watch[lit.sign()] = pbs;
|
||||
}
|
||||
TRACE("sat_verbose", tout << "insert: " << lit.var() << " " << lit.sign() << "\n";);
|
||||
pbs->push_back(&p);
|
||||
}
|
||||
|
||||
void card_extension::clear_watch(pb& p) {
|
||||
unsigned sz = p.size();
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
unwatch_literal(p[i].second, &p);
|
||||
}
|
||||
}
|
||||
|
||||
void card_extension::unwatch_literal(literal lit, pb* p) {
|
||||
if (m_var_infos.size() <= static_cast<unsigned>(lit.var())) {
|
||||
return;
|
||||
}
|
||||
pb_watch*& pbs = m_var_infos[lit.var()].m_pb_watch[lit.sign()];
|
||||
if (!is_tag_empty(pbs)) {
|
||||
if (remove(*pbs, p)) {
|
||||
pbs = set_tag_empty(pbs);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void card_extension::set_conflict(pb& p, literal lit) {
|
||||
m_stats.m_num_pb_conflicts++;
|
||||
TRACE("sat", display(tout, p, true); );
|
||||
// SASSERT(validate_conflict(p));
|
||||
SASSERT(value(lit) == l_false);
|
||||
s().set_conflict(justification::mk_ext_justification(p.index()), ~lit);
|
||||
SASSERT(s().inconsistent());
|
||||
}
|
||||
|
||||
void card_extension::assign(pb& p, literal lit) {
|
||||
switch (value(lit)) {
|
||||
case l_true:
|
||||
break;
|
||||
case l_false:
|
||||
set_conflict(p, lit);
|
||||
break;
|
||||
default:
|
||||
m_stats.m_num_pb_propagations++;
|
||||
m_num_propagations_since_pop++;
|
||||
if (s().m_config.m_drat) {
|
||||
svector<drat::premise> ps;
|
||||
literal_vector lits;
|
||||
get_pb_antecedents(lit, p, lits);
|
||||
lits.push_back(lit);
|
||||
ps.push_back(drat::premise(drat::s_ext(), p.lit()));
|
||||
s().m_drat.add(lits, ps);
|
||||
}
|
||||
s().assign(lit, justification::mk_ext_justification(p.index()));
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
void card_extension::display(std::ostream& out, pb& p, bool values) const {
|
||||
out << p.lit() << "[" << p.size() << "]";
|
||||
if (p.lit() != null_literal && values) {
|
||||
out << "@(" << value(p.lit());
|
||||
if (value(p.lit()) != l_undef) {
|
||||
out << ":" << lvl(p.lit());
|
||||
}
|
||||
out << "): ";
|
||||
}
|
||||
else {
|
||||
out << ": ";
|
||||
}
|
||||
for (unsigned i = 0; i < p.size(); ++i) {
|
||||
literal l = p[i].second;
|
||||
unsigned w = p[i].first;
|
||||
if (w > 1) out << w << " * ";
|
||||
out << l;
|
||||
if (values) {
|
||||
out << "@(" << value(l);
|
||||
if (value(l) != l_undef) {
|
||||
out << ":" << lvl(l);
|
||||
}
|
||||
out << ") ";
|
||||
}
|
||||
else {
|
||||
out << " ";
|
||||
}
|
||||
}
|
||||
out << ">= " << p.k() << "\n";
|
||||
}
|
||||
|
||||
void card_extension::asserted_pb(literal l, ptr_vector<pb>* pbs, pb* p0) {
|
||||
TRACE("sat", tout << l << " " << !is_tag_empty(pbs) << " " << (p0 != 0) << "\n";);
|
||||
if (!is_tag_empty(pbs)) {
|
||||
ptr_vector<pb>::iterator begin = pbs->begin();
|
||||
ptr_vector<pb>::iterator it = begin, it2 = it, end = pbs->end();
|
||||
for (; it != end; ++it) {
|
||||
pb& p = *(*it);
|
||||
if (p.lit() != null_literal && value(p.lit()) != l_true) {
|
||||
continue;
|
||||
}
|
||||
switch (add_assign(p, ~l)) {
|
||||
case l_false: // conflict
|
||||
for (; it != end; ++it, ++it2) {
|
||||
*it2 = *it;
|
||||
}
|
||||
SASSERT(s().inconsistent());
|
||||
pbs->set_end(it2);
|
||||
return;
|
||||
case l_true: // unit propagation, keep watching the literal
|
||||
if (it2 != it) {
|
||||
*it2 = *it;
|
||||
}
|
||||
++it2;
|
||||
break;
|
||||
case l_undef: // watch literal was swapped
|
||||
break;
|
||||
}
|
||||
}
|
||||
pbs->set_end(it2);
|
||||
if (pbs->empty()) {
|
||||
m_var_infos[l.var()].m_pb_watch[!l.sign()] = set_tag_empty(pbs);
|
||||
}
|
||||
}
|
||||
|
||||
if (p0 != 0 && !s().inconsistent()) {
|
||||
init_watch(*p0, !l.sign());
|
||||
}
|
||||
}
|
||||
|
||||
// xor:
|
||||
|
||||
void card_extension::copy_xor(card_extension& result) {
|
||||
for (unsigned i = 0; i < m_xors.size(); ++i) {
|
||||
literal_vector lits;
|
||||
xor& x = *m_xors[i];
|
||||
for (unsigned i = 0; i < x.size(); ++i) {
|
||||
lits.push_back(x[i]);
|
||||
}
|
||||
bool_var v = x.lit() == null_literal ? null_bool_var : x.lit().var();
|
||||
result.add_xor(v, lits);
|
||||
}
|
||||
}
|
||||
|
||||
void card_extension::clear_watch(xor& x) {
|
||||
unwatch_literal(x[0], &x);
|
||||
unwatch_literal(x[1], &x);
|
||||
|
|
@ -229,7 +572,7 @@ namespace sat {
|
|||
if (m_var_infos.size() <= static_cast<unsigned>(lit.var())) {
|
||||
return;
|
||||
}
|
||||
xor_watch* xors = m_var_infos[lit.var()].m_xor_watch;
|
||||
xor_watch*& xors = m_var_infos[lit.var()].m_xor_watch;
|
||||
if (!is_tag_empty(xors)) {
|
||||
if (remove(*xors, c)) {
|
||||
xors = set_tag_empty(xors);
|
||||
|
|
@ -384,6 +727,45 @@ namespace sat {
|
|||
return s().inconsistent() ? l_false : l_true;
|
||||
}
|
||||
|
||||
void card_extension::asserted_xor(literal l, ptr_vector<xor>* xors, xor* x) {
|
||||
TRACE("sat", tout << l << " " << !is_tag_empty(xors) << " " << (x != 0) << "\n";);
|
||||
if (!is_tag_empty(xors)) {
|
||||
ptr_vector<xor>::iterator begin = xors->begin();
|
||||
ptr_vector<xor>::iterator it = begin, it2 = it, end = xors->end();
|
||||
for (; it != end; ++it) {
|
||||
xor& c = *(*it);
|
||||
if (c.lit() != null_literal && 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());
|
||||
xors->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;
|
||||
}
|
||||
}
|
||||
xors->set_end(it2);
|
||||
if (xors->empty()) {
|
||||
m_var_infos[l.var()].m_xor_watch = set_tag_empty(xors);
|
||||
}
|
||||
}
|
||||
|
||||
if (x != 0 && !s().inconsistent()) {
|
||||
init_watch(*x, !l.sign());
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
void card_extension::normalize_active_coeffs() {
|
||||
while (!m_active_var_set.empty()) m_active_var_set.erase();
|
||||
|
|
@ -551,7 +933,15 @@ namespace sat {
|
|||
++m_stats.m_num_xor_resolves;
|
||||
}
|
||||
else if (is_pb_index(index)) {
|
||||
NOT_IMPLEMENTED_YET();
|
||||
pb& p = index2pb(index);
|
||||
m_lemma.reset();
|
||||
m_bound += offset;
|
||||
inc_coeff(consequent, offset);
|
||||
get_pb_antecedents(consequent, p, m_lemma);
|
||||
for (unsigned i = 0; i < m_lemma.size(); ++i) {
|
||||
process_antecedent(~m_lemma[i], offset);
|
||||
}
|
||||
++m_stats.m_num_pb_resolves;
|
||||
}
|
||||
else {
|
||||
UNREACHABLE();
|
||||
|
|
@ -810,10 +1200,10 @@ namespace sat {
|
|||
}
|
||||
|
||||
void card_extension::add_pb_ge(bool_var v, svector<wliteral> const& wlits, unsigned k) {
|
||||
unsigned index = 4*m_pb.size() + 0x11;
|
||||
unsigned index = 4*m_pbs.size() + 0x11;
|
||||
literal lit = v == null_bool_var ? null_literal : literal(v, false);
|
||||
pb* p = new (memory::allocate(pb::get_obj_size(wlits.size()))) pb(index, lit, wlits, k);
|
||||
m_pb.push_back(p);
|
||||
m_pbs.push_back(p);
|
||||
if (v == null_bool_var) {
|
||||
init_watch(*p, true);
|
||||
m_pb_axioms.push_back(p);
|
||||
|
|
@ -946,6 +1336,25 @@ namespace sat {
|
|||
TRACE("sat", tout << r << "\n";);
|
||||
}
|
||||
|
||||
void card_extension::get_pb_antecedents(literal l, pb const& p, literal_vector& r) {
|
||||
if (p.lit() != null_literal) r.push_back(p.lit());
|
||||
SASSERT(p.lit() == null_literal || value(p.lit()) == l_true);
|
||||
unsigned k = p.k();
|
||||
unsigned max_sum = p.max_sum();
|
||||
for (unsigned i = p.size(); i > 0 && max_sum >= k; ) {
|
||||
--i;
|
||||
literal lit = p[i].second;
|
||||
if (lit == l) {
|
||||
max_sum -= p[i].first;
|
||||
}
|
||||
else if (value(lit) == l_false) {
|
||||
r.push_back(~p[i].second);
|
||||
max_sum -= p[i].first;
|
||||
}
|
||||
}
|
||||
SASSERT(max_sum < k);
|
||||
}
|
||||
|
||||
void card_extension::get_antecedents(literal l, ext_justification_idx idx, literal_vector & r) {
|
||||
if (is_card_index(idx)) {
|
||||
card& c = index2card(idx);
|
||||
|
|
@ -984,7 +1393,8 @@ namespace sat {
|
|||
}
|
||||
}
|
||||
else if (is_pb_index(idx)) {
|
||||
NOT_IMPLEMENTED_YET();
|
||||
pb const& p = index2pb(idx);
|
||||
get_pb_antecedents(l, p, r);
|
||||
}
|
||||
else {
|
||||
UNREACHABLE();
|
||||
|
|
@ -1054,9 +1464,11 @@ namespace sat {
|
|||
if (v >= m_var_infos.size()) return;
|
||||
var_info& vinfo = m_var_infos[v];
|
||||
ptr_vector<card>* cards = vinfo.m_card_watch[!l.sign()];
|
||||
ptr_vector<xor>* xors = vinfo.m_xor_watch;
|
||||
ptr_vector<pb>* pbs = vinfo.m_pb_watch[!l.sign()];
|
||||
pb* p = vinfo.m_pb;
|
||||
card* crd = vinfo.m_card;
|
||||
xor* x = vinfo.m_xor;
|
||||
ptr_vector<xor>* xors = vinfo.m_xor_watch;
|
||||
|
||||
if (!is_tag_empty(cards)) {
|
||||
ptr_vector<card>::iterator begin = cards->begin();
|
||||
|
|
@ -1093,51 +1505,17 @@ namespace sat {
|
|||
if (crd != 0 && !s().inconsistent()) {
|
||||
init_watch(*crd, !l.sign());
|
||||
}
|
||||
|
||||
if ((!is_tag_empty(pbs) || p) && !s().inconsistent()) {
|
||||
asserted_pb(l, pbs, p);
|
||||
}
|
||||
|
||||
if (m_has_xor && !s().inconsistent()) {
|
||||
asserted_xor(l, xors, x);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
void card_extension::asserted_xor(literal l, ptr_vector<xor>* xors, xor* x) {
|
||||
TRACE("sat", tout << l << " " << !is_tag_empty(xors) << " " << (x != 0) << "\n";);
|
||||
if (!is_tag_empty(xors)) {
|
||||
ptr_vector<xor>::iterator begin = xors->begin();
|
||||
ptr_vector<xor>::iterator it = begin, it2 = it, end = xors->end();
|
||||
for (; it != end; ++it) {
|
||||
xor& c = *(*it);
|
||||
if (c.lit() != null_literal && 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());
|
||||
xors->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;
|
||||
}
|
||||
}
|
||||
xors->set_end(it2);
|
||||
if (xors->empty()) {
|
||||
m_var_infos[l.var()].m_xor_watch = set_tag_empty(xors);
|
||||
}
|
||||
}
|
||||
|
||||
if (x != 0 && !s().inconsistent()) {
|
||||
init_watch(*x, !l.sign());
|
||||
}
|
||||
}
|
||||
|
||||
check_result card_extension::check() { return CR_DONE; }
|
||||
|
||||
void card_extension::push() {
|
||||
|
|
@ -1153,13 +1531,17 @@ namespace sat {
|
|||
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);
|
||||
if (c) {
|
||||
clear_watch(*c);
|
||||
m_var_infos[v].m_card = 0;
|
||||
dealloc(c);
|
||||
}
|
||||
xor* x = m_var_infos[v].m_xor;
|
||||
clear_watch(*x);
|
||||
m_var_infos[v].m_xor = 0;
|
||||
dealloc(x);
|
||||
if (x) {
|
||||
clear_watch(*x);
|
||||
m_var_infos[v].m_xor = 0;
|
||||
dealloc(x);
|
||||
}
|
||||
}
|
||||
}
|
||||
m_var_lim.resize(new_lim);
|
||||
|
|
@ -1182,15 +1564,8 @@ namespace sat {
|
|||
bool_var v = c.lit() == null_literal ? null_bool_var : c.lit().var();
|
||||
result->add_at_least(v, lits, c.k());
|
||||
}
|
||||
for (unsigned i = 0; i < m_xors.size(); ++i) {
|
||||
literal_vector lits;
|
||||
xor& x = *m_xors[i];
|
||||
for (unsigned i = 0; i < x.size(); ++i) {
|
||||
lits.push_back(x[i]);
|
||||
}
|
||||
bool_var v = x.lit() == null_literal ? null_bool_var : x.lit().var();
|
||||
result->add_xor(v, lits);
|
||||
}
|
||||
copy_xor(*result);
|
||||
copy_pb(*result);
|
||||
return result;
|
||||
}
|
||||
|
||||
|
|
@ -1347,7 +1722,15 @@ namespace sat {
|
|||
}
|
||||
}
|
||||
else if (is_pb_index(idx)) {
|
||||
NOT_IMPLEMENTED_YET();
|
||||
pb& p = index2pb(idx);
|
||||
out << "pb " << p.lit() << ": ";
|
||||
for (unsigned i = 0; i < p.size(); ++i) {
|
||||
if (p[i].first != 1) {
|
||||
out << p[i].first << " ";
|
||||
}
|
||||
out << p[i].second << " ";
|
||||
}
|
||||
out << ">= " << p.k();
|
||||
}
|
||||
else {
|
||||
UNREACHABLE();
|
||||
|
|
@ -1362,6 +1745,9 @@ namespace sat {
|
|||
st.update("xor propagations", m_stats.m_num_xor_propagations);
|
||||
st.update("xor conflicts", m_stats.m_num_xor_conflicts);
|
||||
st.update("xor resolves", m_stats.m_num_xor_resolves);
|
||||
st.update("pb propagations", m_stats.m_num_pb_propagations);
|
||||
st.update("pb conflicts", m_stats.m_num_pb_conflicts);
|
||||
st.update("pb resolves", m_stats.m_num_pb_resolves);
|
||||
}
|
||||
|
||||
bool card_extension::validate_conflict(card& c) {
|
||||
|
|
@ -1457,7 +1843,12 @@ namespace sat {
|
|||
if (lxor != null_literal) p.push(~lxor, offset);
|
||||
}
|
||||
else if (is_pb_index(index)) {
|
||||
NOT_IMPLEMENTED_YET();
|
||||
pb& pb = index2pb(index);
|
||||
p.reset(pb.k());
|
||||
for (unsigned i = 0; i < pb.size(); ++i) {
|
||||
p.push(pb[i].second, pb[i].first);
|
||||
}
|
||||
if (pb.lit() != null_literal) p.push(~pb.lit(), pb.k());
|
||||
}
|
||||
else {
|
||||
UNREACHABLE();
|
||||
|
|
|
|||
|
|
@ -36,6 +36,9 @@ namespace sat {
|
|||
unsigned m_num_xor_propagations;
|
||||
unsigned m_num_xor_conflicts;
|
||||
unsigned m_num_xor_resolves;
|
||||
unsigned m_num_pb_propagations;
|
||||
unsigned m_num_pb_conflicts;
|
||||
unsigned m_num_pb_resolves;
|
||||
stats() { reset(); }
|
||||
void reset() { memset(this, 0, sizeof(*this)); }
|
||||
};
|
||||
|
|
@ -66,6 +69,9 @@ namespace sat {
|
|||
literal m_lit;
|
||||
unsigned m_k;
|
||||
unsigned m_size;
|
||||
unsigned m_slack;
|
||||
unsigned m_num_watch;
|
||||
unsigned m_max_sum;
|
||||
wliteral m_wlits[0];
|
||||
public:
|
||||
static size_t get_obj_size(unsigned num_lits) { return sizeof(card) + num_lits * sizeof(wliteral); }
|
||||
|
|
@ -75,6 +81,11 @@ namespace sat {
|
|||
wliteral operator[](unsigned i) const { return m_wlits[i]; }
|
||||
unsigned k() const { return m_k; }
|
||||
unsigned size() const { return m_size; }
|
||||
unsigned slack() const { return m_slack; }
|
||||
void set_slack(unsigned s) { m_slack = s; }
|
||||
unsigned num_watch() const { return m_num_watch; }
|
||||
unsigned max_sum() const { return m_max_sum; }
|
||||
void set_num_watch(unsigned s) { m_num_watch = s; }
|
||||
void swap(unsigned i, unsigned j) { std::swap(m_wlits[i], m_wlits[j]); }
|
||||
void negate();
|
||||
};
|
||||
|
|
@ -153,7 +164,7 @@ namespace sat {
|
|||
|
||||
ptr_vector<card> m_cards;
|
||||
ptr_vector<xor> m_xors;
|
||||
ptr_vector<pb> m_pb;
|
||||
ptr_vector<pb> m_pbs;
|
||||
|
||||
scoped_ptr_vector<card> m_card_axioms;
|
||||
scoped_ptr_vector<pb> m_pb_axioms;
|
||||
|
|
@ -175,6 +186,9 @@ namespace sat {
|
|||
bool m_has_xor;
|
||||
unsigned_vector m_parity_marks;
|
||||
literal_vector m_parity_trail;
|
||||
|
||||
unsigned_vector m_pb_undef;
|
||||
|
||||
void ensure_parity_size(bool_var v);
|
||||
unsigned get_parity(bool_var v);
|
||||
void inc_parity(bool_var v);
|
||||
|
|
@ -193,6 +207,7 @@ namespace sat {
|
|||
void unwatch_literal(literal w, card* c);
|
||||
|
||||
// xor specific functionality
|
||||
void copy_xor(card_extension& result);
|
||||
void clear_watch(xor& x);
|
||||
void watch_literal(xor& x, literal lit);
|
||||
void unwatch_literal(literal w, xor* x);
|
||||
|
|
@ -202,17 +217,28 @@ namespace sat {
|
|||
bool parity(xor const& x, unsigned offset) const;
|
||||
lbool add_assign(xor& x, literal alit);
|
||||
void asserted_xor(literal l, ptr_vector<xor>* xors, xor* x);
|
||||
void get_xor_antecedents(literal l, unsigned index, justification js, literal_vector& r);
|
||||
|
||||
|
||||
bool is_card_index(unsigned idx) const { return 0x00 == (idx & 0x11); }
|
||||
bool is_xor_index(unsigned idx) const { return 0x01 == (idx & 0x11); }
|
||||
bool is_pb_index(unsigned idx) const { return 0x11 == (idx & 0x11); }
|
||||
card& index2card(unsigned idx) const { SASSERT(is_card_index(idx)); return *m_cards[idx >> 2]; }
|
||||
xor& index2xor(unsigned idx) const { SASSERT(!is_card_index(idx)); return *m_xors[idx >> 2]; }
|
||||
pb& index2pb(unsigned idx) const { SASSERT(is_pb_index(idx)); return *m_pb[idx >> 2]; }
|
||||
pb& index2pb(unsigned idx) const { SASSERT(is_pb_index(idx)); return *m_pbs[idx >> 2]; }
|
||||
|
||||
void get_xor_antecedents(literal l, unsigned inddex, justification js, literal_vector& r);
|
||||
|
||||
// pb functionality
|
||||
void copy_pb(card_extension& result);
|
||||
void asserted_pb(literal l, ptr_vector<pb>* pbs, pb* p);
|
||||
void init_watch(pb& p, bool is_true);
|
||||
lbool add_assign(pb& p, literal alit);
|
||||
void watch_literal(pb& p, wliteral lit);
|
||||
void clear_watch(pb& p);
|
||||
void set_conflict(pb& p, literal lit);
|
||||
void assign(pb& p, literal l);
|
||||
void unwatch_literal(literal w, pb* p);
|
||||
void get_pb_antecedents(literal l, pb const& p, literal_vector & r);
|
||||
|
||||
|
||||
template<typename T>
|
||||
|
|
@ -260,6 +286,7 @@ namespace sat {
|
|||
|
||||
void display(std::ostream& out, ineq& p) const;
|
||||
void display(std::ostream& out, card& c, bool values) const;
|
||||
void display(std::ostream& out, pb& p, bool values) const;
|
||||
void display(std::ostream& out, xor& c, bool values) const;
|
||||
void display_watch(std::ostream& out, bool_var v) const;
|
||||
void display_watch(std::ostream& out, bool_var v, bool sign) const;
|
||||
|
|
|
|||
|
|
@ -191,7 +191,7 @@ namespace sat {
|
|||
m_elim_counter = m_res_limit;
|
||||
m_old_num_elim_vars = m_num_elim_vars;
|
||||
|
||||
scoped_finalize _scoped_finalize(*this);
|
||||
// scoped_finalize _scoped_finalize(*this);
|
||||
|
||||
do {
|
||||
if (m_subsumption)
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue