mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 09:35:32 +00:00
Code Activity

Remove active flag from constraint

Browse source 
Superseded by boolean assignment and pwatch
This commit is contained in:
Jakob Rath 2022-11-22 14:45:21 +01:00
parent da762700d6
commit e4999b07aa
3 changed files with 4 additions and 31 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -59,7 +59,6 @@ namespace polysat {
ckind_t m_kind;
unsigned_vector m_vars;
lbool m_external_sign = l_undef;
bool m_is_active = false;
bool m_is_pwatched = false;
/** The boolean variable associated to this constraint */
sat::bool_var m_bvar = sat::null_bool_var;
@ -114,9 +113,6 @@ namespace polysat {
bool is_external() const { return m_external_sign != l_undef; }
bool external_sign() const { SASSERT(is_external()); return m_external_sign == l_true; }
bool is_active() const { return m_is_active; }
void set_active(bool f) { m_is_active = f; }
bool is_pwatched() const { return m_is_pwatched; }
void set_pwatched(bool f) { m_is_pwatched = f; }

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

@ -208,10 +208,6 @@ namespace polysat {
LOG_H2("Propagate bool " << lit << "@" << m_bvars.level(lit) << " " << m_level << " qhead: " << m_qhead);
LOG("Literal " << lit_pp(*this, lit));
signed_constraint c = lit2cnstr(lit);
SASSERT(c);
// TODO: review active and activate_constraint
if (c->is_active())
return;
activate_constraint(c);
auto& wlist = m_bvars.watch(~lit);
unsigned i = 0, j = 0, sz = wlist.size();
@ -262,11 +258,9 @@ namespace polysat {
return true;
}
}
// at most one poly variable remains unassigned.
// at most one pvar remains unassigned
if (m_bvars.is_assigned(c->bvar())) {
// constraint state: bool-propagated
// // constraint is active, propagate it
// SASSERT(c->is_active()); // TODO: what exactly does 'active' mean now ... use 'pwatched' and similar instead, to make meaning explicit?
signed_constraint sc(c, m_bvars.value(c->bvar()) == l_true);
if (c->vars().size() >= 2) {
unsigned other_v = c->var(1 - idx);
@ -275,9 +269,7 @@ namespace polysat {
}
sc.narrow(*this, false);
} else {
// constraint state: active but unassigned (bvalue undef, but pwatch is set and active; e.g., new constraints generated for lemmas)
// // constraint is not yet active, try to evaluate it
// SASSERT(!c->is_active());
// constraint state: active but unassigned (bvalue undef, but pwatch is set; e.g., new constraints generated for lemmas)
if (c->vars().size() >= 2) {
unsigned other_v = c->var(1 - idx);
// Wait for the remaining variable to be assigned
@ -423,7 +415,6 @@ namespace polysat {
case trail_instr_t::pwatch_i: {
constraint* c = m_pwatch_trail.back();
erase_pwatch(c);
c->set_active(false); // TODO: review meaning of "active"
m_pwatch_trail.pop_back();
break;
}
@ -475,9 +466,6 @@ namespace polysat {
LOG_V("Undo assign_bool_i: " << lit);
unsigned active_level = m_bvars.level(lit);
if (c->is_active())
deactivate_constraint(c);
if (active_level <= target_level)
replay.push_back(lit);
else
@ -922,7 +910,7 @@ namespace polysat {
// Unfortunately, this isn't always possible.
// Consider if the first side lemma contains a constraint that comes from a boolean decision:
//
// 76: v10 + v7 + -1*v0 + -1 == 0 [ l_true decide@5 pwatched active ]
// 76: v10 + v7 + -1*v0 + -1 == 0 [ l_true decide@5 pwatched ]
//
// When we now backtrack behind the decision level of the literal, then we cannot propagate the side lemma,
// and some literals of the main lemma may still be undef at this point.
@ -1005,9 +993,7 @@ namespace polysat {
void solver::activate_constraint(signed_constraint c) {
SASSERT(c);
LOG("Activating constraint: " << c);
SASSERT(m_bvars.value(c.blit()) == l_true);
SASSERT(!c->is_active());
c->set_active(true);
SASSERT_EQ(m_bvars.value(c.blit()), l_true);
add_pwatch(c.get());
if (c->vars().size() == 1)
m_viable_fallback.push_constraint(c->var(0), c);
@ -1017,12 +1003,6 @@ namespace polysat {
#endif
}
/// Deactivate constraint
void solver::deactivate_constraint(signed_constraint c) {
LOG_V("Deactivating constraint: " << c.blit());
c->set_active(false);
}
void solver::backjump(unsigned new_level) {
if (m_level != new_level) {
LOG_H3("Backjumping to level " << new_level << " from level " << m_level);
@ -1222,8 +1202,6 @@ namespace polysat {
}
if (c->is_pwatched())
out << " pwatched";
if (c->is_active())
out << " active";
if (c->is_external())
out << " ext";
out << " ]";

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

@ -173,7 +173,6 @@ namespace polysat {
void assign_decision(sat::literal lit);
void assign_eval(sat::literal lit);
void activate_constraint(signed_constraint c);
void deactivate_constraint(signed_constraint c);
unsigned level(sat::literal lit, clause const& cl);
void assign_propagate(pvar v, rational const& val);