13:- module(mpred_pttp,[]). 15
16:- '$set_source_module'(baseKB). 17
18:- thread_local(t_l:disable_px/0). 19
21:- include(logicmoo('pfc2.0'/'mpred_header.pi')). 23
24ainz_pttp(A):-if_defined(mpred_ainz(A),assertz_new(A)).
28:- kb_shared(baseKB:wid/3). 29:- was_export(int_query/7). 30:- was_dynamic(int_query/7). 31:- was_export(int_not_query/7). 32:- was_dynamic(int_not_query/7). 33
35:- was_export(pttp_ask/1). 36pttp_ask(CALL):-nonegate(_KB,CALL,NNCALL),correct_pttp(NNCALL,REALCALL),apply(REALCALL,[ [], [], 100, _OneHundred, _Proof, [_In|[]]]).
37
39
64
66:- was_export(pttp_call/1). 67pttp_call(Goal) :- !,pttp_call(Goal,70,0,3,[],_,no).
68pttp_call(Goal,Max,Min,Inc,ProofIn,ProofOut,ShowProof):-
69 pttp_prove(Goal,Max,Min,Inc,ProofIn,ProofOut,ShowProof).
70
71
73:- was_export(pttp_load_wid/1). 74pttp_load_wid(Name):-must(pttp_logic(Name,Data)),!,must(pttp_load_wid(Name,Data)).
75:- was_export(pttp_load_wid/2). 76pttp_load_wid(Name,Data):- must(retractall_wid(Name)),wdmsg(pttp_load_wid(Name)),must(pttp_tell_wid(Name:0,Data)),!.
77uses_logic(Name):-pttp_logic(Name,Data),pttp_load_wid(Name,Data).
78
79
81:- was_export(pttp_assert/1). 82pttp_assert(X) :- must_pttp_id(ID),pttp_tell_wid(ID,X).
83
85:- was_export(pttp_tell_wid/2). 86pttp_tell_wid(ID,XY):-
87 with_no_mpred_expansions(
88 locally_tl(disable_px,
89 locally_tl(infSkipFullExpand,
90 must(pttp_assert_wid(ID,pttp,XY))))),!.
91
92:- was_export(pttp_assert_wid/3). 93pttp_assert_wid(ID,Mode,(X,Y)):- !, pttp_assert_wid(ID,Mode,X),kb_incr(ID,ID2), pttp_assert_wid(ID2,Mode,Y).
94pttp_assert_wid(ID,Mode,[X|Y]):- !, pttp_assert_wid(ID,Mode,X),kb_incr(ID,ID2), pttp_assert_wid(ID2,Mode,Y).
95pttp_assert_wid(ID,Mode,(call:-CALL)):-!,pttp_assert_wid(ID,Mode,(call(CALL))).
96pttp_assert_wid(_, _Mode,uses_logic(Name)):-!,must(pttp_logic(Name,Data)),!,must(pttp_load_wid(Name,Data)).
97pttp_assert_wid(ID,_Mode,kif(YY)):-!, must((numbervars(YY,'$VAR',7567,_),must(pttp_assert_wid(ID,kif,YY)))).
98pttp_assert_wid(ID,_Mode,call(CALL)):-!, must((save_wid(ID,call,call(CALL)),unnumbervars(CALL,RCALL),show_failure(why,must(RCALL)))).
99%pttp_assert_wid(ID,Mode,(query:-B)):- must(assertz_unumbered((query:-B))),PNF =(query:-B), must( pttp_nnf(PNF,X)),!,must(must(pttp_assert_real_wid(ID,X))).
100pttp_assert_wid(ID,pttp,X):- must(( \+ \+ (b_setval('$current_why',wp(ID,X),) must(( pttp1_wid(ID,X,Y), pttp2_wid(ID,Y)))))).
102pttp_assert_wid(ID,kif,X):- show_failure(why,must(kif_add_boxes1(ID,X))).
103
104pttp_assert_wid(ID,pttp_in,HB):- !,must((save_wid(ID,pttp_in,HB), pttp_assert_real_wid(ID,HB))).
105pttp_assert_wid(ID,Mode,(X:-Y)):- !,must((save_wid(ID,Mode,(X:-Y)), pttp_assert_real_wid(ID,(X:-Y)))).
106pttp_assert_wid(ID,_Mode,X):- show_failure(why,must(pttp_assert_real_wid(ID,X))),!.
107pttp_assert_wid(ID,_Mode,PNF):- must( pttp_nnf(PNF,X)),!,must(must(pttp_assert_real_wid(ID,X))).
108
109infer_by(_).
110
112:- was_export(pttp_assert_real_wid/2). 113pttp_assert_real_wid(ID,X):-
114 must( pttp1_wid(ID,X,Y)),!, must(pttp_assert_int_wid(ID,Y)),!.
115
116
118:- was_export(is_static_predicate_pttp/2). 119:- meta_predicate(is_static_predicate_pttp(0,?)). 120is_static_predicate_pttp(M:(Y:-_),Why):-!,is_static_predicate_pttp(M:Y,Why).
121is_static_predicate_pttp((Y:-_),Why):-!,is_static_predicate_pttp(Y,Why).
122is_static_predicate_pttp(_:Y,file(F)):-!,predicate_property(_:Y,file(F)),not(predicate_property(_:Y,dynamic)).
123is_static_predicate_pttp(Y,file(F)):-predicate_property(_:Y,file(F)),not(predicate_property(_:Y,dynamic)).
124
125
127:- was_export(pttp_assert_int_wid_for_conjuncts/3). 128:- meta_predicate(pttp_assert_int_wid_for_conjuncts(+,0,+)). 129pttp_assert_int_wid_for_conjuncts(ID,Y,_):- must(pttp_assert_int_wid(ID,Y)).
130
131
133:- was_export(save_wid/3). 134save_wid(IDWhy,Atom,Wff):-must(Atom\=','),to_numbered_ground(wid(IDWhy,Atom,Wff),Assert),show_failure(why,ainz_pttp(Assert)).
135
136to_numbered_ground(I,O):-ground(I)->I=O;(copy_term(I,M),numbervars(M,766,_,[functor_name('$VAR')]),O=M->true;trace_or_throw(to_numbered_ground(I,O))).
137
139clauses_wid(ID,ID:R,F,Y,Ref):-atomic(ID),!,nonvar(ID),clause_asserted(wid(ID:R,F,Y),true,Ref).
140clauses_wid(ID,ID,F,Y,Ref):- clause_asserted(wid(ID,F,Y),true,Ref).
141
142
144:- was_export(retract_if_no_wids/1). 145retract_if_no_wids(Y):- \+ wid(_,_,Y) -> retractall_matches(Y) ; true.
146
148:- was_export(is_wid_key/2). 149is_wid_key(Other,_):-compound(Other),not(not(is_wid_key2(Other))).
150 is_wid_key2(C:N):-number(N),!,(compound(C);atom(C)),!.
151 is_wid_key2(+N):-!,nonvar(N),!,is_wid_key2(N).
152 is_wid_key2(-N):-!,nonvar(N),!,is_wid_key2(N).
153 is_wid_key2(_:N):-!,nonvar(N),!,is_wid_key2(N).
154 is_wid_key2(N):-number(N),!.
155 is_wid_key2(N):-compound(N),!,N=..[_,A],!,number(A).
156
157
159erase_safe_pttp(_,Ref):-erase(Ref).
160
162retractall_matches(Y):-unnumbervars(Y,YY),retractall_matches_0(YY).
163retractall_matches_0((Y:-B)):-!,pred_subst(is_wid_key,B,_,_,BB),forall(clause(Y,BB,Ref),erase_safe_pttp(clause(Y,BB,Ref),Ref)).
164retractall_matches_0(Y):-forall(clause(Y,true,Ref),erase_safe_pttp(clause(Y,true,Ref),Ref)).
165
167:- was_export(retractall_wid/1). 168retractall_wid(ID):-
169 forall(clauses_wid(ID,A,B/C,Y,Ref),must(show_failure(why,(erase_safe_pttp(clauses_wid(ID,A,B/C,Y,Ref),Ref),retract_if_no_wids(Y))))),
170 forall(clauses_wid(ID,A,B,Y,Ref),must(erase_safe_pttp(clauses_wid(ID,A,B,Y,Ref),Ref))).
171
173:- was_export(listing_wid/1). 174:- was_export(listing_wid/0). 175listing_wid:- listing_wid(_).
176listing_wid(ID):- forall(((no_repeats(RID,clauses_wid(ID,RID,_,_,_)))),write_rid(RID)).
177
179:- was_export(write_rid/1). 180write_rid(RID):-
181((nl,write('%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% '),nl,write('% '),
182 write(RID),nl,
183 write('%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n '),nl)),!,
184 forall(((clauses_wid(RID,RID,Atomic,Wff,_),
185 Atomic\=pttp_nnf,atomic(Atomic))),
186 (write('% '),write(Atomic), write(': '), ansicall(green,portray_clause_0( Wff )),nl)),
187 forall(no_repeats(FY,(clauses_wid(RID,RID,NA,FY,_),compound(NA))),
188 show_wid_int(FY)).
189
190:- style_check(+singleton). 191
192show_wid_int(FY):-once((reassemble_intified(FY,FYI),renumbervars_a(FYI,FY2),unnumbervars(FY2,FY3), portray_clause_0( FY3 ),nl)).
193
194reassemble_intified(H :- B, OUT ):-
195 H=..HEADL,append(HARGS,[_G, _E, _A, _M, _F, _O, _D],HEADL),
196 grab_body(B,BOD), FHARGS=..HARGS,
197 OUT = (FHARGS :- BOD),!.
198reassemble_intified(H, FHARGS ):-compound(H),H=..HEADL,append(HARGS,[_G, _E, _A, _M, _F, _O, _D],HEADL), FHARGS=..HARGS,!.
199reassemble_intified(OUT,OUT).
200
201grab_body(call_proof(_,A),A):-!.
202grab_body((A,B),AB):-grab_body(A,AA),grab_body(B,BB),conjoin_pttp(AA,BB,AB).
203grab_body(_,true).
204
205:- was_export(portray_clause_0/1). 206portray_clause_0( Cmp ):- compound(Cmp),call(=,Cmp,(AA:-BB)),!, renumbervars_prev((AA:-BB) ,(A:-B) ),call(=,NV,(A:-B)),
207 current_output(Out),portray_clause(Out,NV,[numbervars(true)]).
208portray_clause_0( (A;B)):- writeq((A;B)),nl,!.
209portray_clause_0( AB ):- current_output(Out),portray_clause(Out,(AB),[numbervars(true)]).
210
211
212
214:- was_export(clear_pttp/0). 215clear_pttp:-
216 eraseall(int_query,_),eraseall(int_not_query,_),
217 forall(wid(ID,_/_,_),retractall(wid(ID,_,_))),
218 forall(was_pttp_functor(internal,F,A),(abolish(F,A),dynamic(F/A))).
219
222
223:- kb_shared(pttp_test/2). 224:- kb_shared(pttp_logic/2). 225
226
228:- dynamic(pttp_test_took/3). 229
230:- export(do_pttp_test_maybe/1). 231:- kb_shared(pttp_test_fails_is_ok/1). 232:- export(do_pttp_test_maybe/2). 233
234do_pttp_test_maybe(TestName):- forall(pttp_test(TestName,Data),do_pttp_test_maybe(TestName,Data)),listing(pttp_test_took).
235do_pttp_test_maybe(TestName,_) :- pttp_test_fails_is_ok(TestName),!.
236do_pttp_test_maybe(TestName,Data) :- do_pttp_test(TestName,Data).
237
238:- was_export(do_pttp_test/1). 239do_pttp_test(TestName):- forall(pttp_test(TestName,Data),do_pttp_test(TestName,Data)),listing(pttp_test_took).
240:- was_export(do_pttp_test/2). 241do_pttp_test(TestName,Data) :-
242 call_cleanup((
243 catch((
244 clear_pttp,
245 must_det_l((
246 dmsg(do_pttp_test(TestName)),
247 retractall_wid(TestName),
248 eraseall(int_query,_),eraseall(int_not_firstOrder,_),eraseall(int_firstOrder,_),
249 pttp_tell_wid(TestName:0,Data),
250 once((ignore(call_print_tf(pttp_test_prove(TestName,query))))),
251 sleep(1)))),E,dmsg(error(TestName:E)))),retractall_wid(TestName)).
252
253
255:- was_export(pttp_test_prove/2). 256pttp_test_prove(TestName,_):- pttp_test_query(TestName,Other),!,call30timed(TestName,Other).
257pttp_test_prove(TestName,A):- call30timed(TestName,pttp_prove(A)).
258
259:- meta_predicate call30timed(*,0). 260call30timed(TestName,CALL):-
261 statistics(cputime, D),
262 ( CALL 263 -> B=success
264 ; B=failure
265 ),
266 statistics(cputime, C),
267 F is C-D,
268 ainz_pttp(pttp_test_took(TestName,B,F)),!,
269 B=success.
270
271
272:- was_export(call_print_tf/1). 273:- meta_predicate(call_print_tf(0)). 274call_print_tf(G):-(G *-> dmsg(succceeded(G)) ; (dmsg(warning(error(failed_finally(G)))),sleep(5))).
275
276:- was_export(do_pttp_tests/0). 277do_pttp_tests :- do_pttp_test_maybe(_),
278 forall(pttp_test_took(Test, failure, _Time),gripe_pttp_failure(Test)).
279
280gripe_pttp_failure(Test):- pttp_test_fails_is_ok(Test),!.
281gripe_pttp_failure(Test):- dmsg(gripe_pttp_failure(Test)),!.
282gripe_pttp_failure(Test):- ignore(pttp_test_took(Test, failure, Time)),trace_or_throw(pttp_test_took(Test, failure, Time)).
283
284:- kb_shared(baseKB:sanity_test/0). 286
287
288:- was_export(isNegOf/2). 289isNegOf(N1,N):-number(N),!,N1 is -N.
290isNegOf(N,-N):-is_ftNonvar(N),!.
291isNegOf(-N,N):-is_ftNonvar(N),!.
292isNegOf(N1,N):-dtrace(not(isNegOf(N1,N))),isNegOf(N,N1).
293
294
295
296:- kb_shared(was_pttp_functor/3). 297
298
299
301
302
303was_pttp_functor(internal, query,7).
304
305
307int_listing_wid0:-
308 forall(was_pttp_functor(external,F,A),catch(prolog_list:listing(F/A),_,fail)),
309 forall(was_pttp_functor(internal,F,A),catch(prolog_list:listing(F/A),_,fail)),!.
310
311int_listing_wid:-
312 forall(was_pttp_functor(external,F,A),(functor(P,F,A),forall(clause(P,B),portray_clause_0((P:-B))))),
313 forall(was_pttp_functor(internal,F,A),(functor(P,F,A),forall(clause(P,B),portray_clause_0((P:-B))))).
314
315:- thread_local(is_query_functor/1). 316must_pttp_id(ID):- must(nb_current('$current_why',wp(ID,_))).
317is_query_lit(Q):- functor(Q,F,_),atom_concat('quer',_,F).
318
319get_int_query(Int_query):- is_query_functor(X),!, atom_concat('int_',X,Int_query).
320get_int_query(int_query).
321
322:- was_export(pttp_query/1). 323pttp_query(X) :- must_pttp_id(ID),pttp_query_wid(ID,X).
324:- was_export(pttp_query_wid/2). 325pttp_query_wid(ID, Y):- dtrace,pttp_tell_wid(ID,(query:-Y)), pttp_test_prove(ID,query),!.
326
334
336
337
338renumbervars_a(In,Out):-renumbervars_prev(In,Out),!.
339
340:- was_export(assertz_unumbered/1). 341
342assertz_unumbered(B,_):-assertz_unumbered(B).
343
344assertz_unumbered(B):-is_ftVar(B),trace_or_throw(var_assertz_unumbered(B)).
345assertz_unumbered(true):-!.
346assertz_unumbered(_:true):-!.
349assertz_unumbered(:-(B)):- !, show_call(why,must(B)),!.
350assertz_unumbered(B):- t_l:current_pttp_db_oper(OP),!, must((unnumbervars(B,BB),show_failure(why,call(OP,BB)))).
351assertz_unumbered(B):-must((unnumbervars(B,BB),show_failure(why,ainz_pttp(BB)))).
352
353:- was_export(add_functor/2). 354add_functor(Ext,F/A):- must(( export(F/A),ainz_pttp(was_pttp_functor(Ext,F,A)))).
355
356
357pttp_tell(Wff):- why_to_id(pttp_tell,Wff,Why),pttp_assert_int_wid(Why,Wff).
358
359
363:- was_export(pttp_assert_int/1). 364pttp_assert_int(Y):- must_pttp_id(ID),pttp_assert_int_wid(ID,Y).
365:- was_export(pttp_assert_int_wid/2). 366:- meta_predicate(pttp_assert_int_wid(+,+)). 367
368
369pttp_assert_int_wid(ID,Var):-is_ftVar(Var),trace_or_throw(var_pttp_assert_int_wid(ID,Var)).
370pttp_assert_int_wid(_ID,true):-!.
371pttp_assert_int_wid(ID,[H|B]):-!,pttp_assert_int_wid(ID,H),!,pttp_assert_int_wid(ID,B),!.
372pttp_assert_int_wid(ID,(H,B)):-!,pttp_assert_int_wid(ID,H),!,pttp_assert_int_wid(ID,B),!.
373pttp_assert_int_wid(ID,_:L):-!, pttp_assert_int_wid(ID,L).
374pttp_assert_int_wid(ID,YB):- must((get_functor(YB,F,A),renumbervars_a(YB,Y),pttp_assert_int_wid04(ID,Y,F,A),assertz_unumbered(Y))).
375
376
377:- meta_predicate pttp_assert_int_wid04(*,0,*,*). 378
379pttp_assert_int_wid04(_,Y,_,_):- is_static_predicate_pttp(Y,Why),must( dmsg(error(warn(is_static_predicate_pttp(Y,Why))))),!.
380pttp_assert_int_wid04(_,_,F,A):- was_pttp_functor(external,F,A),!.
381pttp_assert_int_wid04(_,Y,F,A):- not(internal_functor(F)),add_functor(external,F/A),assertz_unumbered(Y),!.
382pttp_assert_int_wid04(ID,Y,F,A):- show_success(why,wid(ID,F/A,Y)),!.
384pttp_assert_int_wid04(ID,Y,F,A):- wid(_,_,Y),!,ainz_pttp(wid(ID,F/A,Y)),!.
385pttp_assert_int_wid04(ID,Y,F,A):- ainz_pttp(wid(ID,F/A,Y)),add_functor(internal,F/A),!,assertz_unumbered(Y),!.
392
393:- ensure_loaded(dbase_i_mpred_pttp_statics). 394:- ensure_loaded(dbase_i_mpred_pttp_precompiled). 395:- ensure_loaded(dbase_i_mpred_pttp_testing). 396
397:- ensure_loaded(dbase_i_mpred_pttp_compile_stickel_orig). 398
399:- fixup_exports. 400
401:- if_startup_script(do_pttp_tests).