2:- module(callInference,[callTPandMB/8,
3 callMBbis/7]). 4
5:- use_module(library(lists),[member/2,select/3]). 6
7:- use_module(nutcracker(fol2otter),[fol2otter/3,fol2mace/3]). 8:- use_module(nutcracker(fol2bliksem),[fol2bliksem/3]). 9:- use_module(nutcracker(fol2tptp),[fol2tptp/3,fol2tptpOld/3]). 10
11:- use_module(semlib(options),[option/2]). 12
13
17
18initEngine(Opt,Temp,Axioms,Formula,vampire):-
19 option(Opt,vampire),
20 access_file('ext/bin/vampire',execute), !,
21 atom_concat(Temp,'/vampire.in',InFile),
22 open(InFile,write,Stream),
23 fol2tptpOld(Axioms,Formula,Stream),
24 close(Stream).
25
26initEngine(Opt,Temp,Axioms,Formula,otter):-
27 option(Opt,otter),
28 access_file('ext/bin/otter',execute), !,
29 atom_concat(Temp,'/otter.in',InFile),
30 open(InFile,write,Stream),
31 fol2otter(Axioms,not(Formula),Stream),
32 close(Stream).
33
34initEngine(Opt,Temp,Axioms,Formula,bliksem):-
35 option(Opt,bliksem),
36 access_file('ext/bin/bliksem',execute), !,
37 atom_concat(Temp,'/bliksem.in',InFile),
38 open(InFile,write,Stream),
39 fol2bliksem(Axioms,not(Formula),Stream),
40 close(Stream).
41
42initEngine(Opt,Temp,Axioms,Formula,mace):-
43 option(Opt,mace),
44 access_file('ext/bin/mace',execute), !,
45 atom_concat(Temp,'/mace.in',InFile),
46 open(InFile,write,Stream),
47 fol2mace(Axioms,Formula,Stream),
48 close(Stream).
49
50initEngine(Opt,Temp,Axioms,Formula,paradox):-
51 option(Opt,paradox),
52 access_file('ext/bin/paradox',execute), !,
53 atom_concat(Temp,'/paradox.in',InFile),
54 open(InFile,write,Stream),
55 fol2tptp(Axioms,not(Formula),Stream),
56 close(Stream).
57
58initEngine(Opt,_,_,_,_):-
59 option(Opt,X),
60 error('inference engine ext/bin/~p not accessible',[X]),
61 !, fail.
62
63
67
68timeLimit(TimeLim):-
69 option('--timelim',TimeLim),
70 access_file('ext/bin/CPULimitedRun',execute), !.
71
72timeLimit(0).
73
74
78
79callTPandMB(Dir,Axioms,TPProblem,MBProblem,MinDom,MaxDom,Model,Engine):-
80 timeLimit(TimeLim),
81 initEngine('--tp',Dir,Axioms,TPProblem,TP),
82 initEngine('--mb',Dir,Axioms,MBProblem,MB),
83 atomic_list_concat(['perl ./src/prolog/nutcracker/startTPandMB.pl ',
84 Dir,' ',TimeLim,' ',MinDom,' ',MaxDom,' ',TP,MB],Shell),
85 shell(Shell,Return), Return = 0,
86 readResult(Model,Dir,Engine).
87
88
92
93callMBbis(_,_,_,Model,Model,Engine,Engine):-
94 option('--mbbis',none), !.
95
96callMBbis(Dir,Axioms,MBProblem,FirstModel,Model,FirstEngine,Engine):-
97 FirstModel = model(Dom,_), length(Dom,DomSize), DomSize > 0,
98 timeLimit(TimeLim),
99 initEngine('--mbbis',Dir,Axioms,MBProblem,MB),
100 atomic_list_concat(['perl ./src/prolog/nutcracker/startTPandMB.pl ',
101 Dir,' ',TimeLim,' ',DomSize,' ',DomSize,' ',MB],Shell),
102 shell(Shell,Return), Return = 0,
103 readResult(SecondModel,Dir,SecondEngine), !,
104 ( SecondModel = unknown, Model = FirstModel, Engine = FirstEngine, !
105 ; Model = SecondModel, Engine = SecondEngine ).
106
107callMBbis(_,_,_,Model,Model,Engine,Engine).
108
109
113
114readResult(Model,Temp,Engine):-
115 atom_concat(Temp,'/tpmb.out',File),
116 open(File,read,Out),
117 read(Out,Result),
118 (
119 Result=proof, !,
120 read(Out,engine(Engine)),
121 Model=model([],[])
122 ;
123 Result=interpretation(_,_), !,
124 read(Out,engine(Engine)),
125 mace2blackburnbos(Result,Model)
126 ;
127 Result=paradox(_), !,
128 read(Out,engine(Engine)),
129 paradox2blackburnbos(Result,Model)
130 ;
131 Model=unknown,
132 Engine=unknown
133 ),
134 close(Out).
135
136
140
141paradox2blackburnbos(Paradox,model(D,F)):-
142 Paradox = paradox(Terms), \+ Terms=[],
143 paradox2d(Terms,[d1]-D),
144 paradox2f(Terms,[]-F).
145
146paradox2blackburnbos(Paradox,model([],[])):-
147 Paradox = paradox([]).
148
149paradox2blackburnbos(Paradox,unknown):-
150 \+ Paradox = paradox(_).
151
152
156
157paradox2d([],D-D).
158
159paradox2d([_Constant=Entity|L],D1-D2):-
160 \+ member(Entity,D1), !,
161 paradox2d(L,[Entity|D1]-D2).
162
163paradox2d([Symbol:1|L],D1-D2):-
164 functor(Symbol,Functor,1),
165 \+ Functor = '$',
166 arg(1,Symbol,Entity),
167 \+ member(Entity,D1), !,
168 paradox2d(L,[Entity|D1]-D2).
169
170paradox2d([Symbol:1|L],D1-D2):-
171 functor(Symbol,Functor,2),
172 \+ Functor = '$',
173 arg(1,Symbol,Entity1),
174 arg(2,Symbol,Entity2),
175 (
176 \+ member(Entity1,D1), !,
177 (
178 \+ member(Entity2,D2), !,
179 paradox2d(L,[Entity1,Entity2|D1]-D2)
180 ;
181 paradox2d(L,[Entity1|D1]-D2)
182 )
183 ;
184 \+ member(Entity2,D2),
185 paradox2d(L,[Entity2|D1]-D2)
186 ), !.
187
188paradox2d([_|L],D1-D2):-
189 paradox2d(L,D1-D2).
190
191
195
196paradox2f([],F-F).
197
198paradox2f([Constant=Entity|L],D1-D2):-
199 Term = f(0,Constant,Entity),
200 \+ member(Term,D1), !,
201 paradox2f(L,[Term|D1]-D2).
202
203paradox2f([Symbol:1|L],D1-D2):-
204 functor(Symbol,Functor,1),
205 \+ Functor = '$', !,
206 arg(1,Symbol,Arg),
207 (
208 select(f(1,Functor,E),D1,D3), !,
209 paradox2f(L,[f(1,Functor,[Arg|E])|D3]-D2)
210 ;
211 paradox2f(L,[f(1,Functor,[Arg])|D1]-D2)
212 ).
213
214paradox2f([Symbol:0|L],D1-D2):-
215 functor(Symbol,Functor,1),
216 \+ Functor = '$', !,
217 (
218 member(f(1,Functor,_),D1), !,
219 paradox2f(L,D1-D2)
220 ;
221 paradox2f(L,[f(1,Functor,[])|D1]-D2)
222 ).
223
224paradox2f([Symbol:1|L],D1-D2):-
225 functor(Symbol,Functor,2),
226 \+ Functor = '$', !,
227 arg(1,Symbol,Arg1),
228 arg(2,Symbol,Arg2),
229 (
230 select(f(2,Functor,E),D1,D3), !,
231 paradox2f(L,[f(2,Functor,[(Arg1,Arg2)|E])|D3]-D2)
232 ;
233 paradox2f(L,[f(2,Functor,[(Arg1,Arg2)])|D1]-D2)
234 ).
235
236paradox2f([Symbol:0|L],D1-D2):-
237 functor(Symbol,Functor,2),
238 \+ Functor = '$', !,
239 (
240 member(f(2,Functor,_),D1), !,
241 paradox2f(L,D1-D2)
242 ;
243 paradox2f(L,[f(2,Functor,[])|D1]-D2)
244 ).
245
246paradox2f([Symbol:1|L],D1-D2):-
247 functor(Symbol,Functor,3),
248 \+ Functor = '$', !,
249 arg(1,Symbol,Arg1),
250 arg(2,Symbol,Arg2),
251 arg(3,Symbol,Arg3),
252 (
253 select(f(3,Functor,E),D1,D3), !,
254 paradox2f(L,[f(3,Functor,[(Arg1,Arg2,Arg3)|E])|D3]-D2)
255 ;
256 paradox2f(L,[f(3,Functor,[(Arg1,Arg2,Arg3)])|D1]-D2)
257 ).
258
259paradox2f([Symbol:0|L],D1-D2):-
260 functor(Symbol,Functor,3),
261 \+ Functor = '$', !,
262 (
263 member(f(3,Functor,_),D1), !,
264 paradox2f(L,D1-D2)
265 ;
266 paradox2f(L,[f(3,Functor,[])|D1]-D2)
267 ).
268
269paradox2f([_|L],D1-D2):-
270 paradox2f(L,D1-D2).
271
272
276
277mace2blackburnbos(Mace,model(D,F)):-
278 Mace = interpretation(Size,Terms),
279 mace2d(1,Size,D),
280 mace2f(Terms,D,F).
281
282mace2blackburnbos(Mace,unknown):-
283 \+ Mace = interpretation(_Size,_Terms).
284
285
289
290mace2d(N,N,[V]):-
291 name(N,Codes),
292 name(V,[100|Codes]).
293
294mace2d(I,N,[V|D]):-
295 I < N,
296 name(I,Codes),
297 name(V,[100|Codes]),
298 J is I + 1,
299 mace2d(J,N,D).
300
301
305
306mace2f([],_,[]):- !.
307
308mace2f([function(Skolem,_)|Terms],D,F):-
309 \+ atom(Skolem), !,
310 mace2f(Terms,D,F).
311
312mace2f([function(Constant,[V])|Terms],D,[f(0,Constant,X)|F]):-
313 atom(Constant), !,
314 Index is V + 1,
315 name(Index,Codes),
316 name(X,[100|Codes]),
317 mace2f(Terms,D,F).
318
319mace2f([predicate(Relation,V)|Terms],D,[f(1,Functor,X)|F]):-
320 Relation =.. [Functor,_], !,
321 positiveValues(V,1,X),
322 mace2f(Terms,D,F).
323
324mace2f([predicate(Relation,V)|Terms],D,[f(2,Functor,X)|F]):-
325 Relation =.. [Functor,_,_], !,
326 length(D,Size),
327 positivePairValues(V,Size,1,1,X),
328 mace2f(Terms,D,F).
329
330mace2f([predicate(Relation,_V)|Terms],D,[f(3,Functor,X)|F]):-
331 Relation =.. [Functor,_,_,_], !,
334 X=[], 335 mace2f(Terms,D,F).
336
337mace2f([_|Terms],D,F):-
338 mace2f(Terms,D,F).
339
340
344
345positiveValues([],_,[]).
346
347positiveValues([1|Values],I1,[X|Rest]):-
348 name(I1,Codes),
349 name(X,[100|Codes]),
350 I2 is I1 + 1,
351 positiveValues(Values,I2,Rest).
352
353positiveValues([0|Values],I1,Rest):-
354 I2 is I1 + 1,
355 positiveValues(Values,I2,Rest).
356
357
361
362positivePairValues([],_,_,_,[]).
363
364positivePairValues([1|Values],Size,I1,J1,[(X2,X1)|Rest]):-
365 name(I1,Codes1),
366 name(X1,[100|Codes1]),
367 name(J1,Codes2),
368 name(X2,[100|Codes2]),
369 (
370 I1 < Size,
371 I2 is I1 + 1,
372 J2 is J1
373 ;
374 I1 = Size,
375 I2 = 1,
376 J2 is J1 + 1
377 ),
378 positivePairValues(Values,Size,I2,J2,Rest).
379
380positivePairValues([0|Values],Size,I1,J1,Rest):-
381 (
382 I1 < Size,
383 I2 is I1 + 1,
384 J2 is J1
385 ;
386 I1 = Size,
387 I2 = 1,
388 J2 is J1 + 1
389 ),
390 positivePairValues(Values,Size,I2,J2,Rest)