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

remove remove_var

Browse source
This commit is contained in:
Jakob Rath 2021-09-14 14:42:24 +02:00
parent 8103627e47
commit 66a41383e8
3 changed files with 3 additions and 27 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -141,26 +141,6 @@ namespace polysat {
insert(c_new, c_new_premises);
}
void conflict_core::remove_var(pvar v) {
LOG("Removing v" << v << " from core");
unsigned j = 0;
for (unsigned i = 0; i < m_constraints.size(); ++i)
if (m_constraints[i]->contains_var(v))
unset_mark(m_constraints[i]);
else
m_constraints[j++] = m_constraints[i];
m_constraints.shrink(j);
indexed_uint_set literals_copy = m_literals; // TODO: can avoid copy (e.g., add a filter method for indexed_uint_set)
for (unsigned lit_idx : literals_copy) {
signed_constraint c = cm().lookup(sat::to_literal(lit_idx));
if (c->contains_var(v)) {
unset_mark(c);
m_literals.remove(lit_idx);
}
}
m_vars.remove(v);
}
void conflict_core::set_bailout() {
SASSERT(!is_bailout());
m_bailout = true;

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

@ -89,9 +89,6 @@ namespace polysat {
void remove(signed_constraint c);
void replace(signed_constraint c_old, signed_constraint c_new, vector<signed_constraint> c_new_premises);
/** remove all constraints that contain the variable v */
void remove_var(pvar v);
void keep(signed_constraint c);
/** Perform boolean resolution with the clause upon variable 'var'.

7
src/math/polysat/explain.cpp
View file

@ -80,10 +80,9 @@ namespace polysat {
continue;
if (!c->contains_var(v)) {
core.keep(c);
// NOTE: more variables than 'v' might have been removed here (see polysat::test_p3), so remove_var(v) isn't enough.
// also, c alone (+ variables) is now enough to represent the conflict.
// core.remove_var(v);
core.keep(c); // adds propagation of c to the search stack
// NOTE: more variables than just 'v' might have been removed here (see polysat::test_p3).
// c alone (+ variables) is now enough to represent the conflict.
core.reset();
core.set(c);
return l_true;