Mercurial > hg > Applications > Lite

changeset 0:b35e4dc6ec23

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Initial revision
author kono
date Sat, 16 Sep 1995 12:20:45 +0900
parents
children 683efd6f9a81
files dvcomp.pl rstd.pl
diffstat 2 files changed, 549 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/dvcomp.pl	Sat Sep 16 12:20:45 1995 +0900
@@ -0,0 +1,388 @@
+/*
+ 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$
+*/
+
+% itl decomposition for DST
+
+:- dynamic regular_limit/1.
+% requires [chop]
+% itl(Predicate,Next,Empty,ConditionLists)
+
+itl(P) :- expand(P,P0),
+	moref(Ev),itl(P0,Next,Ev,[],C),
+	write(([Ev|C]->Next)),nl,fail.
+itl(_).
+itl(P,Next,[Ev|C]) :- moref(Ev),itl(P,Next,Ev,[],C).
+
+moref(empty).
+moref(more).
+
+% :- table itl/5.
+
+itl(N,F,E,C,C1):-number(N),!,
+	sb(Subterm,N),!,itl(Subterm,F,E,C,C1).
+itl(true,true,_,C,C):-!.
+itl(false,false,_,C,C):-!.
+itl(more,false,empty,C,C).
+itl(more,true,E,C,C):-!,E = more.
+% next two rule determines descrete time
+itl(empty,true,empty,C,C).      
+itl(empty,false,E,C,C):-!,E = more.  % no succeeding more interval
+itl(P,FF,_,C,C1) :- atomic(P),!, local(FF,P,C,C1).
+    local(true,P,C,C1):- true(C,P,C,C1).
+       true([],P,C,[P|C]):-!.
+       true([P|_],P,C,C):-!.
+       true([not(P)|_],P,_,_):-!,fail.
+       true([_|T],P,C,C1):-true(T,P,C,C1).
+    local(false,P,C,C1):- false(C,P,C,C1).
+       false([],P,C,[not(P)|C]):-!.
+       false([P|_],P,_,_):-!,fail.
+       false([not(P)|_],P,C,C):-!.
+       false([_|T],P,C,C1):-false(T,P,C,C1).
+itl(@(P),P,more,C,C).		   % strong next
+itl(@(_),false,E,C,C):-!,E=empty.
+
+itl(?(Cond,T,F),N,E,C,C1):-!,
+	itl(Cond,CN,E,C,C0),itl_cond(CN,T,F,N,E,C0,C1).
+itl_cond(true,T,_,N,E,C,C1) :-!,
+	itl(T,N,E,C,C1).
+itl_cond(false,_,F,N,E,C,C1) :-!,
+	itl(F,N,E,C,C1).
+itl_cond(CN,T,F,N,E,C,C1) :-!,
+	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).
+% 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).
+
+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
+	E=more, S1 is S+1.
+
+% Quantifier
+itl(exists(P,Q),F,E,C,C0) :-!,
+	itl(Q,QT,E,[P|C],C1),itl_ex(QT,Q,E,P,F,C1,C0).
+    itl_ex(true,_,_,P,true,C,C1):-!,remove_p(C,P,C1).
+    itl_ex(false,Q,E,P,F,C,C0):-  !,remove_p(C,P,C1),
+    	itl(Q,QF,E,[not(P)|C1],C2),remove_p(C2,P,C0), exists(QF,P,F).
+    itl_ex(QT,Q,E,P,F,C,C0):- remove_p(C,P,C1),
+    	itl(Q,QF,E,[not(P)|C1],C2), remove_p(C2,P,C0),
+        or(QT,QF,TF),exists(TF,P,F).
+    % constant order optimzation for quantifier
+    exists(P,P,true):-!.
+    exists(P,_,P):-atomic(P),!.
+    exists(Q,P,exists(P,Q)).
+    remove_p([],_,[]):-!.
+    remove_p([not(P)|T],P,T):-!.
+    remove_p([P|T],P,T):-!.
+    remove_p([H|T],P,[H|T1]):-!,remove_p(T,P,T1).
+itl(*(P),F,empty,C,C1):-!,itl(P,F,empty,C,C1).
+itl(*(P),F,E,C,C1):-!,E=more,
+	itl(P,PX,more,C,C1),
+	closure(PX,P,F).
+    closure(false,_,false):-!.
+    closure(PX,P,(PX & *(P))).              %% infinite clousre (strong)
+%%    closure(PX,P,(PX & (*(P);empty))).    %% finite closure (weak)
+%% external state diagram
+itl(st(N),F,E,C,C1):-!,
+        setof((Cond=>X),st(N,Cond,X),L),itl_transition(L,F,E,C,C1).
+    itl_transition([],false,_,C,C):-!.
+    itl_transition([(Cond=>empty)|T],F,E,C,C1):-!,
+        itl((empty,Cond),F0,E,C,C0),
+        itl_transition(T,F1,E,C0,C1),or(F0,F1,F).
+    itl_transition([(Cond=>X)|T],F,E,C,C1):-
+        itl((more,Cond),F0,E,C,C0),
+        itl_transition1(F0,X,T,F,E,C0,C1).
+    itl_transition1(false,_,T,F,E,C,C1):-
+        itl_transition(T,F,E,C,C1).
+    itl_transition1(true,X,T,(st(X);F),E,C,C1):-
+        itl_transition(T,F,E,C,C1).
+%% ignore last state to check non stop predicate
+itl(non_terminate(_),F,empty,C,C):-!,F=true.
+itl(non_terminate(L),F,more,C,C1):-!,
+    itl(L,F,more,C,C1).
+%% shared resources or state
+itl(share(L),F,empty,C,C1):-!,
+	exclusive(L,C,C1,true,F).
+itl(share(L),F,more,C,C1):-!,
+	exclusive(L,C,C1,share(L),F).
+    exclusive([],C,C,F,F):-!.
+    exclusive([A|L],C,C1,F,F1):-
+	true(C,A,C,C0),exclusive1(L,C0,C1,F,F1).
+    exclusive([N|L],C,C1,F,F1):-
+	false(C,N,C,C0), !,exclusive(L,C0,C1,F,F1).
+%    exclusive(_,C,C,_,false).   % eliminate this brach
+    exclusive1([],C,C,F,F):-!.
+    exclusive1([H|L],C,C1,F,F1):-
+	false(C,H,C,C0), !,exclusive1(L,C0,C1,F,F1).
+%    exclusive1(_,C,C,_,false).
+%%
+itl((P,Q),N,E,C,C1) :-!,
+	itl(P,PN,E,C,C0),itland(PN,Q,N,E,C0,C1).
+itland(false,_,false,_,C0,C0):-!.
+itland(true,Q,QN,E,C0,C1):-!,itl(Q,QN,E,C0,C1).
+itland(PN,Q,N,E,C0,C1):-
+	itl(Q,QN,E,C0,C1),and(PN,QN,N).		%% and/3 in chop.pl
+itl((P;Q),N,E,C,C1) :-!,
+	itl(P,PN,E,C,C0),itlor(PN,Q,N,E,C0,C1).
+itlor(true,_,true,_,C0,C0):-!.
+itlor(false,Q,QN,E,C0,C1):-!,itl(Q,QN,E,C0,C1).
+itlor(PN,Q,N,E,C0,C1):-
+	itl(Q,QN,E,C0,C1),or(PN,QN,N).		%% or/3 in chop.pl
+itl(not(P),NN,E,X,X1) :- !,
+	itl(P,N,E,X,X1),
+	negate(N,NN).				%% negate/2 in chop.pl
+% F = empty?(P,Q):(empty(P)*more(Q)+more(PM)&Q)
+itl((P&Q),F,empty,C,C1) :-!,
+	itl((P,Q),F,empty,C,C1).
+itl((P&Q),F,more,C,C2) :-!,
+	itl(P,PE,empty,C,C0),
+	itl(P,PM,more,C0,C1),
+	chop(PM,PE,F,Q,C1,C2).
+
+chop(false,false,false,_,C,C):-!.
+chop(PM,false,(PM & Q),Q,C,C):-!.
+chop(PM,true,F,Q,C,C1):-!,
+    itl(Q,QF,more,C,C1),
+    chop1(PM,QF,Q,F).
+chop(PM,PE,F,Q,C,C):-!,
+	write('next empty conflict:'),write((PM,PE,F,Q,C)),nl,!,
+	fail.
+
+chop1(false,QF,_,QF):-!.
+chop1(false,false,_,false):-!.
+chop1(PM,false,Q,(PM&Q)):-!.
+chop1(_,true,_,true):-!.
+chop1(PM,QF,Q,(QF;(PM&Q))):-!.
+
+itl(proj(_,Q),F,empty,C,C1) :-!,
+	itl(Q,F,empty,C,C1).
+itl(proj(P,Q),F,more,C,C1) :-!,
+	itl(P,PM,more,C,C0),
+	itl(Q,QM,more,C0,C1),
+	prj(PM,QM,P,F).
+prj(false,_,_,false):-!.
+prj(_,false,_,false):-!.
+prj(PM,QM,P,(PM&proj(P,QM))).
+
+itl(prefix(P),F,empty,C,C1) :-!,
+	itl(P,PE,empty,C,C0),
+	itl(P,PM,more,C0,C1),
+	prefix(PM,PE,F).
+itl(prefix(P),F,more,C,C1) :-!,
+	itl(P,PM,more,C,C1),
+	prefix(PM,F).
+
+prefix(true,true):-!.
+prefix(false,false):-!.
+prefix(PM,prefix(PM)):-!.
+
+prefix(true,_,true):-!.
+prefix(_,true,true):-!.
+prefix(false,false,false):-!.
+prefix(_,false,true):-!.
+
+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
+%
+% Mon May 20 17:24:23 BST 1991
+% require([chop]).
+
+:-dynamic verbose/0,state/2,links/2.
+:-dynamic stay/3,lazy/0,singleton/0.
+
+:-assert(verbose).
+verbose(off) :- retract(verbose),fail;true.
+verbose(on) :- asserta(verbose).
+
+lazy(off) :- retract(lazy),fail;true.
+lazy(on) :- asserta(lazy).
+
+singleton(off) :- retract(singleton),fail;true.
+singleton(on) :- asserta(singleton).
+
+set_limit(X) :-
+    set_var(regular_limit,X,_).
+
+deve(ITL) :-
+	init,!,
+	expand(ITL,ITL0),		% chop standard form
+	itlstd(ITL0,StdNOW),		% BDT
+	assert(itl_state(StdNOW,1)),!,  % Initial State
+	deve0((1,StdNOW)).
+
+deve0((S,ITL)) :-
+        show_state(S,ITL),
+	bagof(Next,itldecomp(ITL,Next,S),
+	    Nexts),!,
+	deve1(Nexts).
+deve0(_).
+
+deve1([]).
+deve1([H|T]) :- deve0(H),deve1(T).
+
+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),
+
+	itlstd(Next,StdNext1,[]),
+	bdt2itl(StdNext,ItlNext),
+	bdt2itl(StdNext1,ItlNext1),
+	(ItlNext \== ItlNext1 -> write('>>'),
+	   write(ItlNext),nl,write('  '),
+           write(ItlNext1),nl; true),
+
+	check_state(StdNext,Cond,New,S),
+	(lazy,!;assertz(state(From,Cond,S))),
+	(links(S,From),!;assertz(links(S,From))),
+	itlshow0(S,Cond,StdNext,New),
+	!.
+
+itlshow0(S,Cond,Next,New) :- verbose,!,
+	itlshow1(S,Cond,Next,New),nl,!,New=1.
+itlshow0(0,_,_,0):- !,put(101),!,fail.   % "e"
+itlshow0(false,_,_,0):- !,put(102),!,fail.  % "f"
+itlshow0(true,_,_,0):- !,put(116),!,fail. % "t"
+itlshow0(_,_,_,0):- !,put(46),!,fail.    % "."
+itlshow0(S,_,_,1):- !,write(S),put(46),ttyflush,!.
+
+itlshow1(0,Cond,_,_):-!,
+	write(Cond),write('->'),write(empty).  itlshow1(true,Cond,_,_):-!,
+	write(Cond),write('->'),write(true).
+itlshow1(false,Cond,_,_):-!,
+	write(Cond),write('->'),write(false).
+itlshow1(S,Cond,_,0):-!,
+	write(Cond),write('->'),write(S).
+itlshow1(S,Cond,Org,1):-
+	write(Cond),write('->'),write(S),
+	put(9),bdt2itl(Org,Org0),write(Org0),!.
+
+lazy_state(From,Cond,S) :-
+	links(S,From),
+	itl_state(ITL,From),
+	itl(ITL,Next,Cond),
+	itlstd(Next,StdNext),
+	check_state(StdNext,Cond,_,S).
+
+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)),
+        asserta(itl_state(empty,0)),
+        asserta(itl_state(true,true)),
+	abolish(links,2),asserta(links(true,true)),
+        init_var(current,0),
+        init_var(regular_limit,5),
+	init_var(itl_state_number,1),!.
+
+show_state(S,ITL) :-
+	bdt2itl(ITL,ITL0),
+	nl,write('state('),write(S),  % (
+	(verbose,write(' , '), write(ITL0),write(')'),nl;write(')')),!.
+
+check_state(true,[more |_],0,true):-!.
+check_state(true,[empty|_],0,0):-!.
+check_state(false,_,0,false):-!.
+check_state(STD,_,0,S):-
+	itl_state(STD,S),!.
+check_state(STD,_,1,S):-
+	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),!.
+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),
+        asserta(F1),!.
+set_var(Name,X,X1) :-
+        functor(F,Name,1),retract(F),!,arg(1,F,X),
+	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_statistics.
+
+%% end %%
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/rstd.pl	Sat Sep 16 12:20:45 1995 +0900
@@ -0,0 +1,161 @@
+%
+/*
+ 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$
+*/
+% ITL subterm standarization with BDT
+%
+% Fri Jun 21 10:32:58 BST 1991
+%
+% a standard form of ITL, based on subterm classification
+%
+%
+subterm_init :- 
+	abolish(sb,2),
+	asserta((sb([],-1))),
+	abolish(sbn,1),
+	asserta(sbn(0)).
+
+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),_).
+
+% BDT classification of subterm
+
+sbdt(true,true,L,L):-!.
+sbdt(false,false,L,L):-!.
+sbdt(P,F,L,L) :- atomic(P),!,F= ?(P,true,false).
+sbdt(?(C,T,F),?(C,T,F),L,L) :- !.
+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(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((P,Q),F,L,L2) :- !,
+	sbdt(P,P0,L,L0),sbdt(Q,Q0,L0,L1),
+	sbdt_and(P0,Q0,F,L1,L2),!.
+   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(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,!,
+   	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):-
+   	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((P;Q),F,L,L2) :- !,
+	sbdt(P,P0,L,L0),sbdt(Q,Q0,L0,L1),
+	sbdt_or(P0,Q0,F,L1,L2),!.
+   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(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,!,
+   	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):-
+   	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).
+% 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).
+% 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(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).
+
+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).
+% 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(B,F) :- atom(B),!,F=B.
+bdt2itl(B,F) :- 
+	functor(B,H,N),functor(F,H,N),bdt2itl_subterm(N,N,B,F).
+    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 %