|
2
|
1 %
|
|
|
2 /*
|
|
|
3 Copyright (C) 1991, Shinji Kono, Sony Computer Science Laboratory, Inc.
|
|
|
4 The University, Newcastle upton Tyne
|
|
|
5
|
|
|
6 Everyone is permitted to copy and distribute verbatim copies
|
|
|
7 of this license, but changing it is not allowed. You can also
|
|
|
8 use this wording to make the terms for other programs.
|
|
|
9
|
|
|
10 send your comments to kono@csl.sony.co.jp
|
|
22
|
11 $Id: bdditl.pl,v 1.2 2007/08/30 05:16:36 kono Exp $
|
|
2
|
12 */
|
|
|
13 % ITL subterm standarization with BDT
|
|
|
14 %
|
|
|
15 % a standard form of ITL, based on subterm classification
|
|
|
16 %
|
|
|
17 %
|
|
|
18
|
|
|
19 % :- use_module('~/ITL/tableau/lite').
|
|
|
20 :- use_module('~/ITL/bdd/sicstus/bdd').
|
|
|
21 % :-op(900,xfy,(&)).
|
|
|
22
|
|
|
23 eitl2bdd(X,Y) :-
|
|
|
24 lite:expand(X,X1),itl2bdd(X1,Y).
|
|
|
25 eb(X,Y) :- ex(X,X1),eitl2bdd(X1,Y).
|
|
|
26
|
|
|
27 subterm_init :-
|
|
|
28 (bdd:manager(0);bdd:quit),!,bdd:init,
|
|
20
|
29 r_abolish(sb,2),
|
|
|
30 r_abolish(sbn,1),assertz(sbn(2)),
|
|
2
|
31 bdd:zero(F),assertz(sb(false,F)), % this is wrong...
|
|
|
32 bdd:one(T),assertz(sb(true,T)).
|
|
|
33
|
|
|
34 subterm_check(I,J) :-
|
|
|
35 sb(I,Jid),bdd:var_with_id(Jid,J),!.
|
|
|
36 subterm_check(I,N1) :-
|
|
|
37 bdd:new_var_first(N1),bdd:if_id(N1,N1id),
|
|
|
38 retract(sbn(M)),M1 is M+1,asserta(sbn(M1)),
|
|
|
39 assertz(sb(I,N1id)),!.
|
|
|
40
|
|
|
41 % BDD classification of subterm
|
|
|
42
|
|
|
43 itl2bdd(true,T):-!,bdd:one(T).
|
|
|
44 itl2bdd(false,F):-!,bdd:zero(F).
|
|
|
45 itl2bdd(P,F) :- integer(P),!,bdd:unfree(P),P=F. % bdd
|
|
|
46 itl2bdd(P,F) :- atom(P),!,subterm_check(P,F).
|
|
|
47 itl2bdd(?(C,T,F),N) :- !,
|
|
|
48 itl2bdd(C,C1),itl2bdd(T,T1),itl2bdd(F,F1),
|
|
|
49 bdd:ite(C1,T1,F1,N),bdd:free(C1),bdd:free(T1),bdd:free(F1).
|
|
|
50 itl2bdd(not(P),F) :- !,itl2bdd(P,F0),bdd:not(F0,F),bdd:free(F0).
|
|
|
51 itl2bdd((P,Q),F) :- !,
|
|
|
52 itl2bdd(P,P0),itl2bdd(Q,Q0),
|
|
|
53 bdd:and(P0,Q0,F),bdd:free(P0),bdd:free(Q0),!.
|
|
|
54 itl2bdd((P;Q),F) :- !,
|
|
|
55 itl2bdd(P,P0),itl2bdd(Q,Q0),
|
|
|
56 bdd:or(P0,Q0,F),bdd:free(P0),bdd:free(Q0),!.
|
|
|
57 itl2bdd((P&Q), N) :-!,
|
|
|
58 itl2bdd(P,P1),itl2bdd(Q,Q1),
|
|
|
59 subterm_check((P1&Q1),N).
|
|
|
60 itl2bdd(exists(P,Q), N) :-!,
|
|
|
61 itl2bdd(Q,QF), itl2bdd(P,PF),
|
|
|
62 subterm_check(exists(PF,QF),N).
|
|
|
63 itl2bdd(proj(P,Q), N) :-!,
|
|
|
64 itl2bdd(Q,QF),itl2bdd(P,PF),
|
|
|
65 subterm_check(proj(PF,QF),N).
|
|
|
66 itl2bdd(prefix(P), N) :-!,
|
|
|
67 itl2bdd(P,PF),
|
|
|
68 subterm_check(prefix(PF),N).
|
|
|
69 % Simple Functor including Regular variable and state
|
|
|
70 itl2bdd(Func,N) :- functor(Func,H,1),!,functor(F0,H,1),
|
|
|
71 arg(1,Func,A),itl2bdd(A,A0),arg(1,F0,A0),
|
|
|
72 subterm_check(F0,N).
|
|
|
73 itl2bdd(Func,N) :- functor(Func,H,2),!,functor(F0,H,2),
|
|
|
74 arg(1,Func,A),itl2bdd(A,A0),arg(1,F0,A0),
|
|
|
75 arg(2,Func,B),itl2bdd(B,B0),arg(2,F0,B0),
|
|
|
76 subterm_check(F0,N).
|
|
|
77 itl2bdd(Def,true) :-
|
|
|
78 write('bdditl error: '),write(Def),nl.
|
|
|
79
|
|
|
80 subterm :-
|
|
|
81 listing(sb/2).
|
|
|
82
|
|
|
83 bdd2itl(B,F) :- integer(B),!,
|
|
|
84 bdd:type(B,I),bdd2itl(I,B,F).
|
|
|
85 bdd2itl(B,F) :- atom(B),!,F=B.
|
|
|
86 bdd2itl(B,F) :-
|
|
|
87 functor(B,H,N),functor(F,H,N),bdd2itl_subterm(N,N,B,F).
|
|
|
88
|
|
|
89 bdd2itl_subterm(F,B) :- bdd:if_id(B,Bid),sb(F0,Bid),
|
|
|
90 functor(F0,H,N),functor(F,H,N),
|
|
|
91 bdd2itl_subterm(N,N,F0,F).
|
|
|
92 bdd2itl_subterm(0,_,_,_) :- !.
|
|
|
93 bdd2itl_subterm(N,N1,F,F0) :-
|
|
|
94 N0 is N-1,
|
|
|
95 arg(N,F,A),arg(N,F0,A0),
|
|
|
96 bdd2itl(A,A0),bdd2itl_subterm(N0,N1,F,F0).
|
|
|
97
|
|
|
98 % BDD Type analysis
|
|
|
99 bdd2itl(0,B,OPT) :- !, % nonterminal
|
|
|
100 bdd:if(B,IF0),bdd2itl_subterm(IF,IF0),
|
|
|
101 bdd:then(B,THEN0),bdd2itl(THEN0,THEN),
|
|
|
102 bdd:else(B,ELSE0),bdd2itl(ELSE0,ELSE),
|
|
|
103 bdd2itl_opt(IF,THEN,ELSE,OPT).
|
|
|
104 % little more readable representation
|
|
|
105 bdd2itl_opt(IF,true,false,IF) :- !.
|
|
|
106 bdd2itl_opt(IF,false,true,not(IF)) :- !.
|
|
|
107 bdd2itl_opt(IF,true,ELSE,(IF;ELSE)) :- !.
|
|
|
108 bdd2itl_opt(IF,THEN,false,(IF,THEN)) :- !.
|
|
|
109 bdd2itl_opt(IF,false,ELSE,(not(IF);ELSE)) :- !.
|
|
|
110 bdd2itl_opt(IF,THEN,true,(not(IF),THEN)) :- !.
|
|
|
111 bdd2itl_opt(IF,THEN,ELSE,?(IF,THEN,ELSE)) :- !.
|
|
|
112 bdd2itl(1,_,false) :- !. % zero
|
|
|
113 bdd2itl(2,_,true) :- !. % one
|
|
|
114 bdd2itl(3,B,F) :- !, % posvar
|
|
|
115 bdd2itl_subterm(F,B).
|
|
|
116 bdd2itl(4,B,not(F)) :- !, % negvar
|
|
|
117 bdd:not(B,B1),bdd2itl_subterm(F,B1).
|
|
|
118 bdd2itl(5,_,overflow) :- !. % overflow
|
|
|
119 bdd2itl(6,_,constant) :- !. % constant (mtbdd)
|
|
|
120
|
|
|
121 % Depth One Expansion
|
|
|
122
|
|
|
123 bdd2itl1(B,F) :- integer(B),!,
|
|
|
124 bdd:type(B,I),bdd2itl1(I,B,F).
|
|
|
125 bdd2itl1(B,F) :- atom(B),!,F=B.
|
|
|
126 bdd2itl1(B,B).
|
|
|
127
|
|
|
128 % BDD Type analysis
|
|
|
129 bdd2itl1(0,B,?(IF,THEN,ELSE)) :- !, % nonterminal
|
|
|
130 bdd:if_id(B,IF0id),sb(IF,IF0id),
|
|
|
131 bdd:then(B,THEN),
|
|
|
132 bdd:else(B,ELSE). % no use of opt
|
|
|
133 bdd2itl1(1,_,false) :- !. % zero
|
|
|
134 bdd2itl1(2,_,true) :- !. % one
|
|
|
135 bdd2itl1(3,B,F) :- !, % posvar
|
|
|
136 bdd:if_id(B,Bid),sb(F,Bid).
|
|
|
137 bdd2itl1(4,B,not(F)) :- !, % negvar
|
|
|
138 bdd:not(B,B1),bdd:if_id(B1,B1id),sb(F,B1id).
|
|
|
139 bdd2itl1(5,_,overflow) :- !. % overflow
|
|
|
140 bdd2itl1(6,_,constant) :- !. % constant (mtbdd)
|
|
|
141
|
|
|
142
|
|
|
143 % BDD end %
|
