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

Track set of variables that occur in conflict constraints

Browse source
This commit is contained in:
Jakob Rath 2022-10-31 15:18:48 +01:00
parent eba59356f3
commit 6a03df9017
2 changed files with 11 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/math/polysat/conflict.cpp
View file

@ -147,6 +147,7 @@ namespace polysat {
SASSERT(m_literals.empty()); SASSERT(m_literals.empty());
SASSERT(m_vars.empty()); SASSERT(m_vars.empty());
SASSERT(m_bail_vars.empty()); SASSERT(m_bail_vars.empty());
SASSERT(m_vars_occurring.empty());
SASSERT(m_lemmas.empty()); SASSERT(m_lemmas.empty());
SASSERT(m_narrow_queue.empty()); SASSERT(m_narrow_queue.empty());
} }
@ -159,6 +160,7 @@ namespace polysat {
m_bail_vars.reset(); m_bail_vars.reset();
m_relevant_vars.reset(); m_relevant_vars.reset();
m_var_occurrences.reset(); m_var_occurrences.reset();
m_vars_occurring.reset();
m_lemmas.reset(); m_lemmas.reset();
m_narrow_queue.reset(); m_narrow_queue.reset();
m_kind = conflict_kind_t::ok; m_kind = conflict_kind_t::ok;
@ -302,6 +304,8 @@ namespace polysat {
for (pvar v : c->vars()) { for (pvar v : c->vars()) {
if (v >= m_var_occurrences.size()) if (v >= m_var_occurrences.size())
m_var_occurrences.resize(v + 1, 0); m_var_occurrences.resize(v + 1, 0);
if (!m_var_occurrences[v])
m_vars_occurring.insert(v);
m_var_occurrences[v]++; m_var_occurrences[v]++;
} }
} }
@ -380,8 +384,11 @@ namespace polysat {
void conflict::remove(signed_constraint c) { void conflict::remove(signed_constraint c) {
SASSERT(contains(c)); SASSERT(contains(c));
m_literals.remove(c.blit().index()); m_literals.remove(c.blit().index());
for (pvar v : c->vars()) for (pvar v : c->vars()) {
m_var_occurrences[v]--; m_var_occurrences[v]--;
if (!m_var_occurrences[v])
m_vars_occurring.remove(v);
}
} }
void conflict::remove_all() { void conflict::remove_all() {
@ -391,6 +398,7 @@ namespace polysat {
m_bail_vars.reset(); m_bail_vars.reset();
m_relevant_vars.reset(); m_relevant_vars.reset();
m_var_occurrences.reset(); m_var_occurrences.reset();
m_vars_occurring.reset();
m_kind = conflict_kind_t::ok; m_kind = conflict_kind_t::ok;
} }

2
src/math/polysat/conflict.h
View file

@ -107,6 +107,7 @@ namespace polysat {
uint_set m_relevant_vars; // tracked for cone of influence but not directly involved in conflict resolution uint_set m_relevant_vars; // tracked for cone of influence but not directly involved in conflict resolution
unsigned_vector m_var_occurrences; // for each variable, the number of constraints in m_literals that contain it unsigned_vector m_var_occurrences; // for each variable, the number of constraints in m_literals that contain it
uint_set m_vars_occurring; // set of variables that occur in at least one of the constraints in m_literals
// Additional lemmas that justify new constraints generated during conflict resolution // Additional lemmas that justify new constraints generated during conflict resolution
clause_ref_vector m_lemmas; clause_ref_vector m_lemmas;
@ -177,6 +178,7 @@ namespace polysat {
bool contains(sat::literal lit) const; bool contains(sat::literal lit) const;
bool contains_pvar(pvar v) const { return m_vars.contains(v) || m_bail_vars.contains(v); } bool contains_pvar(pvar v) const { return m_vars.contains(v) || m_bail_vars.contains(v); }
bool pvar_occurs_in_constraints(pvar v) const { return v < m_var_occurrences.size() && m_var_occurrences[v] > 0; } bool pvar_occurs_in_constraints(pvar v) const { return v < m_var_occurrences.size() && m_var_occurrences[v] > 0; }
uint_set const& vars_occurring_in_constraints() const { return m_vars_occurring; }
#if 0 #if 0
clause* side_lemma(signed_constraint c) const { SASSERT(c); return side_lemma(c.blit()); } clause* side_lemma(signed_constraint c) const { SASSERT(c); return side_lemma(c.blit()); }