mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

fix assertion

Browse source
This commit is contained in:
Jakob Rath 2022-09-23 16:15:38 +02:00
parent 0a0953ae78
commit 3c60c418e7
2 changed files with 9 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -598,6 +598,7 @@ namespace polysat {
++m_stats.m_num_propagations;
LOG(assignment_pp(*this, v, val) << " by " << j);
SASSERT(m_viable.is_viable(v, val));
SASSERT(j.is_decision() || j.is_propagation());
SASSERT(j.level() == m_level);
SASSERT(!is_assigned(v));
SASSERT(std::all_of(assignment().begin(), assignment().end(), [v](auto p) { return p.first != v; }));
@ -605,9 +606,12 @@ namespace polysat {
m_search.push_assignment(v, val);
m_trail.push_back(trail_instr_t::assign_i);
m_justification[v] = j;
SASSERT(m_viable_fallback.check_constraints(v));
// Decision should satisfy all univariate constraints.
// Propagation might violate some other constraint; but we will notice that in the propagation loop when v is propagated.
// TODO: on the other hand, checking constraints here would have us discover some conflicts earlier.
SASSERT(!j.is_decision() || m_viable_fallback.check_constraints(v));
#if ENABLE_LINEAR_SOLVER
// TODO: convert justification into a format that can be tracked in a depdendency core.
// TODO: convert justification into a format that can be tracked in a dependency core.
m_linear_solver.set_value(v, val, UINT_MAX);
#endif
}

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

@ -790,8 +790,10 @@ namespace polysat {
for (auto const& c : m_constraints[v]) {
// for this check, all variables need to be assigned
DEBUG_CODE(for (pvar w : c->vars()) { SASSERT(s.is_assigned(w)); });
if (c.is_currently_false(s))
if (c.is_currently_false(s)) {
LOG(assignment_pp(s, v, s.get_value(v)) << " violates constraint " << lit_pp(s, c));
return false;
}
SASSERT(c.is_currently_true(s));
}
return true;