swish
swish copied to clipboard
SWISH residual goals differ significantly from normal toplevel
With the latest git version of SWI, I get the following residual goal on the normal toplevel, with library(clpb) loaded:
?- sat(X+Y). sat(X=\=X*Y#Y).
In contrast, when I run the same query in SWISH, I get:
?- sat(X+Y). sat(Y=\=Y*X#X)
These residual goals are semantically equivalent, which we can see using taut/2:
?- taut((X=\=X*Y#Y) =:= (Y=\=Y*X#X), T). T = 1, sat(X=:=X), sat(Y=:=Y).
Still, this discrepancy is extremely unfortunate, because when the bdd renderer is enabled, then it shows the variables in an order that does not correspond to the actual order that is used for this BDD! In this concrete case, X appears first in the query sat(X+Y), so X should be the root node in the BDD. However, the bdd renderer uses the residual goals to show the BDD, and therefore shows Y as the root node instead, leading to a completely different impression.
As far as I can tell, one commit that is involved in this is: https://github.com/SWI-Prolog/swipl-devel/commit/2bcbced12762fae72420889096120b54aaadc63c
The only thing it does is adding module qualification to sat/1 residual goals, i.e., it simply prepends clpb:... to the arising CLP(B) residuals, which generally should not cause such a severe difference in the residual goals of SWISH and the normal toplevel.