mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 20:33:38 +00:00
Code Activity

disable assertions for now; some notes

Browse source
This commit is contained in:
Jakob Rath 2022-08-25 16:40:38 +02:00
parent 41b74ab215
commit b31931bb9f
1 changed files with 12 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -242,6 +242,7 @@ namespace polysat {
LOG_H2("Propagate bool " << lit << "@" << m_bvars.level(lit) << " " << m_level << " qhead: " << m_qhead); LOG_H2("Propagate bool " << lit << "@" << m_bvars.level(lit) << " " << m_level << " qhead: " << m_qhead);
signed_constraint c = lit2cnstr(lit); signed_constraint c = lit2cnstr(lit);
SASSERT(c); SASSERT(c);
// TODO: review active and activate_constraint
if (c->is_active()) if (c->is_active())
return; return;
activate_constraint(c); activate_constraint(c);
@ -296,8 +297,9 @@ namespace polysat {
} }
// at most one poly variable remains unassigned. // at most one poly variable remains unassigned.
if (m_bvars.is_assigned(c->bvar())) { if (m_bvars.is_assigned(c->bvar())) {
// constraint is active, propagate it // constraint state: bool-propagated
SASSERT(c->is_active()); // // 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); signed_constraint sc(c, m_bvars.value(c->bvar()) == l_true);
if (c->vars().size() >= 2) { if (c->vars().size() >= 2) {
unsigned other_v = c->var(1 - idx); unsigned other_v = c->var(1 - idx);
@ -306,8 +308,9 @@ namespace polysat {
} }
sc.narrow(*this, false); sc.narrow(*this, false);
} else { } else {
// constraint is not yet active, try to evaluate it // constraint state: active but unassigned (bvalue undef, but pwatch is set and active; e.g., new constraints generated for lemmas)
SASSERT(!c->is_active()); // // constraint is not yet active, try to evaluate it
// SASSERT(!c->is_active());
if (c->vars().size() >= 2) { if (c->vars().size() >= 2) {
unsigned other_v = c->var(1 - idx); unsigned other_v = c->var(1 - idx);
// Wait for the remaining variable to be assigned // Wait for the remaining variable to be assigned
@ -427,8 +430,10 @@ namespace polysat {
m_free_pvars.del_var_eh(v); m_free_pvars.del_var_eh(v);
assign_core(v, val, justification::propagation(m_level)); assign_core(v, val, justification::propagation(m_level));
} }
else else {
set_conflict(c); UNREACHABLE();
// set_conflict(c);
}
} }
void solver::push_level() { void solver::push_level() {
@ -834,7 +839,6 @@ namespace polysat {
SASSERT(!lemma.empty()); SASSERT(!lemma.empty());
m_simplify_clause.apply(lemma); m_simplify_clause.apply(lemma);
add_clause(lemma); add_clause(lemma);
// TODO: add pwatch?
} }
/** /**
@ -943,6 +947,7 @@ namespace polysat {
if (!clause.is_redundant()) { if (!clause.is_redundant()) {
// for (at least) non-redundant clauses, we also need to watch the constraints // for (at least) non-redundant clauses, we also need to watch the constraints
// so we can discover when the clause should propagate // so we can discover when the clause should propagate
// TODO: check if we also need pwatch for redundant clauses
for (sat::literal lit : clause) for (sat::literal lit : clause)
add_pwatch(m_constraints.lookup(lit.var())); add_pwatch(m_constraints.lookup(lit.var()));
} }