Incr engine: refine reexecution position for reactivated occurrences
In short, this change restricts information algo needs from journal. It restricts how far invalidation stage goes into journal. Previously it fed ExecQueue with position arbitrarily far in 'past', whereas now it feeds the closest valid position (the 'present').
This commit is contained in:
parent
76b37c3f3e
commit
3bdc1123ad
|
|
@ -81,7 +81,7 @@ internal class ConstraintsProcessing(private var dispatchingFront: Dispatcher.Di
|
|||
val justificationRoots = mutableListOf<Justified>()
|
||||
|
||||
val it = this.iterator()
|
||||
var prevChunk = it.next() // skip initial chunk
|
||||
var lastValidChunk = it.next() // skip initial chunk
|
||||
|
||||
while (it.hasNext()) {
|
||||
val chunk = it.next()
|
||||
|
|
@ -118,11 +118,11 @@ internal class ConstraintsProcessing(private var dispatchingFront: Dispatcher.Di
|
|||
// all occurrences from the head are principal.
|
||||
assert(chunk.match.allHeads().all { it.isPrincipal })
|
||||
|
||||
execQueue.offerAll(prevChunk.toPos(), validOccs.asIterable())
|
||||
execQueue.offerAll(lastValidChunk.toPos(), validOccs.asIterable())
|
||||
}
|
||||
} else {
|
||||
lastValidChunk = chunk
|
||||
}
|
||||
|
||||
prevChunk = chunk
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -128,9 +128,7 @@ internal class ExecutionQueue(
|
|||
fun offerAll(continueFromPos: MatchJournal.Pos, occs: Iterable<Occurrence>) =
|
||||
occs.forEach {
|
||||
journalIndex.activatingChunkOf(it)?.let { occChunk ->
|
||||
// todo: ensure which is better
|
||||
// offer(continueFromPos, occChunk)
|
||||
offer(occChunk.toPos(), occChunk)
|
||||
offer(continueFromPos, occChunk)
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue