Mercurial > hg > Applications > Lite

changeset 1:683efd6f9a81

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
*** empty log message ***
author kono
date Sun, 22 Mar 1998 12:22:28 +0900
parents b35e4dc6ec23
children 1c57a78f1d98
files dvcomp.pl rstd.pl
diffstat 2 files changed, 402 insertions(+), 141 deletions(-) [+]
line wrap: on
line diff
--- a/dvcomp.pl	Sat Sep 16 12:20:45 1995 +0900
+++ b/dvcomp.pl	Sun Mar 22 12:22:28 1998 +0900
@@ -12,7 +12,8 @@
 
 % itl decomposition for DST
 
-:- dynamic regular_limit/1.
+:- dynamic length_limit/1,renaming/0.
+
 % requires [chop]
 % itl(Predicate,Next,Empty,ConditionLists)
 
@@ -31,6 +32,9 @@
 	sb(Subterm,N),!,itl(Subterm,F,E,C,C1).
 itl(true,true,_,C,C):-!.
 itl(false,false,_,C,C):-!.
+itl(true_false,true_false,more,C,C):-!.
+itl(true_false,true,empty,C,[choice(true)|C]).
+itl(true_false,false,E,C,[choice(false)|C]):-!,E=empty.
 itl(more,false,empty,C,C).
 itl(more,true,E,C,C):-!,E = more.
 % next two rule determines descrete time
@@ -60,21 +64,33 @@
 	itl(T,TN,E,C,C0),
 	itl(F,FN,E,C0,C1), negate(CN,NCN),
 	and(TN,CN,N1),and(FN,NCN,N2), or(N1,N2,N).
+% Non deterministic selection (singleton 2nd order variable)
+itl([],true,_,C,C):-!.
+itl([H|L],F,empty,C,C1):-!,
+	empty_choice([H|L],0,F,C,C1).
+    empty_choice([H|_],N,F,C,[choice(N)|C1]) :-
+	itl(H,F,empty,C,C1).
+    empty_choice([_|L],N,F,C,C1) :-
+	N1 is N+1,
+        empty_choice(L,N1,F,C,C1).
+itl([H|L],F,E,C,C1):-!,E=more,
+	choice([H|L],F,C,C1).
+    choice([],[],C,C) :-!.
+    choice([H|L],[H1|L1],C,C2) :-
+	itl(H,H1,more,C,C1),
+        choice(L,L1,C1,C2).
 % Regular Variable
 itl(^(R),F,empty,C,C1):-
-    local(F0,up(R),C,C0),
-    local(F1,down(R,0),C0,C1),and(F0,F1,F).
-itl(^(R),F1,E,C,[^(R,0)|C1]):-!, E=more,
-    local(F,up(R),C,C1),and(F,^(R,0),F1).
+	local(F,^(R,0),C,C1).
+itl(^(R),^(R,1),E,C,C):-!, E=more.
 
 itl(^(R,S),F,empty,C,C1):-
-    local(F,down(R,S),C,C1).
-itl(^(R,S),F,E,C,C1):- E = more,
-        regular_limit(X),S>=X,!,
-	local(F,over(R,S),C,C1).
-itl(^(R,S),^(R,S1),E,C,[^(R,S1)|C]):-!, 
-	% increment regular variable rength
-	% mark reference to detect singleton
+	local(F,^(R,S),C,C1).
+%itl(^(R,S),F,E,C,C1):- E = more,
+%        length_limit(X),S>=X,inc_var(over,_),!,
+%	S1 is S+1,local(F,over(R,S1),C,C1).    
+itl(^(R,S),^(R,S1),E,C,C):-!, 
+	% increment regular variable length
 	E=more, S1 is S+1.
 
 % Quantifier
@@ -169,6 +185,8 @@
 
 chop1(false,QF,_,QF):-!.
 chop1(false,false,_,false):-!.
+chop1(true,false,true,true):-!.
+chop1(true,_,true,true):-!.
 chop1(PM,false,Q,(PM&Q)):-!.
 chop1(_,true,_,true):-!.
 chop1(PM,QF,Q,(QF;(PM&Q))):-!.
@@ -183,6 +201,8 @@
 prj(_,false,_,false):-!.
 prj(PM,QM,P,(PM&proj(P,QM))).
 
+% prefix is not consistently defined
+% prefix(fin(false)) = true ? funny...
 itl(prefix(P),F,empty,C,C1) :-!,
 	itl(P,PE,empty,C,C0),
 	itl(P,PM,more,C0,C1),
@@ -203,38 +223,6 @@
 itl(Def,_,_,_,_) :-
     write('error: '),write(Def),nl,!,fail.
 
-% detect regular variable singleton
-% we can do renumbering here
-% what do we do for permutation?
-
-itl_singleton([empty|L],[empty|L],[]) :- !.
-itl_singleton(Cond,Cond1,Singleton) :- singleton,!,
-	select_singleton(Cond,Cond0,V),
-	split_singleton_case(V,Cond0,Cond1,Singleton).
-itl_singleton(Cond,Cond1,[]) :- 
-	select_singleton(Cond,Cond1,_).
-
-select_singleton([],[],[]):-!.
-select_singleton([^(R,S)|L],L1,V):-!,
-	check_singleton(L,^(R,S),L0,single,F),
-	(F==single -> V = [^(R,S)|V0],select_singleton(L0,L1,V0)
-                  ; select_singleton(L0,L1,V)).
-select_singleton([H|L],[H|L1],V):-!,
-	select_singleton(L,L1,V).
-
-check_singleton([],_,[],F,F):-!.
-check_singleton([H|T],H,T1,_,multi):-!,
-	check_singleton(T,H,T1,_,_).
-check_singleton([H|T],H1,[H|T1],F,F1):-!,
-	check_singleton(T,H1,T1,F,F1).
-
-% choose singleton's truth value
-% split_singleton_case(_,Cond,Cond,[]) :- !.
-split_singleton_case([],Cond,Cond,[]).
-split_singleton_case([^(R,S)|T],Cond,Cond1,[(^(R,S),true)|T1]):-
-	split_singleton_case(T,[ev(^(R,S))|Cond],Cond1,T1).
-split_singleton_case([^(R,S)|T],Cond,Cond1,[(^(R,S),false)|T1]):-
-	split_singleton_case(T,[not(ev(^(R,S)))|Cond],Cond1,T1).
 
 % develop Local ITL formula into state diagram
 %
@@ -242,25 +230,41 @@
 % require([chop]).
 
 :-dynamic verbose/0,state/2,links/2.
-:-dynamic stay/3,lazy/0,singleton/0.
+:-dynamic stay/3,lazy/0,singleton/0,detailed/0.
 
-:-assert(verbose).
 verbose(off) :- retract(verbose),fail;true.
 verbose(on) :- asserta(verbose).
+:-verbose(on).
 
 lazy(off) :- retract(lazy),fail;true.
 lazy(on) :- asserta(lazy).
 
+:-lazy(on).
+
 singleton(off) :- retract(singleton),fail;true.
 singleton(on) :- asserta(singleton).
+:-singleton(on).
+
+renaming(off) :- retract(renaming),fail;true.
+renaming(on) :- asserta(renaming).
+:-renaming(on).
+
+detail(off) :- retract(detailed),fail;true.
+detail(on) :- asserta(detailed).
+% :-detail(on).
 
 set_limit(X) :-
-    set_var(regular_limit,X,_).
+    set_var(length_limit,X,_).
+no_limit :-
+    retract(length_limit),fail.
+no_limit.
+
+:-assert(length_limit(5)).
 
 deve(ITL) :-
 	init,!,
 	expand(ITL,ITL0),		% chop standard form
-	itlstd(ITL0,StdNOW),		% BDT
+	itlstd(ITL0,StdNOW,_),		% BDT
 	assert(itl_state(StdNOW,1)),!,  % Initial State
 	deve0((1,StdNOW)).
 
@@ -277,23 +281,16 @@
 itldecomp(ITL,(NextS,StdNext),From) :-
 	init_var(current,From),
 	itl(ITL,Next,Cond),
-	itl_singleton(Cond,Cond1,Singleton),
 	%% showing
-	itlshow(Next,NextS,Cond1,From,StdNext,Singleton).
-
-itlshow(Next,S,Cond,From,StdNext,Singleton):-
-	itlstd(Next,StdNext,Singleton),
+	itlshow(Next,NextS,Cond,From,StdNext).
 
-	itlstd(Next,StdNext1,[]),
-	bdt2itl(StdNext,ItlNext),
-	bdt2itl(StdNext1,ItlNext1),
-	(ItlNext \== ItlNext1 -> write('>>'),
-	   write(ItlNext),nl,write('  '),
-           write(ItlNext1),nl; true),
-
+itlshow(Next,S,Cond,From,StdNext):-
+	itlstd(Next,StdNext,Rename),
 	check_state(StdNext,Cond,New,S),
-	(lazy,!;assertz(state(From,Cond,S))),
-	(links(S,From),!;assertz(links(S,From))),
+	(verbose,!,write(Rename);true),
+	(links(S,From),!;
+             assertz(links(S,From)),inc_var(itl_transition_count,_)),
+        inc_var(itl_transition,_),
 	itlshow0(S,Cond,StdNext,New),
 	!.
 
@@ -316,19 +313,27 @@
 	write(Cond),write('->'),write(S),
 	put(9),bdt2itl(Org,Org0),write(Org0),!.
 
-lazy_state(From,Cond,S) :-
-	links(S,From),
+% lazy transition condition generator
+
+state(From,Cond,Next) :-
+	links(Next,From),
 	itl_state(ITL,From),
-	itl(ITL,Next,Cond),
-	itlstd(Next,StdNext),
-	check_state(StdNext,Cond,_,S).
+	itl(ITL,Next0,Cond),
+	itlstd(Next0,StdNext,_),
+	check_state(StdNext,Cond,_,Next1),  % Next1 has not to be instantiated
+	Next1=Next.
+
+% detailed state transition including 2var renamings
+
+state(From,Cond,Next,FromFull,NextFull,Rename,Rename1) :-
+        links(Next,From),
+        itl(FromFull,PNext,Cond),
+        itlstd(PNext,StdNext,NextFull,Rename,Rename1),
+        check_state(StdNext,Cond,_,Next1),  % S1 has not to be instantiated
+        Next = Next1.
 
 init :-
 	subterm_init,
-	abolish(state,3),
-	asserta((state(true,[more],true):-!)),
-	asserta((state(true,[empty],0):-!)),
-	(lazy,assertz((state(A,B,C) :- lazy_state(A,B,C))),!;true),
         abolish(itl_state,2),
         abolish(stay,3),asserta(stay(0,0,0)),
         asserta(itl_state(false,false)),
@@ -336,7 +341,9 @@
         asserta(itl_state(true,true)),
 	abolish(links,2),asserta(links(true,true)),
         init_var(current,0),
-        init_var(regular_limit,5),
+        init_var(over,0),
+        init_var(itl_transition,0),
+        init_var(itl_transition_count,0),
 	init_var(itl_state_number,1),!.
 
 show_state(S,ITL) :-
@@ -353,9 +360,7 @@
 	inc_var(itl_state_number,S),
 	assert(itl_state(STD,S)),!.
 
-init_var(X,_) :- functor(F,X,1),assert(F),fail.
-init_var(X,_) :- functor(F,X,1),retract(F),fail.
-init_var(X,V) :- functor(F,X,1),arg(1,F,V),assert(F),!.
+init_var(X,V) :- abolish(X,1),functor(F,X,1),arg(1,F,V),assert(F),!.
 inc_var(Name,X1) :- 
         functor(F,Name,1),retract(F),arg(1,F,X),
         X1 is X+1,functor(F1,Name,1),arg(1,F1,X1),
@@ -365,24 +370,26 @@
 	functor(F1,Name,1),arg(1,F1,X1),asserta(F1),!.
 set_var(Name,X,_) :- init_var(Name,X).
 
-%init_var(X,_) :- recorded(X,_,Ref),erase(Ref),fail.
-%init_var(X,V) :- recorda(X,V,_).
-%inc_var(Name,X1) :- 
-%	recorded(Name,X,Ref),X1 is X+1,
-%	erase(Ref),recorda(Name,X1,_).
-%set_var(Name,X,X1) :-
-%        recorded(Name,X1,_),!,init_var(Name,X).
-%set_var(Name,X,_) :- init_var(Name,X).
 
 itl_statistics :- nl,
         itl_state_number(X),write(X),write(' states'),nl,fail.
 itl_statistics :- 
         sbn(X),write(X),write(' subterms'),nl,fail.
 itl_statistics :- 
-        init_var(tmp,0),
-        ((links(_,_),inc_var(tmp,_),fail);true),
-        tmp(N),
-        write(N),write(' state transions'),nl,fail.
+	itl_transition_count(X),
+        write(X),write(' state transions'),nl,fail.
+itl_statistics :- 
+        over(X),X=\=0,write(X),write(' interval overflows'),nl,fail.
+itl_statistics :- 
+	verbose,write('verbose,'),fail.
+itl_statistics :- 
+	renaming,write('renaming,'),fail.
+itl_statistics :- 
+	singleton,write('singleton,'),fail.
+itl_statistics :- 
+	detailed,write('detailed,'),fail.
+itl_statistics :- 
+	length_limit(X),X=\=0,write('length limit '),write(X),nl,fail.
 itl_statistics.
 
 %% end %%
--- a/rstd.pl	Sat Sep 16 12:20:45 1995 +0900
+++ b/rstd.pl	Sun Mar 22 12:22:28 1998 +0900
@@ -14,35 +14,130 @@
 %
 % Fri Jun 21 10:32:58 BST 1991
 %
-% a standard form of ITL, based on subterm classification
-%
-%
+% :- dynamic renaming/0,count_limit/1.
+
+:- dynamic sb/2,sbn/1.
+
 subterm_init :- 
 	abolish(sb,2),
 	asserta((sb([],-1))),
 	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,List) :- 
-	sbdt(P,List,(0,[]),_).
-itlstd(P,List,S) :- 
-	sbdt(P,List,(0,S),_).
+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) :- !.
+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_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).
@@ -53,20 +148,31 @@
    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,?(QF,R0,R1),L,L1):-PF @> QF,!,
+   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_and(PF,PF,P,Q,?(PF,R0,R1),L,L1):-
+   	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_and(P1,Q1,R1,L0,L1),
+	sbdt_opt(PF,R0,R1,F).
 sbdt((P;Q),F,L,L2) :- !,
 	sbdt(P,P0,L,L0),sbdt(Q,Q0,L0,L1),
 	sbdt_or(P0,Q0,F,L1,L2),!.
@@ -74,71 +180,218 @@
    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,?(QF,R0,R1),L,L1):-PF @> QF,!,
+   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_or(PF,PF,P,Q,?(PF,R0,R1),L,L1):-
+   	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((P&Q), ?(N,true,false),L,L1) :-!,
-	sbdt(P,P1,L,L0),sbdt(Q,Q1,L0,L1), 
-	% projection touch later part of chop
-	std_check((P1&Q1),N).
+   	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((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,true,false),L,L1) :-!,
-	sbdt(Q,QF,L,L1),
-	std_check(exists(P,QF),N).
-sbdt(proj(P,Q), ?(N,true,false),L,L1) :-!,
-	sbdt(Q,QF,L,L1),     % P part is fixed
-	std_check(proj(P,QF),N).
-sbdt(prefix(P), ?(N,true,false),L,L1) :-!,
-	sbdt(P,PF,L,L1),     % P part is fixed
-	std_check(prefix(PF),N).
-%sbdt(^(R), ?(N,true,false),(I,L),(I1,L1)) :-!,
-%	recorded(current,S,_),!,
-%	regular_check(L,L1,S,R,I,I1,N).
-sbdt(^(R), ?(N,true,false),(I,L),(I,L)) :-!,
-	std_check(^(R),N).
-% remove singleton regular variable
-sbdt(^(R,S), F,(I,L),(I,L)) :-
-	member((^(R,S),F),L),!.
-sbdt(^(R,S), ?(N,true,false),(I,L),(I,L)) :-!,
-	std_check(^(R,S),N).
+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).
+    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
 % Simple Functor
-sbdt(Func,F,L,L) :- functor(Func,_,1),!,F= ?(N,true,false),
-	std_check(Func,N).
-sbdt(Func,F,L,L) :- functor(Func,_,2),!,F= ?(N,true,false),
-	std_check(Func,N).
+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.
 
-% renumbering (not used now)
-regular_check([],[S,I1],S,R,I,I1,N) :- !,
-	I1 is I+1,
-	std_check(^(R,I1),N).
-regular_check([S,J|L],L,S,R,I,I1,N) :- !,
-	I1=I,
-	std_check(^(R,J),N).
-regular_check([_,_|L1],L,S,R,I,I1,N) :- !,
-	regular_check(L1,L,S,R,I,I1,N).
+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,THEN,ELSE),F) :-!,
 	bdt2itl(IF,IF0),bdt2itl(THEN,THEN0),bdt2itl(ELSE,ELSE0),
 	bdt2itl_opt(IF0,THEN0,ELSE0,F).
 % little more readable representation
@@ -159,3 +412,4 @@
 	bdt2itl(A,A0),bdt2itl_subterm(N0,N1,F,F0).
 
 % BDT end %
+