# HG changeset patch # User kono # Date 890536948 -32400 # Node ID 683efd6f9a8155769e9bd7a2e710ce40891954c2 # Parent b35e4dc6ec2372e957169add6649c64ad591eacc *** empty log message *** diff -r b35e4dc6ec23 -r 683efd6f9a81 dvcomp.pl --- 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 %% diff -r b35e4dc6ec23 -r 683efd6f9a81 rstd.pl --- 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 % +