mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity

Add note on potential replay problem

Browse source
This commit is contained in:
Jakob Rath 2022-11-23 15:00:31 +01:00
parent 0313f91dc2
commit f51d5c2fe9
1 changed files with 9 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -496,6 +496,15 @@ namespace polysat {
// when substituting polynomials, it will now take into account the replayed variables, which may itself depend on previous propagations.
// will we get into trouble with cyclic dependencies?
// But we do want to take into account variables that are assigned but not yet propagated.
// Possible solutions:
// - keep the replay queue outside of this method?
// prioritize putting stuff on the stack from the replay queue.
// this might however introduce new propagations in between? maybe that is ok?
// - when evaluating/narrowing instead of passing the full assignment,
// we pass a "dependency level" which is basically an index into the search stack.
// then we get an assignment up to that dependency level.
// each literal can only depend on entries with lower dependency level
// (that is the invariant that propagations are justified by a prefix of the search stack.)
}
else
static_assert(always_false<T>::value, "non-exhaustive visitor");