There was a problem in determining when an incrementally recomputed
subgoal was actually changed: specifically when recomputation does not
find as many answers as it did previously. The code handles this case
by keeping a counter field in the previous callnodepointer, called
no_of_answers. When a call is being computed, no_of_answers is
incremented for each new answer. When recomputed no_of_answers for
the *previous* call is decremented. In this case, if no_of_answers
for the previous call is greater than 0, we know that the recomputed
subgoal has fewer answers than previously. Otherwise if no_of_answers
== 0, and some other conditions hold we know that the recomputed
subgoal is unchanged, so that we can propagate_no_change, decrementing
the falsecounts of other subgoals in the IDG.
The problem was that for rederived answers (as opposed to new answers)
the no_of_answers was not being incremented. This meant that in
certain cases, propagate_no_change was being incorrectly called,
preventing some subgoals from being recomputed. So it was a simple 1
line fix.
Its a little surprising that we didn't notice this bug before. The
following example illustrates the conditions. 1) a single answer A is
added to an incr subgoal S. 2) S is recomputed, and A is rederived
(with no other answers): here no_of_answers stays 0 for S:2. 3) S is
recomputed again, but now A is not rederived. Since no_of_answers for
S:2 is 0, and since we only ever computed A for any version of S, S:3
is seen as unchanged and propagate_no_change is called. If
furthermore there is a goal S' affected by S:3 and only by S:3, its
falsecount becomes 0, and S' is never recomputed. Of course the
conditions are somewhat more general, but a similar sequence of
actions and constraints would need to transpire. So maybe its not too
terribly surprising.
