%
/*
 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: bdditl.pl,v 1.2 2007/08/30 05:16:36 kono Exp $
*/
% ITL subterm standarization with BDT
%
% a standard form of ITL, based on subterm classification
%
%

% :- use_module('~/ITL/tableau/lite').
:- use_module('~/ITL/bdd/sicstus/bdd').
% :-op(900,xfy,(&)).

eitl2bdd(X,Y) :-
	lite:expand(X,X1),itl2bdd(X1,Y).
eb(X,Y) :- ex(X,X1),eitl2bdd(X1,Y).

subterm_init :- 
	(bdd:manager(0);bdd:quit),!,bdd:init,
	r_abolish(sb,2),
	r_abolish(sbn,1),assertz(sbn(2)),
	bdd:zero(F),assertz(sb(false,F)), % this is wrong...
	bdd:one(T),assertz(sb(true,T)).

subterm_check(I,J) :-
	sb(I,Jid),bdd:var_with_id(Jid,J),!.
subterm_check(I,N1) :-
	bdd:new_var_first(N1),bdd:if_id(N1,N1id),
	retract(sbn(M)),M1 is M+1,asserta(sbn(M1)),
	assertz(sb(I,N1id)),!.

% BDD classification of subterm

itl2bdd(true,T):-!,bdd:one(T).
itl2bdd(false,F):-!,bdd:zero(F).
itl2bdd(P,F) :- integer(P),!,bdd:unfree(P),P=F.  % bdd
itl2bdd(P,F) :- atom(P),!,subterm_check(P,F).
itl2bdd(?(C,T,F),N) :- !,
	itl2bdd(C,C1),itl2bdd(T,T1),itl2bdd(F,F1),
	bdd:ite(C1,T1,F1,N),bdd:free(C1),bdd:free(T1),bdd:free(F1).
itl2bdd(not(P),F) :- !,itl2bdd(P,F0),bdd:not(F0,F),bdd:free(F0).
itl2bdd((P,Q),F) :- !,
	itl2bdd(P,P0),itl2bdd(Q,Q0),
	bdd:and(P0,Q0,F),bdd:free(P0),bdd:free(Q0),!.
itl2bdd((P;Q),F) :- !,
	itl2bdd(P,P0),itl2bdd(Q,Q0),
	bdd:or(P0,Q0,F),bdd:free(P0),bdd:free(Q0),!.
itl2bdd((P&Q), N) :-!,
	itl2bdd(P,P1),itl2bdd(Q,Q1),
	subterm_check((P1&Q1),N).
itl2bdd(exists(P,Q), N) :-!,
	itl2bdd(Q,QF), itl2bdd(P,PF),
	subterm_check(exists(PF,QF),N).
itl2bdd(proj(P,Q), N) :-!,
	itl2bdd(Q,QF),itl2bdd(P,PF),
	subterm_check(proj(PF,QF),N).
itl2bdd(prefix(P), N) :-!,
	itl2bdd(P,PF),
	subterm_check(prefix(PF),N).
% Simple Functor including Regular variable and state
itl2bdd(Func,N) :- functor(Func,H,1),!,functor(F0,H,1),
	arg(1,Func,A),itl2bdd(A,A0),arg(1,F0,A0),
	subterm_check(F0,N).
itl2bdd(Func,N) :- functor(Func,H,2),!,functor(F0,H,2),
	arg(1,Func,A),itl2bdd(A,A0),arg(1,F0,A0),
	arg(2,Func,B),itl2bdd(B,B0),arg(2,F0,B0),
	subterm_check(F0,N).
itl2bdd(Def,true) :-
    write('bdditl error: '),write(Def),nl.

subterm :-
	listing(sb/2).

bdd2itl(B,F) :- integer(B),!,
	bdd:type(B,I),bdd2itl(I,B,F).
bdd2itl(B,F) :- atom(B),!,F=B.
bdd2itl(B,F) :- 
	functor(B,H,N),functor(F,H,N),bdd2itl_subterm(N,N,B,F).

bdd2itl_subterm(F,B) :- bdd:if_id(B,Bid),sb(F0,Bid),
	functor(F0,H,N),functor(F,H,N),
	bdd2itl_subterm(N,N,F0,F).
bdd2itl_subterm(0,_,_,_) :- !.
bdd2itl_subterm(N,N1,F,F0) :-
	N0 is N-1,
	arg(N,F,A),arg(N,F0,A0),
	bdd2itl(A,A0),bdd2itl_subterm(N0,N1,F,F0).

% BDD Type analysis 
bdd2itl(0,B,OPT) :- !, % nonterminal
	bdd:if(B,IF0),bdd2itl_subterm(IF,IF0),
	bdd:then(B,THEN0),bdd2itl(THEN0,THEN),
	bdd:else(B,ELSE0),bdd2itl(ELSE0,ELSE),
	bdd2itl_opt(IF,THEN,ELSE,OPT).
% little more readable representation
    bdd2itl_opt(IF,true,false,IF) :- !.
    bdd2itl_opt(IF,false,true,not(IF)) :- !.
    bdd2itl_opt(IF,true,ELSE,(IF;ELSE)) :- !.
    bdd2itl_opt(IF,THEN,false,(IF,THEN)) :- !.
    bdd2itl_opt(IF,false,ELSE,(not(IF);ELSE)) :- !.
    bdd2itl_opt(IF,THEN,true,(not(IF),THEN)) :- !.
    bdd2itl_opt(IF,THEN,ELSE,?(IF,THEN,ELSE)) :- !.
bdd2itl(1,_,false) :- !. % zero
bdd2itl(2,_,true) :- !. % one
bdd2itl(3,B,F) :- !, % posvar
	bdd2itl_subterm(F,B).
bdd2itl(4,B,not(F)) :- !, % negvar
	bdd:not(B,B1),bdd2itl_subterm(F,B1).
bdd2itl(5,_,overflow) :- !. % overflow
bdd2itl(6,_,constant) :- !. % constant (mtbdd)

% Depth One Expansion

bdd2itl1(B,F) :- integer(B),!,
	bdd:type(B,I),bdd2itl1(I,B,F).
bdd2itl1(B,F) :- atom(B),!,F=B.
bdd2itl1(B,B).

% BDD Type analysis 
bdd2itl1(0,B,?(IF,THEN,ELSE)) :- !, 	% nonterminal
	bdd:if_id(B,IF0id),sb(IF,IF0id),
	bdd:then(B,THEN),
	bdd:else(B,ELSE).    		% no use of opt
bdd2itl1(1,_,false) :- !. 		% zero
bdd2itl1(2,_,true) :- !. 		% one
bdd2itl1(3,B,F) :- !, 			% posvar
	bdd:if_id(B,Bid),sb(F,Bid).
bdd2itl1(4,B,not(F)) :- !, % negvar
	bdd:not(B,B1),bdd:if_id(B1,B1id),sb(F,B1id).
bdd2itl1(5,_,overflow) :- !. % overflow
bdd2itl1(6,_,constant) :- !. % constant (mtbdd)

	
% BDD end %