mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 08:28:44 +00:00
Code Activity

minor issue about narrow with first=true

Browse source
This commit is contained in:
Jakob Rath 2022-12-08 15:30:55 +01:00
parent 85818612fb
commit 3fe8f4a0cd
1 changed files with 4 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1052,6 +1052,10 @@ namespace polysat {
} }
if (v != null_var) if (v != null_var)
m_viable_fallback.push_constraint(v, c); m_viable_fallback.push_constraint(v, c);
// TODO: we use narrow with first=true to add axioms about the constraint to the solver.
// However, constraints can be activated multiple times (e.g., if it comes from a lemma and is propagated at a non-base level).
// So the same axioms may be added multiple times.
// Maybe separate narrow/activate? And keep a flag in m_bvars to remember whether constraint has already been activated.
c.narrow(*this, true); c.narrow(*this, true);
#if ENABLE_LINEAR_SOLVER #if ENABLE_LINEAR_SOLVER
m_linear_solver.activate_constraint(c); m_linear_solver.activate_constraint(c);