[m-rev.] diff: avoid runtime aborts from the decl debug oracle

[Zoltan Somogyi]

On 11-Oct-2002, Mark Brown <dougl at cs.mu.OZ.AU> wrote:
> 	1) The user is asked a missing answer question for p, for which the
> 	solutions are A, B and C.  The user asserts that this set is complete
> 	(but it may contain wrong answers).
> 
> 	2) The user goes on to diagnose a bug, then saves the oracle
> 	state, fixes the bug, and fires up another debugging session to
> 	diagnose some other symptom.
> 
> 	3) The user is again asked about that call to p, but this time the
> 	solutions are A, B and D.  The user asserts that this set is also
> 	complete.
> 
> 	4) At this point, the oracle deduces that {A, B} must be a complete
> 	set of solutions for that call to p, since it is the intersection
> 	of the two previous complete sets.

I figure that getting A, B and D at step 3 would a pretty rare event.
Most predicates don't have higher order outputs, and the ones that do
tend not to be modified in ways that return syntactically different
but semantically equivalent higher order terms.

Another solution would be to modify the process of updating the solution sets.
If the intersection reduces the cardinality of the set, we can check whether
the deleted elements include higher order components. If not, do everything
as before. If yes, then compute the differences between the sets being
intersected, which in this case yields {C} and {D}, and ask the user
whether they contain the same functions semantically. If yes, add their union
to the intersection. In this case, that means storing {A, B, C, D} as the
complete set of solutions.

Of course, we can even avoid asking the user, and always add the union of the
residues to the intersection. This may lead to more questions than if the set
was precise, but it may lead to fewer questions than a scheme that doesn't
keep the answer sets at all.

Zoltan.
--------------------------------------------------------------------------
mercury-reviews mailing list
post:  mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------