mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 00:26:38 +00:00
Code Activity

fix some bugs

Browse source
This commit is contained in:
Jakob Rath 2022-03-18 16:05:51 +01:00
parent fd353bff17
commit d41d3fa6ea
2 changed files with 12 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -270,7 +270,7 @@ namespace polysat {
auto& wlist = m_pwatch[v];
unsigned i = 0, j = 0, sz = wlist.size();
for (; i < sz && !is_conflict(); ++i)
if (propagate(v, wlist[i]))
if (!propagate(v, wlist[i]))
wlist[j++] = wlist[i];
for (; i < sz; ++i)
wlist[j++] = wlist[i];
@ -280,6 +280,7 @@ namespace polysat {
bool solver::propagate(pvar v, signed_constraint c) {
LOG_H3("Propagate " << m_vars[v] << " in " << c);
SASSERT(is_assigned(v));
SASSERT(!c->vars().empty());
unsigned idx = 0;
if (c->var(idx) != v)
@ -297,9 +298,11 @@ namespace polysat {
}
}
// at most one variable remains unassigned.
unsigned other_v = c->var(idx);
if (!is_assigned(other_v))
m_viable_fallback.push_constraint(other_v, c);
if (c->vars().size() >= 2) {
unsigned other_v = c->var(1 - idx);
if (!is_assigned(other_v))
m_viable_fallback.push_constraint(other_v, c);
}
c.narrow(*this, false);
return false;
}
@ -505,8 +508,10 @@ namespace polysat {
// TODO: we should add a better way to test constraints under assignments, without modifying the solver state.
m_value[v] = val;
m_search.push_assignment(v, val);
m_justification[v] = j;
bool is_valid = m_viable_fallback.check_constraints(v);
m_search.pop();
m_justification[v] = justification::unassigned();
if (!is_valid) {
// Try to find a valid replacement value
switch (m_viable_fallback.find_viable(v, val)) {

4
src/math/polysat/viable.cpp
View file

@ -738,15 +738,17 @@ namespace polysat {
void viable_fallback::push_var(unsigned sz) {
auto& mk_solver = *m_usolver_factory;
m_usolver.push_back(mk_solver(sz));
m_constraints.push_back({});
}
void viable_fallback::pop_var() {
m_usolver.pop_back();
m_constraints.pop_back();
}
void viable_fallback::push_constraint(pvar v, signed_constraint const& c) {
// v is the only unassigned variable in c.
SASSERT(!s.is_assigned(v));
SASSERT(c->vars().size() == 1 || !s.is_assigned(v));
DEBUG_CODE(for (pvar w : c->vars()) { if (v != w) SASSERT(s.is_assigned(w)); });
auto& us = *m_usolver[v];
// TODO: would be enough to push the solver only for new decision levels