%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%% Set based groundness analysis tests %%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% This file contains a number of simple Prolog programs
% which are analyzed to check the groundness property
% using the set-based program analysis technique presented
% in the paper at
% http://www.math.unipr.it/~gianfr/PROJECT/COFIN99/DPR.draft.SC.ps.

% All CLP(SET) constraints have been generated "by hand"
% by applying the above cited technique
% to the relevant Prolog programs.

% In order to check satisfiability of the constraints listed below
% (hence, in order to perform the groundness analysis of the
% relevant programs) you must 
%   - consult the Prolog file 'analyzer.pl'
%   - issue the goal 'analyze(N)' where N is the number of the
%     program you want to analyze
%   - supply the analyzer with the name P of the predicate and the
%     number I of the argument you want to analyze
% The analyzer will answer you with either "Surely ground" or "Possibly
% not ground"  


%%%%%%%%%%%%%%%%%%%%%%%%% PROGRAM #1 %%%%%%%%%%%%%%%%%%%%%%%%%

% p(X) :- q(X).
% p(Y).
% p(Z).
% q(a).

program(1,p,1,Vp1) :- 
   Wp11=Vq1R  & Wp21={Y} & Wp31={Z} & Wq11={c} & delta(Vq1,Vq1R,N) &
   un(Wp11,Wp21,Vpaux) & un(Vpaux,Wp31,Vp1) & Vq1=Wq11.
program(1,q,1,Vq1) :- 
   Wp11=Vq1R  & Wp21={Y} & Wp31={Z} & Wq11={c} & delta(Vq1,Vq1R,N) &
   un(Wp11,Wp21,Vpaux) & un(Vpaux,Wp31,Vp1) & Vq1=Wq11.

% Answers:  p possibly not ground; q surely ground


%%%%%%%%%%%%%%%%%%%%%%%%% PROGRAM #2 %%%%%%%%%%%%%%%%%%%%%%%%%

% p(X) :- q(X).
% p(a).
% p(b).
% q(a).

program(2,p,1,Vp1) :- 
   Wp11=Vq1R  & Wp21={c} & Wp31={c} & Wq11={c} & delta(Vq1,Vq1R,N) &
   un(Wp11,Wp21,Vpaux) & un(Vpaux,Wp31,Vp1) & Vq1=Wq11.
program(2,q,1,Vq1) :- 
   Wp11=Vq1R  & Wp21={c} & Wp31={c} & Wq11={c} & delta(Vq1,Vq1R,N) &
   un(Wp11,Wp21,Vpaux) & un(Vpaux,Wp31,Vp1) & Vq1=Wq11.

% Answers:  p surely ground; q surely ground


%%%%%%%%%%%%%%%%%%%%%%%%% PROGRAM #3 %%%%%%%%%%%%%%%%%%%%%%%%%

% q(Z,a).
% p(X,Y) :- q(X,X).

program(3,p,1,Vp1) :- 
     Wq11={Z} & Wq12={c} & 
     int(Vq1R,Vq2R,Wp11) & delta(Vq1,Vq1R,N) & delta(Vq2,Vq2R,N) & delta(Wp11,Wp11R,N) &
     Wp12={Y} &
     Vq1=Wq11 & Vq2=Wq12 & Vp1=Wp11 & Vp2=Wp12.
program(3,p,2,Vp2) :- 
     Wq11={Z} & Wq12={c} & 
     int(Vq1R,Vq2R,Wp11) & delta(Vq1,Vq1R,N) & delta(Vq2,Vq2R,N) & delta(Wp11,Wp11R,N) &
     Wp12={Y} &
     Vq1=Wq11 & Vq2=Wq12 & Vp1=Wp11 & Vp2=Wp12.
program(3,q,1,Vq1) :- 
     Wq11={Z} & Wq12={c} & 
     int(Vq1R,Vq2R,Wp11) & delta(Vq1,Vq1R,N) & delta(Vq2,Vq2R,N) & delta(Wp11,Wp11R,N) &
     Wp12={Y} &
     Vq1=Wq11 & Vq2=Wq12 & Vp1=Wp11 & Vp2=Wp12.
program(3,q,2,Vq2) :- 
     Wq11={Z} & Wq12={c} & 
     int(Vq1R,Vq2R,Wp11) & delta(Vq1,Vq1R,N) & delta(Vq2,Vq2R,N) & delta(Wp11,Wp11R,N) &
     Wp12={Y} &
     Vq1=Wq11 & Vq2=Wq12 & Vp1=Wp11 & Vp2=Wp12.

% Answers:  p_1 (i.e., the first argument of p) and q_2 surely ground; 
%           p_2 and q_1 possibly not ground


%%%%%%%%%%%%%%%%%%%%%%%%% PROGRAM #4 %%%%%%%%%%%%%%%%%%%%%%%%%
%% See Example 6.1 in the paper at
%% http://www.math.unipr.it/~gianfr/PROJECT/COFIN99/DPR.draft.SC.ps

% r(a).
% r(f(H)).
% q(Z,a).
% p(X,Y) :- q(X,X), r(Y).

program(4,p,1,Vp1) :- 
     Wr11={c} & Wr21={H} &
     Wq11={Z} & Wq12={c} & 
     int(Vq1R,Vq2R,Wp11) & delta(Vq1,Vq1R,N) & delta(Vq2,Vq2R,N) & delta(Wp11,Wp11R,N) &
     Wp12=Vr1R & delta(Vr1,Vr1R,M) &
     un(Wr11,Wr21,Vr1) & Vq1=Wq11 & Vq2=Wq12 & Vp1=Wp11 & Vp2=Wp12.
program(4,p,2,Vp2) :- 
     Wr11={c} & Wr21={H} &
     Wq11={Z} & Wq12={c} & 
     int(Vq1R,Vq2R,Wp11) & delta(Vq1,Vq1R,N) & delta(Vq2,Vq2R,N) & delta(Wp11,Wp11R,N) &
     Wp12=Vr1R & delta(Vr1,Vr1R,M) &
     un(Wr11,Wr21,Vr1) & Vq1=Wq11 & Vq2=Wq12 & Vp1=Wp11 & Vp2=Wp12.
program(4,q,1,Vq1) :- 
     Wr11={c} & Wr21={H} &
     Wq11={Z} & Wq12={c} & 
     int(Vq1R,Vq2R,Wp11) & delta(Vq1,Vq1R,N) & delta(Vq2,Vq2R,N) & delta(Wp11,Wp11R,N) &
     Wp12=Vr1R & delta(Vr1,Vr1R,M) &
     un(Wr11,Wr21,Vr1) & Vq1=Wq11 & Vq2=Wq12 & Vp1=Wp11 & Vp2=Wp12.
program(4,q,2,Vq2) :- 
     Wr11={c} & Wr21={H} &
     Wq11={Z} & Wq12={c} & 
     int(Vq1R,Vq2R,Wp11) & delta(Vq1,Vq1R,N) & delta(Vq2,Vq2R,N) & delta(Wp11,Wp11R,N) &
     Wp12=Vr1R & delta(Vr1,Vr1R,M) &
     un(Wr11,Wr21,Vr1) & Vq1=Wq11 & Vq2=Wq12 & Vp1=Wp11 & Vp2=Wp12.
program(4,r,1,Vr1) :- 
     Wr11={c} & Wr21={H} &
     Wq11={Z} & Wq12={c} & 
     int(Vq1R,Vq2R,Wp11) & delta(Vq1,Vq1R,N) & delta(Vq2,Vq2R,N) & delta(Wp11,Wp11R,N) &
     Wp12=Vr1R & delta(Vr1,Vr1R,M) &
     un(Wr11,Wr21,Vr1) & Vq1=Wq11 & Vq2=Wq12 & Vp1=Wp11 & Vp2=Wp12.

% Answers:  p_1 and q_2 surely ground; 
%           p_2 and q_1 possibly not ground
%           r_1 possibly not ground


%%%%%%%%%%%%%%% PROGRAM #5 - with recursion %%%%%%%%%%%%%%%%
%% See Example 6.3 in the paper at
%% http://www.math.unipr.it/~gianfr/PROJECT/COFIN99/DPR.draft.SC.ps

% nat(0).
% nat(s(X)) :- nat(X).

program(5,nat,1,Vnat1) :- 
      Wnat11={c} & Wnat21=Vnat1R & delta(Vnat1,Vnat1R,N) &
      un(Wnat11,Wnat21,Vnat1).

% Answers:  nat surely ground


%%%%%%%%%%%%%%% PROGRAM #6 - with recursion %%%%%%%%%%%%%%%%

% nat(Y).
% nat(s(X)) :- nat(X).

program(6,nat,1,Vnat1) :- 
      Wnat11={Y} & Wnat21=Vnat1R & delta(Vnat1,Vnat1R,N) &
      un(Wnat11,Wnat21,Vnat1).

% Answers:  nat possibly not ground


%%%%%%%%%%%%% PROGRAM #7 - with recursion %%%%%%%%%%%%%

% p(a).
% p(X) :- q(X), p(X).
% q(Y).

program(7,p,1,Vp1) :- 
       Wp11={c} & int(Vq1R,Vp1R,Wp21) & 
       delta(Vq1,Vq1R,N) & delta(Vp1,Vp1R,N) & delta(Wp21,Wp21R,N) &
       Wq11={Y} &
       un(Wp11,Wp21,Vp1) & Vq1=Wq11.
program(7,q,1,Vq1) :- 
       Wp11={c} & int(Vq1R,Vp1R,Wp21) & 
       delta(Vq1,Vq1R,N) & delta(Vp1,Vp1R,N) & delta(Wp21,Wp21R,N) &
       Wq11={Y} &
       un(Wp11,Wp21,Vp1) & Vq1=Wq11.

% Answers:  p surely ground; q possibly not ground


%%%%%%%%%%%%%%%%% PROGRAM #8 - with aliasing %%%%%%%%%%%%%%%%

% q(a,b).
% q(U,U).
% p(X,Y) :- q(X,Y).

program(8,p,1,Vp1) :- 
       Wq11={c} & Wq12={c} &
       Wq21={U} & Wq22={U} &
       Wp11=Vq1R & delta(Vq1,Vq1R,N) &
       Wp12=Vq2R & delta(Vq2,Vq2R,N) &
       un(Wq11,Wq21,Vq1) & un(Wq12,Wq22,Vq2) & Vp1=Wp11 & Vp2=Wp12.
program(8,p,2,Vp2) :- 
       Wq11={c} & Wq12={c} &
       Wq21={U} & Wq22={U} &
       Wp11=Vq1R & delta(Vq1,Vq1R,N) &
       Wp12=Vq2R & delta(Vq2,Vq2R,N) &
       un(Wq11,Wq21,Vq1) & un(Wq12,Wq22,Vq2) & Vp1=Wp11 & Vp2=Wp12.
program(8,q,1,Vq1) :- 
       Wq11={c} & Wq12={c} &
       Wq21={U} & Wq22={U} &
       Wp11=Vq1R & delta(Vq1,Vq1R,N) &
       Wp12=Vq2R & delta(Vq2,Vq2R,N) &
       un(Wq11,Wq21,Vq1) & un(Wq12,Wq22,Vq2) & Vp1=Wp11 & Vp2=Wp12.
program(8,q,2,Vq2) :- 
       Wq11={c} & Wq12={c} &
       Wq21={U} & Wq22={U} &
       Wp11=Vq1R & delta(Vq1,Vq1R,N) &
       Wp12=Vq2R & delta(Vq2,Vq2R,N) &
       un(Wq11,Wq21,Vq1) & un(Wq12,Wq22,Vq2) & Vp1=Wp11 & Vp2=Wp12.

% Answers:  p_1 and p_2 possibly not ground;
%           q_1 and q_2 possibly not ground.

%%%%%%%%%%%%%%%%% PROGRAM #9 - with aliasing %%%%%%%%%%%%%%%%%

% r(a).
% q(U,U).
% p(X,Y) :- q(X,Y), r(X).

program(9,p,1,Vp1) :- 
       Wr11={c} & Wq11={U} & Wq12={U} &
       int(Vq1R,Vr1R,Wp11) & delta(Vq1,Vq1R,N) & delta(Vr1,Vr1R,N) & delta(Wp11,Wp11R,N) &
       Wp12=Vq2R & delta(Vq2,Vq2R,N) &
       Vr1=Wr11 & Vq1=Wq11 & Vq2=Wq12 & Vp1=Wp11 & Vp2=Wp12.
program(9,p,2,Vp2) :- 
       Wr11={c} & Wq11={U} & Wq12={U} &
       int(Vq1R,Vr1R,Wp11) & delta(Vq1,Vq1R,N) & delta(Vr1,Vr1R,N) & delta(Wp11,Wp11R,N) &
       Wp12=Vq2R & delta(Vq2,Vq2R,N) &
       Vr1=Wr11 & Vq1=Wq11 & Vq2=Wq12 & Vp1=Wp11 & Vp2=Wp12.
program(9,q,1,Vq1) :- 
       Wr11={c} & Wq11={U} & Wq12={U} &
       int(Vq1R,Vr1R,Wp11) & delta(Vq1,Vq1R,N) & delta(Vr1,Vr1R,N) & delta(Wp11,Wp11R,N) &
       Wp12=Vq2R & delta(Vq2,Vq2R,N) &
       Vr1=Wr11 & Vq1=Wq11 & Vq2=Wq12 & Vp1=Wp11 & Vp2=Wp12.
program(9,q,2,Vq2) :- 
       Wr11={c} & Wq11={U} & Wq12={U} &
       int(Vq1R,Vr1R,Wp11) & delta(Vq1,Vq1R,N) & delta(Vr1,Vr1R,N) & delta(Wp11,Wp11R,N) &
       Wp12=Vq2R & delta(Vq2,Vq2R,N) &
       Vr1=Wr11 & Vq1=Wq11 & Vq2=Wq12 & Vp1=Wp11 & Vp2=Wp12.

% Answers:  p_1 and p_2 surely ground;
%           q_1 and q_2 possibly not ground
%
% Specifically, Vq1={U} and Vq2={U}.
% Observe that the presence of program variables in the generated
% CLP(SET) constraint allows one to easily account for dependencies 
% among variables. Thus, for instance, in the program above, the 
% fact that both Vq1 and Vq2 are equal to {U}, with the same 
% variable U in both equations, means that whenever
% Vq1 becomes ground then so does Vq2, and vice versa.