1:- if(( ( \+ ((current_prolog_flag(logicmoo_include,Call),Call))) )). 2:- module(mpred_pttp_compile,[]). 3:- endif. 4
5:- abolish(pttp_prove,6). 6:- abolish(search_cost,3). 7:- abolish(search,6). 8:- abolish(make_wrapper,3). 9:- abolish(add_features,2). 10:- abolish(add_args,13). 11
12
49
50:- abolish(pttp_prove,6). 51pttp_prove(Goal,Max,Min,Inc,ProofIn,ProofOut):-dalit_prove(Goal,Max,Min,Inc,ProofIn,ProofOut).
52
53dalit_prove(Goal,Max,Min,Inc,ProofIn,ProofOut) :-
54 expand_input_proof(ProofIn,PrfEnd),
55 PrevInc is Min + 1,
56 dalit_add_args(INFO,Goal,_,_,[],_,_,[],[],DepthIn,[PrfEnd|PrfEnd],ProofOut1,Goal1,_),
57 !,
58 timed_call(dalit_search(Goal1,Max,Min,Inc,PrevInc,DepthIn),'Proof'),
59 contract_output_proof(ProofOut1,ProofOut),
60 write_proof(ProofOut1),
61 nl.
62
63dalit_prove(Goal,Max,Min,Inc,ProofIn) :-
64 dalit_prove(Goal,Max,Min,Inc,ProofIn,_).
65
66dalit_prove(Goal,Max,Min,Inc) :-
67 dalit_prove(Goal,Max,Min,Inc,[],_).
68
69dalit_prove(Goal,Max,Min) :-
70 dalit_prove(Goal,Max,Min,1,[],_).
71
72dalit_prove(Goal,Max) :-
73 dalit_prove(Goal,Max,0,1,[],_).
74
75dalit_prove(Goal) :-
76 dalit_prove(Goal,10000,0,1,[],_).
77
78:- abolish(search_cost,3). 79search_cost(Body,HeadArgs,N):-dalit_search_cost(Body,HeadArgs,N).
80dalit_search_cost(Body,HeadArgs,N) :-
81 Body = dalit_search_cost(M) ->
82 N = M;
83 Body = (A , B) ->
84 (A = dalit_search_cost(M) -> 85 N = M; 86 87 dalit_search_cost(A,HeadArgs,N1),
88 dalit_search_cost(B,HeadArgs,N2),
89 max(N1,N2,N));
90 Body = (A ; B) ->
91 dalit_search_cost(A,HeadArgs,N1),
92 dalit_search_cost(B,HeadArgs,N2),
93 min(N1,N2,N);
94 pttp_builtin(Body) ->
95 N = 0;
96 97 N = 1.
98
99:- abolish(search,6). 100search(Goal,Max,Min,Inc,PrevInc,DepthIn):-dalit_search(Goal,Max,Min,Inc,PrevInc,DepthIn).
101
102dalit_search(_Goal,Max,Min,_Inc,_PrevInc,_DepthIn) :-
103 Min > Max,
104 !,
105 fail.
106dalit_search(Goal,_Max,Min,_Inc,PrevInc,DepthIn) :-
107 write_search_progress(Min),
108 DepthIn = Min,
109 call(Goal),
110 true. 111dalit_search(Goal,Max,Min,Inc,_PrevInc,DepthIn) :-
112 Min1 is Min + Inc,
113 dalit_search(Goal,Max,Min1,Inc,Inc,DepthIn).
114
115:- abolish(make_wrapper,3). 116make_wrapper(Body,HeadArgs,N):-dalit_make_wrapper(Body,HeadArgs,N).
117
118dalit_make_wrapper(_DefinedPreds,[query,0],true) :-
119 !.
120dalit_make_wrapper(DefinedPreds,[P,N],Result) :-
121 functor(Goal,P,N),
122 Goal =.. [P|Args],
123 ExtraArgs = [PosAncestors,NegAncestors,DepthIn,ProofIn,ProofOut],
124 list_append(Args,ExtraArgs,Args1),
125 Head =.. [P|Args1],
126 internal_functor(P,IntP),
127 list_length_pttp(ExtraArgs,NExtraArgs),
128 NN is N + NExtraArgs + 1,
129 (identical_member_special([IntP,NN],DefinedPreds) ->
130 list_append(ExtraArgs,[GoalAtom],ExtraArgs2),
131 list_append(Args,ExtraArgs2,Args2),
132 IntHead =.. [IntP|Args2];
133 134 IntHead = fail),
135 (is_negative_functor(P) ->
136 negated_literal(Goal,PosGoal),
137 Red = redn, 138 C1Ancestors = NegAncestors,
139 C2Ancestors = PosAncestors;
140 141 PosGoal = Goal,
142 Red = red,
143 C1Ancestors = PosAncestors,
144 C2Ancestors = NegAncestors),
145 (N = 0 -> 146 V1 = (identical_member_special(GoalAtom,C2Ancestors) , !);
147 148 V1 = ((identical_member_special(GoalAtom,C2Ancestors) , !);
149 unifiable_member(GoalAtom,C2Ancestors))),
150 V2 = (
151 ProofIn = [Prf,[Red,GoalAtom,PosAncestors,NegAncestors]|PrfEnd],
152 ProofOut = [Prf|PrfEnd]),
153 conjoin_pttp(V1,V2,Reduce),
154 Result = (Head :- GoalAtom = PosGoal,
155 (identical_member_special_loop_check(GoalAtom,C1Ancestors) ->
156 fail;
157 158 (Reduce;
159 IntHead))).
160
161query(PosAncestors,NegAncestors,DepthIn,ProofIn,ProofOut) :-
162 int_query(PosAncestors,NegAncestors,DepthIn,ProofIn,ProofOut,query).
163
164:- abolish(add_features,2). 165add_features(A,B):-dalit_add_features(A,B).
166
167dalit_add_features((Head :- Body),(Head1 :- Body1)) :-
168 (functor(Head,query,_) ->
169 Head2 = Head,
170 dalit_add_args(INFO,Body,yes,query,[],
171 PosAncestors,NegAncestors,
172 PosAncestors,NegAncestors,
173 DepthIn,
174 ProofIn,ProofOut,
175 Body1,_);
176 177 linearize(Head,Head2,[],_,true,Matches),
178 (is_negative_literal(Head) ->
179 PosGoal = no;
180 181 PosGoal = yes),
182 Head =.. [_|HeadArgs],
183 dalit_add_args(INFO,Body,PosGoal,GoalAtom,HeadArgs,
184 PosAncestors,NegAncestors,
185 NewPosAncestors,NewNegAncestors,
186 Depth1,
187 ProofIn,ProofOut,
188 Body2,New),
189 (is_ftVar(New) ->
190 PushAnc = true;
191 PosGoal = yes ->
192 NewNegAncestors = NegAncestors,
193 PushAnc = (NewPosAncestors = [GoalAtom|PosAncestors]);
194 195 NewPosAncestors = PosAncestors,
196 PushAnc = (NewNegAncestors = [GoalAtom|NegAncestors])),
197 dalit_search_cost(Body,HeadArgs,Cost),
198 test_and_decrement_search_cost_expr(DepthIn,Cost,Depth1,TestExp),
199 conjoin_pttp(PushAnc,Body2,Body4),
200 conjoin_pttp(Matches,Body4,Body5),
201 conjoin_pttp(TestExp,Body5,Body1)),
202 Head2 =.. [P|L],
203 internal_functor(P,IntP),
204 list_append(L,[PosAncestors,NegAncestors,
205 DepthIn,
206 ProofIn,ProofOut,
207 GoalAtom],
208 L1),
209 Head1 =.. [IntP|L1].
210
211:- abolish(add_args,13). 212
213add_args(INFO,Body,PosGoal,GoalAtom,HeadArgs,
214 PosAncestors,NegAncestors,
215 NewPosAncestors,NewNegAncestors,
216 DepthIn,
217 ProofIn,ProofOut,
218 Body1,New):-
219 dalit_add_args(INFO,Body,PosGoal,GoalAtom,HeadArgs,
220 PosAncestors,NegAncestors,
221 NewPosAncestors,NewNegAncestors,
222 DepthIn,
223 ProofIn,ProofOut,
224 Body1,New).
225
226dalit_add_args(INFO,Body,PosGoal,GoalAtom,HeadArgs,
227 PosAncestors,NegAncestors,
228 NewPosAncestors,NewNegAncestors,
229 DepthIn,
230 ProofIn,ProofOut,
231 Body1,New) :-
232 Body = (A , B) ->
233 dalit_add_args(INFO,A,PosGoal,GoalAtom,HeadArgs,
234 PosAncestors,NegAncestors,
235 NewPosAncestors,NewNegAncestors,
236 DepthIn,
237 ProofIn,Proof1,
238 A1,New),
239 dalit_add_args(INFO,B,PosGoal,GoalAtom,HeadArgs,
240 PosAncestors,NegAncestors,
241 NewPosAncestors,NewNegAncestors,
242 DepthIn,
243 Proof1,ProofOut,
244 B1,New),
245 conjoin_pttp(A1,B1,Body1);
246 Body = (A ; B) ->
247 throw(unimplemented);
248 functor(Body,dalit_search_cost,_) ->
249 ProofOut = ProofIn,
250 Body1 = true;
251 Body = infer_by(N) ->
252 (PosGoal = yes ->
253 N1 = N;
254 255 isNegOf(N1,N)),
256 Body1 = (ProofIn = [Prf,[N1,GoalAtom,PosAncestors,NegAncestors]|PrfEnd],
257 ProofOut = [Prf|PrfEnd]);
258 Body = dalit_search_cost(N) ->
259 ProofOut = ProofIn,
260 Body1 = true;
261 pttp_builtin(Body) ->
262 ProofOut = ProofIn,
263 Body1 = Body;
264 265 Body =.. L,
266 list_append(L,
267 [NewPosAncestors,NewNegAncestors,
268 DepthIn,
269 ProofIn,ProofOut],
270 L1),
271 Body1 =.. L1,
272 New = yes.
274
275:- fixup_exports.