mthom / scryer-prolog

A modern Prolog implementation written mostly in Rust.
BSD 3-Clause "New" or "Revised" License
2.05k stars 120 forks source link

Unexpected multiple solutions of setof/3 #2499

Open hurufu opened 2 months ago

hurufu commented 2 months ago

This query unexpectedly produces multiple answers:

?- setof(X, phrase((...,seq(X)),"abc"), Xs).
   Xs = [[]]
;  Xs = ["abc"]
;  Xs = ["bc"]
;  Xs = ["c"].

But the next succeeds deterministically and behaves as expected:

?- setof(X, phrase(...,"abc",X), Xs).
   Xs = [[],"abc","bc","c"].

I'm struggling to find a minimal example.

UWN commented 2 months ago
?- phrase(("","";""),X).
   X = []
;  X = [].
?- setof(X,phrase(("","";""),X),Xs).
   Xs = [[]]
;  Xs = [[]], unexpected.
?- setof(X,phrase(("";""),X),Xs).
   Xs = [[]].

So this clearly is an artefact of inconsistent use of goal expansion. setof/3 detects variables in its goals that should be used for enumeration. Actually, there are none. But when applying goal expansions there are some internal variables.

UWN commented 2 months ago

Currently, there is a cheap hack to circumvent goal expansion:


?- setof(X,t^phrase(("","";""),X),Xs).
   Xs = [[]].