mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-02 02:48:47 +00:00
Code Activity

update set/unset mark for propagation

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-09-13 13:14:07 +02:00
parent bb227c0d6e
commit 73b4e7f2a8
4 changed files with 11 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/math/polysat/conflict_core.cpp
View file

@ -66,7 +66,7 @@ namespace polysat {
void conflict_core::reset() { void conflict_core::reset() {
for (auto c : *this) for (auto c : *this)
unset_mark(c.get()); unset_mark(c);
m_constraints.reset(); m_constraints.reset();
m_literals.reset(); m_literals.reset();
m_vars.reset(); m_vars.reset();
@ -113,7 +113,7 @@ namespace polysat {
SASSERT(!c.is_always_false()); SASSERT(!c.is_always_false());
if (c->is_marked()) if (c->is_marked())
return; return;
set_mark(c.get()); set_mark(c);
if (c->has_bvar()) if (c->has_bvar())
insert_literal(c.blit()); insert_literal(c.blit());
else else
@ -126,7 +126,7 @@ namespace polysat {
} }
void conflict_core::remove(signed_constraint c) { void conflict_core::remove(signed_constraint c) {
unset_mark(c.get()); unset_mark(c);
if (c->has_bvar()) { if (c->has_bvar()) {
SASSERT(std::count(m_constraints.begin(), m_constraints.end(), c) == 0); SASSERT(std::count(m_constraints.begin(), m_constraints.end(), c) == 0);
remove_literal(c.blit()); remove_literal(c.blit());
@ -144,7 +144,7 @@ namespace polysat {
unsigned j = 0; unsigned j = 0;
for (unsigned i = 0; i < m_constraints.size(); ++i) for (unsigned i = 0; i < m_constraints.size(); ++i)
if (m_constraints[i]->contains_var(v)) if (m_constraints[i]->contains_var(v))
unset_mark(m_constraints[i].get()); unset_mark(m_constraints[i]);
else else
m_constraints[j++] = m_constraints[i]; m_constraints[j++] = m_constraints[i];
@ -172,7 +172,7 @@ namespace polysat {
if (c->bvar() != var) if (c->bvar() != var)
m_constraints[j++] = c; m_constraints[j++] = c;
else else
unset_mark(c.get()); unset_mark(c);
} }
m_constraints.shrink(j); m_constraints.shrink(j);
@ -333,10 +333,10 @@ namespace polysat {
return false; return false;
} }
void conflict_core::set_mark(constraint* c) { void conflict_core::set_mark(signed_constraint c) {
if (c->is_marked()) if (c->is_marked())
return; return;
bool bool_propagated = c->has_bvar() && s().m_bvars.is_assigned(c->bvar()); bool bool_propagated = c->has_bvar() && s().m_bvars.value(c.blit()) == l_true;
c->set_mark(); c->set_mark();
if (c->has_bvar()) if (c->has_bvar())
set_bmark(c->bvar()); set_bmark(c->bvar());
@ -347,7 +347,7 @@ namespace polysat {
inc_pref(v); inc_pref(v);
} }
void conflict_core::unset_mark(constraint* c) { void conflict_core::unset_mark(signed_constraint c) {
if (!c->is_marked()) if (!c->is_marked())
return; return;
c->unset_mark(); c->unset_mark();

4
src/math/polysat/conflict_core.h
View file

@ -42,8 +42,8 @@ namespace polysat {
void set_bmark(sat::bool_var b); void set_bmark(sat::bool_var b);
void unset_bmark(sat::bool_var b); void unset_bmark(sat::bool_var b);
void set_mark(constraint* c); void set_mark(signed_constraint c);
void unset_mark(constraint* c); void unset_mark(signed_constraint c);
void insert_literal(sat::literal lit); void insert_literal(sat::literal lit);
void remove_literal(sat::literal lit); void remove_literal(sat::literal lit);

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

@ -99,7 +99,6 @@ namespace polysat {
return sz2pdd(sz).mk_val(v); return sz2pdd(sz).mk_val(v);
} }
void solver::del_var() { void solver::del_var() {
// TODO also remove v from all learned constraints. // TODO also remove v from all learned constraints.
pvar v = m_value.size() - 1; pvar v = m_value.size() - 1;

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

@ -282,6 +282,7 @@ namespace polysat {
unsigned get_level(pvar v) const { SASSERT(is_assigned(v)); return m_justification[v].level(); } unsigned get_level(pvar v) const { SASSERT(is_assigned(v)); return m_justification[v].level(); }
/** /**
* Create polynomial constraints (but do not activate them). * Create polynomial constraints (but do not activate them).
* Each constraint is tracked by a dependency. * Each constraint is tracked by a dependency.