mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-25 01:55:32 +00:00
Code Activity

streamline propagation

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-09-19 08:30:51 -04:00
parent 663b61b612
commit 16d48c17dd
2 changed files with 34 additions and 38 deletions
Download patch file Download diff file Expand all files Collapse all files

69
src/math/polysat/solver.cpp
View file

@ -155,7 +155,7 @@ namespace polysat {
else if (c.is_always_false())
m_conflict.set(c);
else
propagate_bool(c.blit(), c->unit_clause());
propagate_bool_at(m_level, c.blit(), c->unit_clause());
}
bool solver::can_propagate() {
@ -178,37 +178,24 @@ namespace polysat {
SASSERT(assignment_invariant());
}
void solver::propagate_watch(sat::literal lit) {
LOG("propagate " << lit);
auto& wlist = m_bvars.watch(~lit);
unsigned j = 0, end = 0;
unsigned sz = wlist.size();
for (; j < sz && !is_conflict(); ++j) {
clause& cl = *wlist[j];
SASSERT(cl.size() >= 2);
unsigned idx = cl[0] == ~lit ? 1 : 0;
SASSERT(cl[1 - idx] == ~lit);
if (m_bvars.is_true(cl[idx])) {
wlist[end++] = &cl;
continue;
}
unsigned i = 2;
for (; i < cl.size() && m_bvars.is_false(cl[i]); ++i);
if (i < cl.size()) {
m_bvars.watch(cl[i]).push_back(&cl);
std::swap(cl[1 - idx], cl[i]);
continue;
}
wlist[end++] = &cl;
if (m_bvars.is_false(cl[idx])) {
set_conflict(cl);
continue;
}
assign_bool(level(cl), cl[idx], &cl, nullptr);
bool solver::propagate(sat::literal lit, clause& cl) {
SASSERT(cl.size() >= 2);
unsigned idx = cl[0] == ~lit ? 1 : 0;
SASSERT(cl[1 - idx] == ~lit);
if (m_bvars.is_true(cl[idx]))
return true;
unsigned i = 2;
for (; i < cl.size() && m_bvars.is_false(cl[i]); ++i);
if (i < cl.size()) {
m_bvars.watch(cl[i]).push_back(&cl);
std::swap(cl[1 - idx], cl[i]);
return false;
}
for (; j < sz; ++j)
wlist[end++] = wlist[j];
wlist.shrink(end);
if (m_bvars.is_false(cl[idx]))
set_conflict(cl);
else
assign_bool(level(cl), cl[idx], &cl, nullptr);
return true;
}
void solver::linear_propagate() {
@ -223,14 +210,27 @@ namespace polysat {
#endif
}
/**
* Propagate assignment to a Boolean variable
*/
void solver::propagate(sat::literal lit) {
LOG_H2("Propagate bool " << lit);
signed_constraint c = lit2cnstr(lit);
SASSERT(c);
activate_constraint(c);
propagate_watch(lit);
auto& wlist = m_bvars.watch(~lit);
unsigned i = 0, j = 0, sz = wlist.size();
for (; i < sz && !is_conflict(); ++i)
if (!propagate(lit, *wlist[i]))
wlist[j++] = wlist[i];
for (; i < sz; ++i)
wlist[j++] = wlist[i];
wlist.shrink(j);
}
/**
* Propagate assignment to a pvar
*/
void solver::propagate(pvar v) {
LOG_H2("Propagate v" << v);
auto& wlist = m_pwatch[v];
@ -587,7 +587,7 @@ namespace polysat {
push_cjust(lemma.justified_var(), c);
if (num_choices == 1)
propagate_bool(choice, &lemma);
propagate_bool_at(level(lemma), choice, &lemma);
else
decide_bool(choice, &lemma);
}
@ -686,9 +686,6 @@ namespace polysat {
assign_bool(m_level, lit, nullptr, lemma);
}
void solver::propagate_bool(sat::literal lit, clause* reason) {
propagate_bool_at(m_level, lit, reason);
}
void solver::propagate_bool_at(unsigned level, sat::literal lit, clause* reason) {
LOG("Propagate boolean literal " << lit << " @ " << level << " by " << show_deref(reason));

3
src/math/polysat/solver.h
View file

@ -153,7 +153,6 @@ namespace polysat {
void deactivate_constraint(signed_constraint c);
void decide_bool(clause& lemma);
void decide_bool(sat::literal lit, clause* lemma);
void propagate_bool(sat::literal lit, clause* reason);
void propagate_bool_at(unsigned level, sat::literal lit, clause* reason);
unsigned level(clause const& cl);
@ -167,7 +166,7 @@ namespace polysat {
void propagate(sat::literal lit);
void propagate(pvar v);
void propagate(pvar v, rational const& val, signed_constraint c);
void propagate_watch(sat::literal lit);
bool propagate(sat::literal lit, clause& cl);
void erase_watch(pvar v, signed_constraint c);
void erase_watch(signed_constraint c);
void add_watch(signed_constraint c);