|
0
|
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: rstd.pl,v 1.4 2007/08/30 05:16:36 kono Exp $
|
|
0
|
12 */
|
|
|
13 % ITL subterm standarization with BDT
|
|
|
14 %
|
|
|
15 % Fri Jun 21 10:32:58 BST 1991
|
|
|
16 %
|
|
1
|
17 % :- dynamic renaming/0,count_limit/1.
|
|
|
18
|
|
|
19 :- dynamic sb/2,sbn/1.
|
|
|
20
|
|
0
|
21 subterm_init :-
|
|
20
|
22 r_abolish(sb,2),
|
|
0
|
23 asserta((sb([],-1))),
|
|
20
|
24 r_abolish(sbn,1),
|
|
0
|
25 asserta(sbn(0)).
|
|
|
26
|
|
1
|
27 std_check([],I,?(I1,true,false)) :-!, % no regular variable
|
|
|
28 std_check(I,I1) .
|
|
|
29 std_check(_,I,?(I,true,false)) :-!. % can be changed in path 2
|
|
|
30
|
|
|
31 std_check(I,I) :- atomic(I),!.
|
|
0
|
32 std_check(I,J) :-
|
|
|
33 sb(I,J),!.
|
|
|
34 std_check(I,N1) :-
|
|
|
35 retract(sbn(N)),N1 is N+1,asserta(sbn(N1)),
|
|
|
36 assertz(sb(I,N1)),!.
|
|
|
37
|
|
1
|
38 itlstd(P,StdP,Rename) :-
|
|
|
39 sbdt(P,P1,([],[],[]),(_,Vars,Dup)), % path 1
|
|
|
40 itlstd1(Vars,Dup,P1,StdP,Rename).
|
|
|
41 itlstd1([],[],P,P,[]) :-!. % no regular variable path 1 is enough
|
|
|
42 itlstd1(Vars,Dup,P,P1,Rename) :-
|
|
|
43 rename_list(Vars,Dup,Rename),
|
|
|
44 sbdt2(P,P1,Rename). % path 2
|
|
|
45
|
|
|
46 % for detailed trace
|
|
|
47 % itlstd(PNext,StdNext,NextFull,Rename,Rename1)
|
|
|
48
|
|
|
49 itlstd(P,StdP,FullP1,_,Rename) :-
|
|
|
50 sbdt(P,FullP,([],[],[]),(_,Vars,Dup)), % path 1
|
|
|
51 itlstd2(Vars,Dup,FullP,FullP1,StdP,Rename).
|
|
|
52 itlstd2([],[],P,P,P,[]) :-!. % no regular variable path 1 is enough
|
|
|
53 itlstd2(Vars,Dup,FullP,FullP1,StdP,Rename) :-
|
|
|
54 rename_list(Vars,Dup,Rename),
|
|
|
55 sbdt2(FullP,StdP,Rename), % path 2
|
|
|
56 detailed_rename(Rename,Rename1),
|
|
|
57 write((Rename,Rename1)),nl,
|
|
|
58 sbdt2(FullP,FullP1,Rename1). % over limit replacement only
|
|
|
59
|
|
|
60 % preserve singleton variable
|
|
|
61 % fix limit overed non-singleton variable
|
|
|
62 detailed_rename([],[]) :-!.
|
|
|
63 detailed_rename([(_,true_false)|R],R1) :-!, % singleton
|
|
|
64 detailed_rename(R,R1).
|
|
|
65 detailed_rename([(_,^(_,_))|R],R1) :-!, % renaming
|
|
|
66 detailed_rename(R,R1).
|
|
|
67 detailed_rename([H|R],[H|R1]) :-!, % true/false replacement
|
|
|
68 detailed_rename(R,R1).
|
|
|
69
|
|
|
70 rename_list(L,D,R):- singleton,!,
|
|
|
71 rename_singleton(L,D,L0,R,R1),
|
|
|
72 sortC(L0,L1),
|
|
|
73 number_list(L1,L2),
|
|
|
74 compact_list(L2,R1).
|
|
|
75 rename_list(L,_,L3):- renaming,!,
|
|
|
76 sortC(L,L1),
|
|
|
77 number_list(L1,L2),
|
|
|
78 compact_list(L2,L3).
|
|
|
79 rename_list(_,_,[]).
|
|
|
80
|
|
|
81 % rename_singleton(Vars,Duplicate,Deleted,Replace,Replace1)
|
|
|
82 rename_singleton([],_,[],R,R):-!.
|
|
|
83 rename_singleton([V|L],Dup,[V|L1],R,R1):-
|
|
|
84 member(V,Dup),!,
|
|
|
85 rename_singleton(L,Dup,L1,R,R1).
|
|
|
86 rename_singleton([V|L],Dup,L1,[(V,true_false)|R],R1):-
|
|
|
87 rename_singleton(L,Dup,L1,R,R1).
|
|
|
88
|
|
|
89 uniq([],[]):-!.
|
|
|
90 uniq([H|L],[H|L1]) :-
|
|
|
91 uniq(L,H,L1).
|
|
|
92 uniq([],_,[]) :-!.
|
|
|
93 uniq([H|L],H,L1) :-!,
|
|
|
94 uniq(L,H,L1).
|
|
|
95 uniq([H|L],_,[H|L1]) :-
|
|
|
96 uniq(L,H,L1).
|
|
|
97
|
|
|
98 number_list([],[]) :-!.
|
|
|
99 number_list([^(R,S)|L],[(^(R,S),^(R,1))|L1]) :-
|
|
|
100 length_limit(LM),
|
|
|
101 number_list(L,R,2,L1,LM).
|
|
|
102
|
|
|
103 number_list([],_,_,[],_) :-!.
|
|
|
104 number_list([^(R,S)|L],R,N,[(^(R,S),^(R,N))|L1],LM) :- % same variable
|
|
|
105 N =< LM,!,
|
|
|
106 N1 is N+1,
|
|
|
107 number_list(L,R,N1,L1,LM).
|
|
|
108 number_list([^(R,S)|L],R,N,[(^(R,S),F)|L1],LM) :- % same variable
|
|
|
109 inc_var(over,_),
|
|
|
110 !,(F=true;F=false), % over the limit
|
|
|
111 number_list(L,R,N,L1,LM).
|
|
|
112 number_list([^(R,S)|L],_,_,[(^(R,S),^(R,1))|L1],LM) :- % new variable
|
|
|
113 number_list(L,R,2,L1,LM).
|
|
|
114
|
|
|
115 compact_list([],[]) :-!.
|
|
|
116 compact_list([(^(R,N),^(R,N))|L1],L2) :-!, % remove identity
|
|
|
117 compact_list(L1,L2).
|
|
|
118 compact_list([H|L1],[H|L2]) :-
|
|
|
119 compact_list(L1,L2).
|
|
|
120
|
|
|
121 % do substitution member first ( to avoid infinite loop by identity
|
|
|
122 % substitution
|
|
|
123
|
|
|
124 sbdt_s([],[]):-!.
|
|
|
125 sbdt_s([(A,B)|L],[(A,B1)|L1]):-!,
|
|
|
126 sbdt(B,B1,([],[],[]),_),
|
|
|
127 sbdt_s(L,L1).
|
|
0
|
128
|
|
|
129 % BDT classification of subterm
|
|
|
130
|
|
1
|
131 % sbdt(Input,BDD,(UseInTerm,Variable,Duplicate),( ... )) path 1
|
|
0
|
132 sbdt(true,true,L,L):-!.
|
|
|
133 sbdt(false,false,L,L):-!.
|
|
1
|
134 sbdt(true_false,true_false,L,L):-!.
|
|
0
|
135 sbdt(P,F,L,L) :- atomic(P),!,F= ?(P,true,false).
|
|
1
|
136 sbdt(?(C,T,F),?(C,T,F),L,L) :- !. % already done.
|
|
0
|
137 sbdt(not(P),F,L,L1) :- !,sbdt(P,F0,L,L0),sbdt_not(F0,F,L0,L1),!.
|
|
|
138 sbdt((P,Q),F,L,L2) :- !,
|
|
|
139 sbdt(P,P0,L,L0),sbdt(Q,Q0,L0,L1),
|
|
|
140 sbdt_and(P0,Q0,F,L1,L2),!.
|
|
|
141 sbdt((P;Q),F,L,L2) :- !,
|
|
|
142 sbdt(P,P0,L,L0),sbdt(Q,Q0,L0,L1),
|
|
|
143 sbdt_or(P0,Q0,F,L1,L2),!.
|
|
1
|
144 sbdt((P&Q), N,(U,V,D),(U,V2,D2)) :-!,
|
|
|
145 sbdt(P,P1,([],V,D),(U1,V1,D1)),
|
|
|
146 sbdt(Q,Q1,([],V1,D1),(U2,V2,D2)),
|
|
|
147 or_list(U1,U2,U3),
|
|
|
148 % projection and closure touch later part of chop
|
|
|
149 std_check(U3,(P1&Q1),N).
|
|
0
|
150 % bottom up development is effective for quantifier
|
|
1
|
151 sbdt(exists(P,Q), N,(U,R,D),(U,R1,D1)) :-!,
|
|
|
152 sbdt(Q,QF,([],R,D),(U1,R1,D1)),
|
|
|
153 std_check(U1,exists(P,QF),N).
|
|
|
154 sbdt(proj(P,Q), N,(U,V,D),(U,V2,D2)) :-!,
|
|
|
155 sbdt(P,P1,([],V,D),(U1,V1,D1)),
|
|
|
156 sbdt(Q,Q1,([],V1,D1),(U2,V2,D2)),
|
|
|
157 or_list(U1,U2,U3),
|
|
|
158 std_check(U3,proj(P1,Q1),N).
|
|
|
159 sbdt(prefix(Q), N,(U,R,D),(U,R1,D1)) :-!,
|
|
|
160 sbdt(Q,QF,([],R,D),(U1,R1,D1)),
|
|
|
161 std_check(U1,prefix(QF),N).
|
|
|
162 sbdt(^(R), ?(^(R),true,false),L,L) :-!.
|
|
|
163 sbdt(Rg, ?(Rg,true,false),(U,V,D),(U1,V1,D1)) :- Rg = ^(_,_),!,
|
|
|
164 sbdt_r(Rg,U,V,D,U1,V1,D1).
|
|
0
|
165 % Simple Functor
|
|
1
|
166 sbdt(Func,N,(U,V,D),(U,V1,D1)) :- functor(Func,H,1),!,
|
|
|
167 arg(1,Func,A),
|
|
|
168 sbdt(A,A1,([],V,D),(U1,V1,D1)),
|
|
|
169 functor(Func1,H,1),arg(1,Func1,A1),
|
|
|
170 std_check(U1,Func1,N).
|
|
|
171 sbdt(Func,N,(U,V,D),(U,V2,D2)) :- functor(Func,H,2),!,
|
|
|
172 arg(1,Func,A),sbdt(A,A1,([],V,D),(U1,V1,D1)),
|
|
|
173 arg(2,Func,B),sbdt(B,B1,([],V1,D1),(U2,V2,D2)),
|
|
|
174 functor(Func1,H,2),arg(1,Func1,A1),arg(2,Func1,B1),
|
|
|
175 or_list(U1,U2,U3),std_check(U3,Func1,N).
|
|
0
|
176 sbdt(Def,true,L,L) :-
|
|
|
177 write('bdtstd error: '),write(Def),nl.
|
|
|
178
|
|
19
|
179 sbdt_not(true,false,L,L).
|
|
|
180 sbdt_not(false,true,L,L).
|
|
|
181 sbdt_not(true_false,true_false,L,L).
|
|
|
182 sbdt_not(F,?(H,A1,B1),L,L1):-
|
|
|
183 arg(1,F,H),arg(2,F,A),arg(3,F,B),
|
|
|
184 sbdt_not(A,A1,L,L0),sbdt_not(B,B1,L0,L1).
|
|
|
185 sbdt_and(false,_,false,L,L):-!.
|
|
|
186 sbdt_and(_,false,false,L,L):-!.
|
|
|
187 sbdt_and(true,T,T,L,L):-!.
|
|
|
188 sbdt_and(T,true,T,L,L):-!.
|
|
|
189 sbdt_and(T,T1,T1,L,L):- atomic(T),T=T1,!.
|
|
|
190 sbdt_and(?(PF,P0,P1),true_false,F,L,L1):-!,
|
|
|
191 sbdt_and(P0,true_false,R0,L,L0),
|
|
|
192 sbdt_and(P1,true_false,R1,L0,L1),
|
|
|
193 sbdt_opt(PF,R0,R1,F).
|
|
|
194 sbdt_and(true_false,?(PF,P0,P1),F,L,L1):-!,
|
|
|
195 sbdt_and(P0,true_false,R0,L,L0),
|
|
|
196 sbdt_and(P1,true_false,R1,L0,L1),
|
|
|
197 sbdt_opt(PF,R0,R1,F).
|
|
|
198 sbdt_and(P,Q,R,L,L1) :-!,
|
|
|
199 arg(1,P,PF),arg(1,Q,QF),
|
|
|
200 sbdt_and(PF,QF,P,Q,R,L,L1).
|
|
|
201 sbdt_and(PF,QF,P,Q,R,L,L1):-PF @< QF,!,
|
|
|
202 sbdt_and(QF,PF,Q,P,R,L,L1).
|
|
|
203 sbdt_and(PF,QF,P,Q,F,L,L1):-PF @> QF,!,
|
|
|
204 arg(2,Q,Q0),arg(3,Q,Q1),
|
|
|
205 sbdt_and(Q0,P,R0,L,L0),
|
|
|
206 sbdt_and(Q1,P,R1,L0,L1),
|
|
|
207 sbdt_opt(QF,R0,R1,F).
|
|
|
208 sbdt_and(PF,PF,P,Q,F,L,L1):-
|
|
|
209 arg(2,P,P0),arg(3,P,P1),
|
|
|
210 arg(2,Q,Q0),arg(3,Q,Q1),
|
|
|
211 sbdt_and(P0,Q0,R0,L,L0),
|
|
|
212 sbdt_and(P1,Q1,R1,L0,L1),
|
|
|
213 sbdt_opt(PF,R0,R1,F).
|
|
|
214 sbdt_or(true,_,true,L,L):-!.
|
|
|
215 sbdt_or(_,true,true,L,L):-!.
|
|
|
216 sbdt_or(false,T,T,L,L):-!.
|
|
|
217 sbdt_or(T,false,T,L,L):-!.
|
|
|
218 sbdt_or(T,T1,T1,L,L):- atomic(T),T=T1,!.
|
|
|
219 sbdt_or(?(PF,P0,P1),true_false,F,L,L1):-!,
|
|
|
220 sbdt_or(P0,true_false,R0,L,L0),
|
|
|
221 sbdt_or(P1,true_false,R1,L0,L1),
|
|
|
222 sbdt_opt(PF,R0,R1,F).
|
|
|
223 sbdt_or(true_false,?(PF,P0,P1),F,L,L1):-!,
|
|
|
224 sbdt_or(P0,true_false,R0,L,L0),
|
|
|
225 sbdt_or(P1,true_false,R1,L0,L1),
|
|
|
226 sbdt_opt(PF,R0,R1,F).
|
|
|
227 sbdt_or(P,Q,R,L,L1) :-!,
|
|
|
228 arg(1,P,PF),arg(1,Q,QF),
|
|
|
229 sbdt_or(PF,QF,P,Q,R,L,L1).
|
|
|
230 sbdt_or(PF,QF,P,Q,R,L,L1):-PF @< QF,!,
|
|
|
231 sbdt_or(QF,PF,Q,P,R,L,L1).
|
|
|
232 sbdt_or(PF,QF,P,Q,F,L,L1):-PF @> QF,!,
|
|
|
233 arg(2,Q,Q0),arg(3,Q,Q1),
|
|
|
234 sbdt_or(Q0,P,R0,L,L0),
|
|
|
235 sbdt_or(Q1,P,R1,L0,L1),
|
|
|
236 sbdt_opt(QF,R0,R1,F).
|
|
|
237 sbdt_or(PF,PF,P,Q,F,L,L1):-
|
|
|
238 arg(2,P,P0),arg(3,P,P1),
|
|
|
239 arg(2,Q,Q0),arg(3,Q,Q1),
|
|
|
240 sbdt_or(P0,Q0,R0,L,L0),
|
|
|
241 sbdt_or(P1,Q1,R1,L0,L1),
|
|
|
242 sbdt_opt(PF,R0,R1,F).
|
|
|
243 sbdt_opt(_IF,THEN,ELSE,THEN) :- THEN==ELSE,!.
|
|
|
244 sbdt_opt(IF,THEN,ELSE,?(IF,THEN,ELSE)).
|
|
|
245 sbdt_r(Rg,U,V,D,U,V,D) :-
|
|
|
246 member(Rg,U),!. % in the same formula
|
|
|
247 sbdt_r(Rg,U,V,D,[Rg|U],V,[Rg|D]) :-
|
|
|
248 member(Rg,V),!. % duplicate
|
|
|
249 sbdt_r(Rg,U,V,D,[Rg|U],[Rg|V],D). % new
|
|
|
250
|
|
1
|
251 or_list([],[],[]):-!.
|
|
|
252 or_list(_,_,[a]):-!.
|
|
|
253
|
|
|
254 % sbdt2(BDD0 ,BDD,Substitute) path 2
|
|
|
255 % eliminate and renumber regular variable
|
|
|
256 % variable reordering is also necessary
|
|
|
257
|
|
|
258 sbdt2(true,true,_):-!.
|
|
|
259 sbdt2(false,false,_):-!.
|
|
|
260 sbdt2(true_false,true_false,_):-!.
|
|
|
261 sbdt2(P,P1,L) :- functor(P,?,3),!,
|
|
|
262 sbdt2ife(P,P1,L).
|
|
|
263 sbdt2(P,F,_) :- atomic(P),!,F= ?(P,true,false).
|
|
|
264 sbdt2(P,P,_) :- write('error in sbdt2:'),write(P),nl.
|
|
|
265
|
|
|
266 sbdt2ife(?(^(R,N),T,F),TF,L) :-
|
|
|
267 member((^(R,N),true_false),L),!, % singleton
|
|
|
268 sbdt2(T,T1,L),sbdt2(F,F1,L),
|
|
|
269 sbdt_select(T1,F1,TF,L).
|
|
|
270 sbdt2ife(?(C,T,F),T2,L) :-
|
|
|
271 sbdt2cond(C,C1,L), % T/F may contain C1...
|
|
|
272 sbdt2(T,T1,L),sbdt2(F,F1,L),
|
|
|
273 sbdt_ife_t(T1,F1,C1,T2).
|
|
|
274
|
|
|
275 sbdt2cond(C,C,_) :- atomic(C),!.
|
|
|
276 sbdt2cond(^(C),N,_):- !,std_check(^(C),N).
|
|
|
277 sbdt2cond(^(R,N),R1,L):-
|
|
|
278 member((^(R,N),^(R,N1)),L),!, % renumber
|
|
|
279 std_check(^(R,N1),R1).
|
|
|
280 sbdt2cond(^(R,N),F,L):-
|
|
|
281 member((^(R,N),F),L),!. % true/false
|
|
|
282 sbdt2cond(^(R,N),^(R,N),_):- !.
|
|
|
283 sbdt2cond(P,N,L):- functor(P,?,3),!,
|
|
|
284 sbdt2(P,P1,L),std_check(P1,N).
|
|
|
285 sbdt2cond(C,C0,L) :- functor(C,H,1),!,
|
|
|
286 functor(C1,H,1),
|
|
|
287 arg(1,C,A),sbdt2(A,A1,L),arg(1,C1,A1),
|
|
|
288 std_check(C1,C0).
|
|
|
289 sbdt2cond(C,C0,L) :- functor(C,H,2),!,
|
|
|
290 functor(C1,H,2),
|
|
|
291 arg(1,C,A),sbdt2(A,A1,L),arg(1,C1,A1),
|
|
|
292 arg(2,C,B),sbdt2(B,B1,L),arg(2,C1,B1),
|
|
|
293 std_check(C1,C0).
|
|
|
294 % reordering
|
|
|
295
|
|
|
296 % sbdt_split(F,TC,FT,FF),
|
|
|
297 sbdt_split(?(C,T,F),C,T,F) :- !.
|
|
|
298 sbdt_split(P,C,P,P) :- P = ?(C1,_,_),C1 @> C,!.
|
|
|
299 sbdt_split(?(C1,T1,F1),C,T,F) :- T1 @< C,!,
|
|
|
300 sbdt_split(T1,C,CTT,CTF),
|
|
|
301 sbdt_split(F1,C,CFT,CFF),
|
|
|
302 sbdt_opt(C1,CTT,CFT,T),
|
|
|
303 sbdt_opt(C1,CTF,CFF,F).
|
|
|
304 sbdt_split(T,_,T,T).
|
|
|
305
|
|
|
306 sbdt_ife(C,T,F,P) :- sbdt_ife_t(T,F,C,P).
|
|
|
307 sbdt_ife_t(T,F,C,P) :- T = ?(TC,_,_),TC @> C,!,
|
|
|
308 sbdt_ife_f(F,T,C,P).
|
|
|
309 sbdt_ife_t(?(TC,TT,TF),F,C,P) :- TC @< C,!,
|
|
|
310 sbdt_split(F,TC,FT,FF),
|
|
|
311 sbdt_ife_t(TT,FT,C,PT),
|
|
|
312 sbdt_ife_t(TF,FF,C,PF),
|
|
|
313 sbdt_opt(TC,PT,PF,P).
|
|
|
314 sbdt_ife_t(?(C,TT,_),F,C,P) :- !,
|
|
|
315 sbdt_ife_f(F,TT,C,P).
|
|
|
316 sbdt_ife_t(T,F,C,P) :- !,
|
|
|
317 sbdt_ife_f(F,T,C,P).
|
|
|
318
|
|
|
319 sbdt_ife_f(F,T,C,P) :- F = ?(FC,_,_),FC @> C,!,
|
|
|
320 sbdt_opt(C,T,F,P).
|
|
|
321 sbdt_ife_f(?(FC,FT,FF),T,C,P) :- FC @< C,!,
|
|
|
322 sbdt_split(T,FC,TT,TF),
|
|
|
323 sbdt_ife_f(FT,TT,C,PT),
|
|
|
324 sbdt_ife_f(FF,TF,C,PF),
|
|
|
325 sbdt_opt(FC,PT,PF,P).
|
|
|
326 sbdt_ife_f(?(C,_,F),T,C,P) :- !,
|
|
|
327 % We don't have go further, it is already reordered
|
|
|
328 sbdt_opt(C,T,F,P).
|
|
|
329 sbdt_ife_f(F,T,C,P) :-
|
|
|
330 sbdt_opt(C,T,F,P).
|
|
|
331
|
|
|
332 sbdt_select(true_false,_,true_false,_):-!.
|
|
|
333 sbdt_select(_,true_false,true_false,_):-!.
|
|
|
334 sbdt_select(false,true,true_false,_):-!.
|
|
|
335 sbdt_select(true,false,true_false,_):-!.
|
|
|
336 sbdt_select(I,I1,I,_):-atomic(I),I=I1,!.
|
|
|
337 sbdt_select(P,Q,R,L) :-
|
|
|
338 arg(1,P,PF), arg(1,Q,QF),!,
|
|
|
339 sbdt_select(PF,QF,P,Q,R,L).
|
|
|
340 sbdt_select(?(C,T,F),Q,R,L) :-
|
|
|
341 sbdt_select(T,Q,T1,L),
|
|
|
342 sbdt_select(F,Q,F1,L),
|
|
|
343 sbdt_opt(C,T1,F1,R).
|
|
|
344 sbdt_select(Q,?(C,T,F),R,L) :-
|
|
|
345 sbdt_select(T,Q,T1,L),
|
|
|
346 sbdt_select(F,Q,F1,L),
|
|
|
347 sbdt_opt(C,T1,F1,R).
|
|
|
348
|
|
|
349 sbdt_select(PF,QF,P,Q,R,L):-PF @< QF,!,
|
|
|
350 sbdt_select(QF,PF,Q,P,R,L).
|
|
|
351 sbdt_select(PF,QF,P,Q,F,L):-PF @> QF,!,
|
|
|
352 arg(2,Q,Q0),arg(3,Q,Q1),
|
|
|
353 sbdt_select(Q0,P,R0,L),
|
|
|
354 sbdt_select(Q1,P,R1,L),
|
|
|
355 sbdt_opt(QF,R0,R1,F).
|
|
|
356 sbdt_select(PF,PF,P,Q,F,L):-
|
|
|
357 arg(2,P,P0),arg(3,P,P1),
|
|
|
358 arg(2,Q,Q0),arg(3,Q,Q1),
|
|
|
359 sbdt_select(P0,Q0,R0,L),
|
|
|
360 sbdt_select(P1,Q1,R1,L),
|
|
|
361 sbdt_opt(PF,R0,R1,F).
|
|
|
362
|
|
|
363 % sbdt_unify(3Valued,Detailed)
|
|
|
364 % Order of regular variable checking is not necessary
|
|
|
365 sbdt_unify(true,D) :- !,D=true.
|
|
|
366 sbdt_unify(false,D) :- !,D=false.
|
|
|
367 sbdt_unify(true_false,true).
|
|
|
368 sbdt_unify(true_false,false).
|
|
|
369 sbdt_unify(N,N1) :- number(N),!,
|
|
|
370 sb(T,N), sbdt_unify(T,N1).
|
|
|
371 sbdt_unify(N,N1) :- number(N1),!,
|
|
|
372 sb(T,N1), sbdt_unify(T,N).
|
|
|
373 sbdt_unify(?(^(_,_),T,F),D) :- !, % really?
|
|
|
374 sbdt_unify(T,D),sbdt_unify(F,D).
|
|
|
375 sbdt_unify(C,?(^(_,_),T,F)) :- C = ?(_,_,_),!, % really?
|
|
|
376 sbdt_unify(C,T),sbdt_unify(C,F).
|
|
|
377 sbdt_unify(?(C,T1,F1),D) :- !,D = ?(C,T2,F2),
|
|
|
378 sbdt_unify(T1,T2),sbdt_unify(F1,F2).
|
|
|
379 sbdt_unify(F,F1) :-
|
|
|
380 functor(F,H,N),functor(F1,H,N),!,
|
|
|
381 sbdt_unify_arg(N,N,F,F1).
|
|
19
|
382
|
|
|
383 sbdt_unify_arg(0,_,_,_) :- !.
|
|
|
384 sbdt_unify_arg(N,N1,F,F0) :-
|
|
|
385 N0 is N-1,
|
|
|
386 arg(N,F,A),arg(N,F0,A0),
|
|
|
387 sbdt_unify(A,A0),sbdt_unify_arg(N0,N1,F,F0).
|
|
0
|
388
|
|
|
389 sbterm :-
|
|
|
390 listing(sb/2),listing(itl_state/2).
|
|
|
391
|
|
|
392 bdt2itl(B,F) :- number(B),!,sb(F0,B),
|
|
|
393 bdt2itl(F0,F).
|
|
|
394 bdt2itl(^(R,N),^(R,N)) :-!.
|
|
|
395 bdt2itl(st(R),st(R)) :-!.
|
|
1
|
396 bdt2itl(?(IF,THEN,ELSE),F) :-!,
|
|
0
|
397 bdt2itl(IF,IF0),bdt2itl(THEN,THEN0),bdt2itl(ELSE,ELSE0),
|
|
|
398 bdt2itl_opt(IF0,THEN0,ELSE0,F).
|
|
|
399 bdt2itl(B,F) :- atom(B),!,F=B.
|
|
|
400 bdt2itl(B,F) :-
|
|
|
401 functor(B,H,N),functor(F,H,N),bdt2itl_subterm(N,N,B,F).
|
|
19
|
402 % little more readable representation
|
|
|
403 bdt2itl_opt(IF,true,false,IF) :- !.
|
|
|
404 bdt2itl_opt(IF,false,true,not(IF)) :- !.
|
|
|
405 bdt2itl_opt(IF,true,ELSE,(IF;ELSE)) :- !.
|
|
|
406 bdt2itl_opt(IF,THEN,false,(IF,THEN)) :- !.
|
|
|
407 bdt2itl_opt(IF,false,ELSE,(not(IF);ELSE)) :- !.
|
|
|
408 bdt2itl_opt(IF,THEN,true,(not(IF),THEN)) :- !.
|
|
|
409 bdt2itl_opt(IF,THEN,ELSE,?(IF,THEN,ELSE)) :- !.
|
|
|
410 bdt2itl_subterm(0,_,_,_) :- !.
|
|
|
411 bdt2itl_subterm(N,N1,F,F0) :-
|
|
|
412 N0 is N-1,
|
|
|
413 arg(N,F,A),arg(N,F0,A0),
|
|
|
414 bdt2itl(A,A0),bdt2itl_subterm(N0,N1,F,F0).
|
|
0
|
415
|
|
|
416 % BDT end %
|
|
1
|
417
|
