%
/*
 Copyright (C) 1991, Shinji Kono, Sony Computer Science Laboratory, Inc.
                                  The University, Newcastle upton Tyne

 Everyone is permitted to copy and distribute verbatim copies
 of this license, but changing it is not allowed.  You can also
 use this wording to make the terms for other programs.

 send your comments to kono@csl.sony.co.jp
 $Id: rstd.pl,v 1.4 2007/08/30 05:16:36 kono Exp $
*/
% ITL subterm standarization with BDT
%
% Fri Jun 21 10:32:58 BST 1991
%
% :- dynamic renaming/0,count_limit/1.

:- dynamic sb/2,sbn/1.

subterm_init :- 
	r_abolish(sb,2),
	asserta((sb([],-1))),
	r_abolish(sbn,1),
	asserta(sbn(0)).

std_check([],I,?(I1,true,false)) :-!,   % no regular variable
	std_check(I,I1) .
std_check(_,I,?(I,true,false)) :-!. % can be changed in path 2

std_check(I,I) :- atomic(I),!.
std_check(I,J) :-
	sb(I,J),!.
std_check(I,N1) :-
	retract(sbn(N)),N1 is N+1,asserta(sbn(N1)),
	assertz(sb(I,N1)),!.

itlstd(P,StdP,Rename) :- 
	sbdt(P,P1,([],[],[]),(_,Vars,Dup)),     % path 1
	itlstd1(Vars,Dup,P1,StdP,Rename).
itlstd1([],[],P,P,[]) :-!.     % no regular variable path 1 is enough 
itlstd1(Vars,Dup,P,P1,Rename) :-
	rename_list(Vars,Dup,Rename),
	sbdt2(P,P1,Rename).                     % path 2

% for detailed trace
%        itlstd(PNext,StdNext,NextFull,Rename,Rename1)

itlstd(P,StdP,FullP1,_,Rename) :- 
	sbdt(P,FullP,([],[],[]),(_,Vars,Dup)),  % path 1
	itlstd2(Vars,Dup,FullP,FullP1,StdP,Rename).
itlstd2([],[],P,P,P,[]) :-!.     % no regular variable path 1 is enough 
itlstd2(Vars,Dup,FullP,FullP1,StdP,Rename) :-
	rename_list(Vars,Dup,Rename),
	sbdt2(FullP,StdP,Rename),               % path 2
	detailed_rename(Rename,Rename1),
	write((Rename,Rename1)),nl,
	sbdt2(FullP,FullP1,Rename1).            % over limit replacement only

% preserve singleton variable
% fix limit overed non-singleton variable
detailed_rename([],[]) :-!.
detailed_rename([(_,true_false)|R],R1) :-!,     % singleton
	detailed_rename(R,R1).
detailed_rename([(_,^(_,_))|R],R1) :-!,         % renaming
	detailed_rename(R,R1).
detailed_rename([H|R],[H|R1]) :-!,              % true/false replacement
	detailed_rename(R,R1).

rename_list(L,D,R):- singleton,!,
	rename_singleton(L,D,L0,R,R1),
	sortC(L0,L1),
	number_list(L1,L2),
	compact_list(L2,R1).
rename_list(L,_,L3):- renaming,!,
	sortC(L,L1),
	number_list(L1,L2),
	compact_list(L2,L3).
rename_list(_,_,[]).

%  rename_singleton(Vars,Duplicate,Deleted,Replace,Replace1)
rename_singleton([],_,[],R,R):-!.
rename_singleton([V|L],Dup,[V|L1],R,R1):-
	member(V,Dup),!,
	rename_singleton(L,Dup,L1,R,R1).
rename_singleton([V|L],Dup,L1,[(V,true_false)|R],R1):-
	rename_singleton(L,Dup,L1,R,R1).

uniq([],[]):-!.
uniq([H|L],[H|L1]) :-
	uniq(L,H,L1).
uniq([],_,[]) :-!.
uniq([H|L],H,L1) :-!,
	uniq(L,H,L1).
uniq([H|L],_,[H|L1]) :-
	uniq(L,H,L1).

number_list([],[]) :-!.
number_list([^(R,S)|L],[(^(R,S),^(R,1))|L1]) :-
	length_limit(LM),
	number_list(L,R,2,L1,LM).

number_list([],_,_,[],_) :-!.
number_list([^(R,S)|L],R,N,[(^(R,S),^(R,N))|L1],LM) :-  % same variable
	N =< LM,!, 
	N1 is N+1,
	number_list(L,R,N1,L1,LM).
number_list([^(R,S)|L],R,N,[(^(R,S),F)|L1],LM) :-       % same variable
	inc_var(over,_),
	!,(F=true;F=false),                             % over the limit
	number_list(L,R,N,L1,LM).
number_list([^(R,S)|L],_,_,[(^(R,S),^(R,1))|L1],LM) :-  % new variable
	number_list(L,R,2,L1,LM).

compact_list([],[]) :-!.
compact_list([(^(R,N),^(R,N))|L1],L2) :-!,            % remove identity
	compact_list(L1,L2).
compact_list([H|L1],[H|L2]) :-
	compact_list(L1,L2).

% do substitution member first ( to avoid infinite loop by identity
% substitution

sbdt_s([],[]):-!.
sbdt_s([(A,B)|L],[(A,B1)|L1]):-!,
	sbdt(B,B1,([],[],[]),_),
	sbdt_s(L,L1).

% BDT classification of subterm

% sbdt(Input,BDD,(UseInTerm,Variable,Duplicate),( ... ))  path 1
sbdt(true,true,L,L):-!.
sbdt(false,false,L,L):-!.
sbdt(true_false,true_false,L,L):-!.
sbdt(P,F,L,L) :- atomic(P),!,F= ?(P,true,false).
sbdt(?(C,T,F),?(C,T,F),L,L) :- !.  % already done.
sbdt(not(P),F,L,L1) :- !,sbdt(P,F0,L,L0),sbdt_not(F0,F,L0,L1),!.
sbdt((P,Q),F,L,L2) :- !,
	sbdt(P,P0,L,L0),sbdt(Q,Q0,L0,L1),
	sbdt_and(P0,Q0,F,L1,L2),!.
sbdt((P;Q),F,L,L2) :- !,
	sbdt(P,P0,L,L0),sbdt(Q,Q0,L0,L1),
	sbdt_or(P0,Q0,F,L1,L2),!.
sbdt((P&Q), N,(U,V,D),(U,V2,D2)) :-!,
	sbdt(P,P1,([],V,D),(U1,V1,D1)),
	sbdt(Q,Q1,([],V1,D1),(U2,V2,D2)), 
	or_list(U1,U2,U3),
	% projection and closure touch later part of chop
	std_check(U3,(P1&Q1),N).
% bottom up development is effective for quantifier
sbdt(exists(P,Q), N,(U,R,D),(U,R1,D1)) :-!,
	sbdt(Q,QF,([],R,D),(U1,R1,D1)),
	std_check(U1,exists(P,QF),N).
sbdt(proj(P,Q), N,(U,V,D),(U,V2,D2)) :-!,
	sbdt(P,P1,([],V,D),(U1,V1,D1)),
	sbdt(Q,Q1,([],V1,D1),(U2,V2,D2)), 
	or_list(U1,U2,U3),
	std_check(U3,proj(P1,Q1),N).
sbdt(prefix(Q), N,(U,R,D),(U,R1,D1)) :-!,
	sbdt(Q,QF,([],R,D),(U1,R1,D1)),
	std_check(U1,prefix(QF),N).
sbdt(^(R), ?(^(R),true,false),L,L) :-!.
sbdt(Rg, ?(Rg,true,false),(U,V,D),(U1,V1,D1)) :- Rg = ^(_,_),!,
	sbdt_r(Rg,U,V,D,U1,V1,D1).
% Simple Functor
sbdt(Func,N,(U,V,D),(U,V1,D1)) :- functor(Func,H,1),!,
	arg(1,Func,A),
	sbdt(A,A1,([],V,D),(U1,V1,D1)),
	functor(Func1,H,1),arg(1,Func1,A1),
	std_check(U1,Func1,N).
sbdt(Func,N,(U,V,D),(U,V2,D2)) :- functor(Func,H,2),!,
	arg(1,Func,A),sbdt(A,A1,([],V,D),(U1,V1,D1)),
	arg(2,Func,B),sbdt(B,B1,([],V1,D1),(U2,V2,D2)),
	functor(Func1,H,2),arg(1,Func1,A1),arg(2,Func1,B1),
	or_list(U1,U2,U3),std_check(U3,Func1,N).
sbdt(Def,true,L,L) :-
    write('bdtstd error: '),write(Def),nl.

sbdt_not(true,false,L,L).
sbdt_not(false,true,L,L).
sbdt_not(true_false,true_false,L,L).
sbdt_not(F,?(H,A1,B1),L,L1):-
    arg(1,F,H),arg(2,F,A),arg(3,F,B),
    sbdt_not(A,A1,L,L0),sbdt_not(B,B1,L0,L1).
sbdt_and(false,_,false,L,L):-!.
sbdt_and(_,false,false,L,L):-!.
sbdt_and(true,T,T,L,L):-!.
sbdt_and(T,true,T,L,L):-!.
sbdt_and(T,T1,T1,L,L):- atomic(T),T=T1,!.
sbdt_and(?(PF,P0,P1),true_false,F,L,L1):-!,
    sbdt_and(P0,true_false,R0,L,L0),
    sbdt_and(P1,true_false,R1,L0,L1),
    sbdt_opt(PF,R0,R1,F).
sbdt_and(true_false,?(PF,P0,P1),F,L,L1):-!,
    sbdt_and(P0,true_false,R0,L,L0),
    sbdt_and(P1,true_false,R1,L0,L1),
    sbdt_opt(PF,R0,R1,F).
sbdt_and(P,Q,R,L,L1) :-!,
    arg(1,P,PF),arg(1,Q,QF),
    sbdt_and(PF,QF,P,Q,R,L,L1).
sbdt_and(PF,QF,P,Q,R,L,L1):-PF @< QF,!,
    sbdt_and(QF,PF,Q,P,R,L,L1).
sbdt_and(PF,QF,P,Q,F,L,L1):-PF @> QF,!,
    arg(2,Q,Q0),arg(3,Q,Q1),
    sbdt_and(Q0,P,R0,L,L0),
    sbdt_and(Q1,P,R1,L0,L1),
    sbdt_opt(QF,R0,R1,F).
sbdt_and(PF,PF,P,Q,F,L,L1):-
    arg(2,P,P0),arg(3,P,P1),
    arg(2,Q,Q0),arg(3,Q,Q1),
    sbdt_and(P0,Q0,R0,L,L0),
    sbdt_and(P1,Q1,R1,L0,L1),
    sbdt_opt(PF,R0,R1,F).
sbdt_or(true,_,true,L,L):-!.
sbdt_or(_,true,true,L,L):-!.
sbdt_or(false,T,T,L,L):-!.
sbdt_or(T,false,T,L,L):-!.
sbdt_or(T,T1,T1,L,L):- atomic(T),T=T1,!.
sbdt_or(?(PF,P0,P1),true_false,F,L,L1):-!,
    sbdt_or(P0,true_false,R0,L,L0),
    sbdt_or(P1,true_false,R1,L0,L1),
    sbdt_opt(PF,R0,R1,F).
sbdt_or(true_false,?(PF,P0,P1),F,L,L1):-!,
    sbdt_or(P0,true_false,R0,L,L0),
    sbdt_or(P1,true_false,R1,L0,L1),
    sbdt_opt(PF,R0,R1,F).
sbdt_or(P,Q,R,L,L1) :-!,
    arg(1,P,PF),arg(1,Q,QF),
    sbdt_or(PF,QF,P,Q,R,L,L1).
sbdt_or(PF,QF,P,Q,R,L,L1):-PF @< QF,!,
    sbdt_or(QF,PF,Q,P,R,L,L1).
sbdt_or(PF,QF,P,Q,F,L,L1):-PF @> QF,!,
    arg(2,Q,Q0),arg(3,Q,Q1),
    sbdt_or(Q0,P,R0,L,L0),
    sbdt_or(Q1,P,R1,L0,L1),
    sbdt_opt(QF,R0,R1,F).
sbdt_or(PF,PF,P,Q,F,L,L1):-
    arg(2,P,P0),arg(3,P,P1),
    arg(2,Q,Q0),arg(3,Q,Q1),
    sbdt_or(P0,Q0,R0,L,L0),
    sbdt_or(P1,Q1,R1,L0,L1),
    sbdt_opt(PF,R0,R1,F).
sbdt_opt(_IF,THEN,ELSE,THEN) :- THEN==ELSE,!.
sbdt_opt(IF,THEN,ELSE,?(IF,THEN,ELSE)).
sbdt_r(Rg,U,V,D,U,V,D) :- 
    member(Rg,U),!.                      % in the same formula
sbdt_r(Rg,U,V,D,[Rg|U],V,[Rg|D]) :- 
    member(Rg,V),!.                      % duplicate
sbdt_r(Rg,U,V,D,[Rg|U],[Rg|V],D).        % new

or_list([],[],[]):-!.
or_list(_,_,[a]):-!.

% sbdt2(BDD0 ,BDD,Substitute)              path 2
% eliminate and renumber regular variable
% variable reordering is also necessary

sbdt2(true,true,_):-!.
sbdt2(false,false,_):-!.
sbdt2(true_false,true_false,_):-!.
sbdt2(P,P1,L) :- functor(P,?,3),!,
	sbdt2ife(P,P1,L).
sbdt2(P,F,_) :- atomic(P),!,F= ?(P,true,false).
sbdt2(P,P,_) :- write('error in sbdt2:'),write(P),nl.

sbdt2ife(?(^(R,N),T,F),TF,L) :-
    member((^(R,N),true_false),L),!,  % singleton
    sbdt2(T,T1,L),sbdt2(F,F1,L),
    sbdt_select(T1,F1,TF,L).
sbdt2ife(?(C,T,F),T2,L) :-
    sbdt2cond(C,C1,L),                % T/F may contain C1...
    sbdt2(T,T1,L),sbdt2(F,F1,L),
    sbdt_ife_t(T1,F1,C1,T2).

sbdt2cond(C,C,_) :- atomic(C),!.
sbdt2cond(^(C),N,_):- !,std_check(^(C),N).
sbdt2cond(^(R,N),R1,L):- 
    member((^(R,N),^(R,N1)),L),!,     % renumber
    std_check(^(R,N1),R1).
sbdt2cond(^(R,N),F,L):- 
    member((^(R,N),F),L),!.           % true/false
sbdt2cond(^(R,N),^(R,N),_):- !.
sbdt2cond(P,N,L):- functor(P,?,3),!,
    sbdt2(P,P1,L),std_check(P1,N).
sbdt2cond(C,C0,L) :- functor(C,H,1),!,
    functor(C1,H,1),
    arg(1,C,A),sbdt2(A,A1,L),arg(1,C1,A1),
    std_check(C1,C0).
sbdt2cond(C,C0,L) :- functor(C,H,2),!,
    functor(C1,H,2),
    arg(1,C,A),sbdt2(A,A1,L),arg(1,C1,A1),
    arg(2,C,B),sbdt2(B,B1,L),arg(2,C1,B1),
    std_check(C1,C0).
% reordering

% sbdt_split(F,TC,FT,FF),
sbdt_split(?(C,T,F),C,T,F) :- !.
sbdt_split(P,C,P,P) :- P = ?(C1,_,_),C1 @> C,!.
sbdt_split(?(C1,T1,F1),C,T,F) :- T1 @< C,!,
	sbdt_split(T1,C,CTT,CTF),
	sbdt_split(F1,C,CFT,CFF),
	sbdt_opt(C1,CTT,CFT,T),
	sbdt_opt(C1,CTF,CFF,F).
sbdt_split(T,_,T,T).

sbdt_ife(C,T,F,P) :- sbdt_ife_t(T,F,C,P).
sbdt_ife_t(T,F,C,P) :- T = ?(TC,_,_),TC @> C,!,
	sbdt_ife_f(F,T,C,P).
sbdt_ife_t(?(TC,TT,TF),F,C,P) :- TC @< C,!,
	sbdt_split(F,TC,FT,FF),
	sbdt_ife_t(TT,FT,C,PT),
	sbdt_ife_t(TF,FF,C,PF),
	sbdt_opt(TC,PT,PF,P).
sbdt_ife_t(?(C,TT,_),F,C,P) :- !,
	sbdt_ife_f(F,TT,C,P).
sbdt_ife_t(T,F,C,P) :- !,
	sbdt_ife_f(F,T,C,P).

sbdt_ife_f(F,T,C,P) :- F = ?(FC,_,_),FC @> C,!,
	sbdt_opt(C,T,F,P).
sbdt_ife_f(?(FC,FT,FF),T,C,P) :- FC @< C,!,
	sbdt_split(T,FC,TT,TF),
	sbdt_ife_f(FT,TT,C,PT),
	sbdt_ife_f(FF,TF,C,PF),
	sbdt_opt(FC,PT,PF,P).
sbdt_ife_f(?(C,_,F),T,C,P) :- !,
	% We don't have go further, it is already reordered
	sbdt_opt(C,T,F,P).
sbdt_ife_f(F,T,C,P) :-
	sbdt_opt(C,T,F,P).

sbdt_select(true_false,_,true_false,_):-!.
sbdt_select(_,true_false,true_false,_):-!.
sbdt_select(false,true,true_false,_):-!.
sbdt_select(true,false,true_false,_):-!.
sbdt_select(I,I1,I,_):-atomic(I),I=I1,!.
sbdt_select(P,Q,R,L) :-
    arg(1,P,PF), arg(1,Q,QF),!,
    sbdt_select(PF,QF,P,Q,R,L).
sbdt_select(?(C,T,F),Q,R,L) :- 
    sbdt_select(T,Q,T1,L),
    sbdt_select(F,Q,F1,L),
    sbdt_opt(C,T1,F1,R).
sbdt_select(Q,?(C,T,F),R,L) :- 
    sbdt_select(T,Q,T1,L),
    sbdt_select(F,Q,F1,L),
    sbdt_opt(C,T1,F1,R).

sbdt_select(PF,QF,P,Q,R,L):-PF @< QF,!,
    sbdt_select(QF,PF,Q,P,R,L).
sbdt_select(PF,QF,P,Q,F,L):-PF @> QF,!,
    arg(2,Q,Q0),arg(3,Q,Q1),
    sbdt_select(Q0,P,R0,L),
    sbdt_select(Q1,P,R1,L),
    sbdt_opt(QF,R0,R1,F).
sbdt_select(PF,PF,P,Q,F,L):-
    arg(2,P,P0),arg(3,P,P1),
    arg(2,Q,Q0),arg(3,Q,Q1),
    sbdt_select(P0,Q0,R0,L),
    sbdt_select(P1,Q1,R1,L),
    sbdt_opt(PF,R0,R1,F).

% sbdt_unify(3Valued,Detailed)
% Order of regular variable checking is not necessary
sbdt_unify(true,D) :- !,D=true.
sbdt_unify(false,D) :- !,D=false.
sbdt_unify(true_false,true).
sbdt_unify(true_false,false).
sbdt_unify(N,N1) :- number(N),!,
	sb(T,N), sbdt_unify(T,N1).
sbdt_unify(N,N1) :- number(N1),!,
	sb(T,N1), sbdt_unify(T,N).
sbdt_unify(?(^(_,_),T,F),D) :- !,   % really?
	sbdt_unify(T,D),sbdt_unify(F,D).
sbdt_unify(C,?(^(_,_),T,F)) :- C = ?(_,_,_),!,  % really?
	sbdt_unify(C,T),sbdt_unify(C,F).
sbdt_unify(?(C,T1,F1),D) :- !,D = ?(C,T2,F2),
	sbdt_unify(T1,T2),sbdt_unify(F1,F2).
sbdt_unify(F,F1) :-
	functor(F,H,N),functor(F1,H,N),!,
	sbdt_unify_arg(N,N,F,F1).

sbdt_unify_arg(0,_,_,_) :- !.
sbdt_unify_arg(N,N1,F,F0) :-
    N0 is N-1,
    arg(N,F,A),arg(N,F0,A0),
    sbdt_unify(A,A0),sbdt_unify_arg(N0,N1,F,F0).

sbterm :-
	listing(sb/2),listing(itl_state/2).

bdt2itl(B,F) :- number(B),!,sb(F0,B),
	bdt2itl(F0,F).
bdt2itl(^(R,N),^(R,N)) :-!.
bdt2itl(st(R),st(R)) :-!.
bdt2itl(?(IF,THEN,ELSE),F) :-!,
	bdt2itl(IF,IF0),bdt2itl(THEN,THEN0),bdt2itl(ELSE,ELSE0),
	bdt2itl_opt(IF0,THEN0,ELSE0,F).
bdt2itl(B,F) :- atom(B),!,F=B.
bdt2itl(B,F) :- 
	functor(B,H,N),functor(F,H,N),bdt2itl_subterm(N,N,B,F).
% little more readable representation
bdt2itl_opt(IF,true,false,IF) :- !.
bdt2itl_opt(IF,false,true,not(IF)) :- !.
bdt2itl_opt(IF,true,ELSE,(IF;ELSE)) :- !.
bdt2itl_opt(IF,THEN,false,(IF,THEN)) :- !.
bdt2itl_opt(IF,false,ELSE,(not(IF);ELSE)) :- !.
bdt2itl_opt(IF,THEN,true,(not(IF),THEN)) :- !.
bdt2itl_opt(IF,THEN,ELSE,?(IF,THEN,ELSE)) :- !.
bdt2itl_subterm(0,_,_,_) :- !.
bdt2itl_subterm(N,N1,F,F0) :-
    N0 is N-1,
    arg(N,F,A),arg(N,F0,A0),
    bdt2itl(A,A0),bdt2itl_subterm(N0,N1,F,F0).

% BDT end %