% simple confluence checker Thom Fruehwirth 2004-07-02ff 07-23 confl5.pl

% Built-ins (and guards) must be simulated by proper CHR constraints
% CHR rules must be represented as usual AND as Prolog facts named rule/3
%   where propagation and simpagation rules are written as simplification
% Spurious non-joinable states are possible since not all derivations are tried
%   and since propagation rules may be applied twice instead of once

:- use_module(library(terms)).  % term_variables/2, variant/2

:- use_module(library(chr)).

handler union_find_confl5.


% The confluence checker =====================================================

% call confluence checker as follows:
% ?- confl(R1,R2,ST,ST1-ST2,SZ1,SZ2,SZZ).  

% Handling built-ins as CHR constraints

constraints bi/1.  % built-in as CHR

bi(A) \ bi(A) <=> true.
bi(X=Y) <=> X=Y.
bi(X>=X) <=> true.
bi(X>=Y), bi(Y>=X) <=> X=Y.

%-----------------------------------------------------------------------------
% ?- confl(RuleNameHead1,RuleNameHead2,CriticalAncestorState,CriticalPair,FinalState1,FinalState2, FinalStateDifference).
% ?- confl(R1,R2,ST,ST1-ST2,SZ1,SZ2,SZZ).  % Names to get nice output in Sicstus

confl((R1,H1), (R2,H2), (H1R,OL,H2R), (B1,H2R) - (H1R,B2), S1-VV1, S2-VV2, S11-S22) :-
   rule(R1,H1,B1),
   rule(R2,H2,B2),
     R1 @=< R2,   % avoid symmetries
     OL=[_|_],    % avoid trivial cases
   overlap(H1,H2,H1R,OL,H2R), 
     \+ (B1==B2, H1R==H2R),    % avoid trivial cases
   once((
   term_variables((H1R,OL,H2R),Vs),
   findall(Vs-FS22,
     (
     (calll(B1,H2R) ; calll(H1R,B2)),
      findall_constraints(_,FS1),
      sort(FS1,FS2),
      strip(FS2,FS22)
     ),
     FS3
   ),
   (FS3=[Vs1-S1,Vs2-S2] ; FS3=[Vs1-S1],Vs2=Vs1,S2=[]),
   numbervars(Vs,0,_),
   namevars(Vs1,Vs,[],VV1),
   namevars(Vs2,Vs,[],VV2),
   append(S1,VV1,S1V),
   append(S2,VV2,S2V),
   maxoverlap(S1V,S2V,S11,SO,S22)
   )),
   \+ (S11==[],S22==[]),
   \+ (variant(Vs1-VV1-S1,Vs2-VV2-S2)), %S1\==S2,
   nl.  % only for more readable output
 

 strip([],[]).
 strip([bi(C)#Id|L1],[C|L2]):- 
    !,
    remove_constraint(Id), % needed since findall leaves CHR constraints around
    strip(L1,L2).
 strip([C#Id|L1],[C|L2]):- 
    remove_constraint(Id), % needed since findall leaves CHR constraints around
    strip(L1,L2).

 calll([],[]).
 calll([],G):- G=[_|_], calll(G,[]).
 calll([G|L],G2):- G, calll(L,G2). 

 overlap(H1,H2, H1,[],H2).
 overlap([X|H1],XH2,H1R,[X|OL],H2R):-
    delete(X,XH2,H2),
    overlap(H1,H2,H1R,OL,H2R).
 overlap([X|H1],H2,[X|H1R],OL,H2R):-
    OL=[_|_],
    overlap(H1,H2,H1R,OL,H2R).

 delete( X, [X|L],  L).
 delete( Y, [X|Xs], [X|Xt]) :-
    delete( Y, Xs, Xt).

 append([],L,L).
 append([X|L1],L2,[X|L3]):- append(L1,L2,L3).

 maxoverlap([],H2, [],[],H2).
 maxoverlap([X|H1],XH2,H1R,[X|OL],H2R):-
    delete(X1,XH2,H2),X==X1,
    !,
    maxoverlap(H1,H2,H1R,OL,H2R).
 maxoverlap([X|H1],H2,[X|H1R],OL,H2R):-
    maxoverlap(H1,H2,H1R,OL,H2R).

 % namevars(ActualVars,ParameterVars,UsedParameterVars, Equations)
 namevars([],[],_,[]).
 namevars([X|L1],[Y|L2],L3, VV1):- 
    ((nonvar(X) ; delete(Z,L3,_),X==Z) -> VV1=[X=Y|VV2] ; X=Y,VV1=VV2),
    namevars(L1,L2,[X|L3], VV2).



% Union-Find Examples =================================================

constraints '~>'/2, union/2, find/2, link/2, make/1, root/1, root/2.
operator(700, xfx, '~>').

/*
% rules added in paper for ufd_basic to avoid critical pairs
% should be applied before standard rules for ufd_rank

% possible preamble to eliminate unwanted non-joinable critical pairs
A ~> A <=> fail.
A ~> _, A ~> _ <=> fail.
root(A), A ~> _ <=> fail.
root(A), root(A) <=> fail.
root(A,_), A ~> _ <=> fail.
root(A,_), root(A,_) <=> fail.

% another preamble to eliminate unwanted non-joinable critical pairs
A ~> B \ A ~> C <=> B=C.
root(A) \ A ~> B <=> A=B.
root(A) \ root(A) <=> true.
root(A,_) \ A ~> B <=> A=B.
root(A,N) \ root(A,M) <=> N=M.

A ~> C \ link(A,B) <=> link(C,B).
A ~> C \ link(B,A) <=> link(B,C).

% to check confluence with these rules

rule(point, [A ~> B, A ~> C] , [A ~> B, B=C]).
rule(root1, [root(A,N), A ~> B] , [root(A,N), A=B]).
rule(root2, [root(A,N), root(A,M)] , [root(A,N), N=M]).

rule(link1, [A ~> C, link(A,B)] , [A ~> C, link(C,B)]).
rule(link2, [A ~> C, link(B,A)] , [A ~> C, link(B,C)]).
*/



% ufd_rank

make      @ make(A) <=> root(A,0).

union     @ union(A,B) <=> find(A,X), find(B,Y), link(X,Y).

findNode  @ find(A,X), A ~> B <=> find(B,X), A ~> X.  
findRoot  @ root(A,_) \ find(A,X) <=> X=A.      

linkEq    @ link(A,A) <=> true.  
linkLeft  @ link(A,B), root(A,N), root(B,M) <=> N>=M | 
               B ~> A, N1 is max(N,M+1), root(A,N1).
linkRight @ link(B,A), root(A,N), root(B,M) <=> N>=M |
               B ~> A, N1 is max(N,M+1), root(A,N1).

% only for confluence checker
linkLeftbi  @ bi(N>=M) \ link(A,B), root(A,N), root(B,M) <=>
               B ~> A, bi(N1 is max(N,M+1)), root(A,N1).
linkRightbi @ bi(N>=M) \ link(B,A), root(A,N), root(B,M) <=>
               B ~> A, bi(N1 is max(N,M+1)), root(A,N1).


% rule representation for confluence checker
%:- op(700, xfx, '~>').

rule(make      ,[ make(A)] ,[root(A,0)]).
rule(union     ,[ union(A,B)] ,[find(A,X), find(B,Y), link(X,Y)]).

rule(findNode  ,[ A ~> B, find(A,X)] ,[find(B,X), A ~> X]).
rule(findRoot  ,[ root(A,N), find(A,X)] ,[root(A,N), bi(X=A)]).      

rule(linkEq    ,[ link(A,A)] ,[true]).  
rule(linkLeft  ,[ link(A,B), root(A,N), root(B,M), bi(N>=M)] , 
                  [B ~> A, bi(N1 is max(N,M+1)), root(A,N1), bi(N>=M)]).
rule(linkRight ,[ link(B,A), root(A,N), root(B,M), bi(N>=M)] , 
                  [B ~> A, bi(N1 is max(N,M+1)), root(A,N1), bi(N>=M)]).


/*
% version ufd_basic

make      @ make(A) <=> root(A).
union     @ union(A,B) <=> find(A,X), find(B,Y), link(X,Y).

findNode  @ A ~> B \  find(A,X) <=> find(B,X).
findRoot  @ root(A) \ find(A,X) <=> X=A.      

linkEq    @ link(A,A) <=> true.  
link      @ link(A,B), root(A), root(B) <=> B ~> A, root(A).

%:- op(700, xfx, '~>').

rule([A ~> B, A ~> C] , [A ~> B, A=C]).
rule([root(A), A ~> B] , [root(A), A=B]).
rule([root(A), root(A)] , [root(A)]).

rule([A ~> C, link(A,B)] , [A ~> C, link(C,B)]).
rule([A ~> C, link(B,A)] , [A ~> C, link(B,C)]).


rule(make      ,[ make(A)] ,[root(A)]).
rule(union     ,[ union(A,B)] ,[find(A,X), find(B,Y), link(X,Y)]).

rule(findNode  ,[ A ~> B,  find(A,X)] ,[A ~> B, find(B,X)]).
rule(findRoot  ,[ root(A), find(A,X)] ,[root(A), bi(X=A)]).      

rule(linkEq    ,[ link(A,A)] ,[true]).  
rule(link      ,[ link(A,B), root(A), root(B)] ,[B ~> A, root(A)]).
*/


% ufd-keepfind version deleted


%-------------------- eof ------------------------------------------------