12
13:-module(ics_quant,
14 [quantify_variables_in_ics/2,
15 ics_scan_head/3, adjust_variable_list/2]). 16
17:-use_module(quantif). 18
19:-use_module(library(lists)). 20
21:-use_module(library(terms),
22 [term_variables/2]). 23
24:- use_module(solver). 25
26operator(700,xfx,ne).
27
86
97
98
99quantify_variables_in_ics(ICS,ICS1):-
100 ics_variables(ICS,ics(Body,Head),Variables),
101 quantify_variables(Variables),
102 split_body(Body,Body1),
103 shuffle_head(Head,Head1),
104 ICS1=ics(Body1,Head1).
105
106ics_variables(ics(Body,Head),ics(Body,Head1),Variables):-
107 ics_scan_body(Body,[],BodyVariables),
108 ics_scan_head(Head,BodyVariables,ICSVariables),
109 adjust_variable_list(ICSVariables,RepeatedVariables),
110 modify_head(RepeatedVariables,Head,Head1,Variables).
111
112quantify_variables([]).
113quantify_variables([Variable|MoreVariables]):-
114 decide_variable_quantification(Variable,Quantification),
115 attach_variable_quantification(Variable,Quantification),
116 quantify_variables(MoreVariables).
117
118
119attach_variable_quantification(variable(VarName,_),Quantification):-
120 (get_quant(VarName,_)
121 -> true
122 ; quant(VarName,Quantification)).
123
126split_body([],[[],[],[],[],[],[],[],[]]).
127split_body([h(Event,Time)|MoreAtoms],
128 [[h(Event,Time)|More],NH,E,NE,EN,NEN,ABD,O]):-
129 !,
130 split_body(MoreAtoms,[More,NH,E,NE,EN,NEN,ABD,O]).
131split_body([noth(Event,Time)|MoreAtoms],
132 [H,[noth(Event,Time)|More],E,NE,EN,NEN,ABD,O]):-
133 !,
134 split_body(MoreAtoms,[H,More,E,NE,EN,NEN,ABD,O]).
135split_body([e(Event,Time)|MoreAtoms],
136 [H,NH,[e(Event,Time)|More],NE,EN,NEN,ABD,O]):-
137 !,
138 split_body(MoreAtoms,[H,NH,More,NE,EN,NEN,ABD,O]).
139split_body([note(Event,Time)|MoreAtoms],
140 [H,NH,E,[note(Event,Time)|More],EN,NEN,ABD,O]):-
141 !,
142 split_body(MoreAtoms,[H,NH,E,More,EN,NEN,ABD,O]).
143split_body([en(Event,Time)|MoreAtoms],
144 [H,NH,E,NE,[en(Event,Time)|More],NEN,ABD,O]):-
145 !,
146 split_body(MoreAtoms,[H,NH,E,NE,More,NEN,ABD,O]).
147split_body([noten(Event,Time)|MoreAtoms],
148 [H,NH,E,NE,EN,[noten(Event,Time)|More],ABD,O]):-
149 !,
150 split_body(MoreAtoms,[H,NH,E,NE,EN,More,ABD,O]).
151split_body([abd(Event,Time)|MoreAtoms],
152 [H,NH,E,NE,EN,NEN,[abd(Event,Time)|More],O]):-
153 !,
154 split_body(MoreAtoms,[H,NH,E,NE,EN,NEN,More,O]).
155split_body([Atom|MoreAtoms],
156 [H,NH,E,NE,EN,NEN,ABD,[Constraint|More]]):-
157 rewrite_constraint(Atom,Constraint1),
158 !,
159 check_if_restriction(Constraint1,Constraint),
160 split_body(MoreAtoms,[H,NH,E,NE,EN,NEN,ABD,More]).
161split_body([Atom|MoreAtoms],
162 [H,NH,E,NE,EN,NEN,ABD,[Atom|More]]):-
163 split_body(MoreAtoms,[H,NH,E,NE,EN,NEN,ABD,More]).
206
207
208
209shuffle_head([],[]).
210shuffle_head([Disjunct|MoreDisjuncts],
211 [ShuffledDisjunct|MoreShuffledDisjuncts]):-
212 shuffle_disjunct(Disjunct,ShuffledDisjunct),
213 shuffle_head(MoreDisjuncts,MoreShuffledDisjuncts).
214
215shuffle_disjunct(Disjunct,ShuffledDisjunct):-
216 modify_conjuncts(Disjunct,KeyedDisjunct),
217 keysort(KeyedDisjunct,SortedDisjunct),
218 remove_keys(SortedDisjunct,ShuffledDisjunct).
219
220remove_keys([],[]).
221remove_keys([_-V|KMore],[V|More]):-
222 remove_keys(KMore,More).
223
224modify_conjuncts([],[]).
225modify_conjuncts([Conjunct|MoreConjuncts],
226 [ModifiedConjunct|MoreModifiedConjuncts]):-
227 modify_conjunct(Conjunct,ModifiedConjunct),
228 modify_conjuncts(MoreConjuncts,MoreModifiedConjuncts).
229
230modify_conjunct(Conjunct,1-Conjunct):-
231 is_abducible(Conjunct),
232 !.
233modify_conjunct(Conjunct,0-Constraint):-
234 rewrite_constraint(Conjunct,Constraint1),
235 !,
236 check_if_restriction(Constraint1,Constraint).
237
238modify_conjunct(Conjunct,2-Conjunct).
239
240is_abducible(Conjunct):-
241 functor(Conjunct,F,N),
242 abducible_signature(F,N).
243
244abducible_signature(e,2).
245abducible_signature(en,2).
246abducible_signature(note,2).
247abducible_signature(noten,2).
248abducible_signature(abd,2).
249
253rewrite_constraint(clp_constraint(C),clp_constraint(C)):- !.
254
255rewrite_constraint(unif(A,B),clp_constraint(reif_unify(A,B,1))):-
256 !.
257rewrite_constraint(not_unif(A,B), clp_constraint(reif_unify(A,B,0))):-
258 !.
259rewrite_constraint(Constraint,clp_constraint(Constraint1)):-
260 solver_rewrite_constraint(Constraint,Constraint1).
261
262
269check_if_restriction(clp_constraint(st(Arg1)),clp_constraint(st(Arg1))):- !.
270check_if_restriction(clp_constraint(st(Arg1, Arg2)),clp_constraint(st(Arg1, Arg2))) :- !.
271check_if_restriction(clp_constraint(Constraint1),clp_constraint(Constraint2)):-
272 only_universal_variables(Constraint1) ->
273 Constraint2=st(Constraint1);
274 Constraint2=Constraint1.
275
276
277
278
279
280
292
293only_universal_variables(Term):-
294 term_variables(Term,Variables),
295 all_universal(Variables).
296
297all_universal([Var|_]):-
298 is_existential(Var),
299 !,
300 fail.
301all_universal([_|MoreVars]):-
302 all_universal_1(MoreVars).
303
304all_universal_1([]).
305all_universal_1([Var|_]):-
306 is_existential(Var),
307 !,
308 fail.
309all_universal_1([_|MoreVars]):-
310 all_universal_1(MoreVars).
311
323
324modify_head(RepeatedVariables,Head,Head1,Variables):-
325 modify_head(RepeatedVariables,Head,Head1,[],Variables).
326
327modify_head([],Head,Head,Variables,Variables).
328
329modify_head([RVar|MoreRVars],OldHead,NewHead,OldVars,NewVars):-
330 var_modify_head(RVar,OldHead,IntHead,Vars),
331 append(OldVars,Vars,IntVars),
332 modify_head(MoreRVars,IntHead,NewHead,IntVars,NewVars).
333
334
335var_modify_head(Var,OldHead,NewHead,Vars):-
336 var_to_var_list(Var,Vars),
337 var_modify_head(Vars,OldHead,NewHead).
338
339var_modify_head([_],Head,Head):-
340 !.
341var_modify_head([variable(VarName,_)|MoreVars],OldHead,NewHead):-
342 replace_vars_in_head(MoreVars,VarName,OldHead,NewHead).
343
344replace_vars_in_head([],_,Head,Head).
345replace_vars_in_head([variable(RName,
346 [occur(head(Disjunct),_)|_])|MoreVars],
347 OName,OldHead,NewHead):-
348 replace_var_in_head(OldHead,1,Disjunct,OName,RName,IntHead),
349 replace_vars_in_head(MoreVars,OName,IntHead,NewHead).
350
351replace_var_in_head([Disjunct|MoreDisjuncts],N,N,OName,RName,
352 [NewDisjunct|MoreDisjuncts]):-
353 !,
354 replace(Disjunct,OName,RName,NewDisjunct).
355replace_var_in_head([Disjunct|MoreDisjuncts],M,N,OName,RName,
356 [Disjunct|MoreNewDisjuncts]):-
357 M1 is M+1,
358 replace_var_in_head(MoreDisjuncts,M1,N,OName,RName,
359 MoreNewDisjuncts).
360
361
377
378var_to_var_list(Variable,[Variable]):-
379 Variable=variable(_,[occur(body,_)|_]),
380 !.
381
382var_to_var_list(variable(VarName,OccurList),VarList):-
383 split_occurrence_list(OccurList,SplittedOccurList),
384 create_var_list(VarName,SplittedOccurList,VarList).
385
386
387split_occurrence_list([occur(head(N),Type)|MoreOccurs],
388 [[occur(head(N),Type)|MoreOccurs1]|MoreLists]):-
389 split_occurrence_list(MoreOccurs,N,[MoreOccurs1|MoreLists]).
390
391split_occurrence_list([],_,[[]]).
392split_occurrence_list([occur(head(N),Type)|MoreOccurs],N,
393 [[occur(head(N),Type)|MoreOccurs1]|MoreLists]):-
394 !,
395 split_occurrence_list(MoreOccurs,N,[MoreOccurs1|MoreLists]).
396split_occurrence_list([occur(head(N),Type)|MoreOccurs],_,
397 [[],[occur(head(N),Type)|MoreOccurs1]|MoreLists]):-
398 split_occurrence_list(MoreOccurs,N,[MoreOccurs1|MoreLists]).
399
400create_var_list(VarName,[OccurList|MoreOccurLists],
401 [variable(VarName,OccurList)|MoreVariables]):-
402 create_var_list(MoreOccurLists,MoreVariables).
403
404create_var_list([],[]).
405create_var_list([OccurList|MoreOccurLists],
406 [variable(_,OccurList)|MoreVariables]):-
407 create_var_list(MoreOccurLists,MoreVariables).
408
433
434ics_scan_body([],Variables,Variables).
435ics_scan_body([Conjunct|MoreConjuncts],OldVariables,NewVariables):-
436 conjunct_variables(Conjunct,body,ConjunctVariables),
437 append(OldVariables,ConjunctVariables,IntVariables),
438 ics_scan_body(MoreConjuncts,IntVariables,NewVariables).
439
440ics_scan_head(Head,OldVariables,NewVariables):-
441 ics_scan_head(Head,1,OldVariables,NewVariables).
442
443ics_scan_head([],_,Variables,Variables).
444ics_scan_head([Disjunct|MoreDisjuncts],DisjunctNumber,
445 OldVariables,NewVariables):-
446 ics_scan_disjunct(Disjunct,DisjunctNumber,
447 OldVariables,IntVariables),
448 NewDisjunctNumber is DisjunctNumber+1,
449 ics_scan_head(MoreDisjuncts,NewDisjunctNumber,
450 IntVariables,NewVariables).
451
452ics_scan_disjunct([],_,Variables,Variables).
453ics_scan_disjunct([Conjunct|MoreConjuncts],DisjunctNumber,
454 OldVariables,NewVariables):-
455 conjunct_variables(Conjunct,head(DisjunctNumber),ConjunctVariables),
456 append(OldVariables,ConjunctVariables,IntVariables),
457 ics_scan_disjunct(MoreConjuncts,DisjunctNumber,
458 IntVariables,NewVariables).
459
460conjunct_variables(Conjunct,Where,ConjunctVariables):-
461 Conjunct=..[Functor|_],
462 functor_type(Functor,Type),
463 term_variables(Conjunct,Variables),
464 build_variables_list(Variables,Where,Type,ConjunctVariables).
465
466build_variables_list([],_,_,[]).
467build_variables_list([Variable|MoreVariables],Where,Type,
468 [variable(Variable,Where,Type)|MoreVarStructs]):-
469 build_variables_list(MoreVariables,Where,Type,MoreVarStructs).
470
471functor_type(h,h):-
472 !.
473functor_type(noth,noth):-
474 !.
475functor_type(e,e):-
476 !.
477functor_type(note,note):-
478 !.
479functor_type(en,en):-
480 !.
481functor_type(noten,noten):-
482 !.
483functor_type(abd,abd):-
484 !.
485functor_type(C,clp_constraint):-
486 is_clp_functor(C),
487 !.
488functor_type(_,other).
489
490adjust_variable_list([],[]):-
491 !.
492adjust_variable_list(Variables,
493 [VarStruct|MoreVarStructs]):-
494 get_var_struct(Variables,VarStruct,Remaining),
495 adjust_variable_list(Remaining,MoreVarStructs).
496
497get_var_struct([variable(VarName,Where,Type)|MoreVariables],
498 variable(VarName,[occur(Where,Type)|MoreOccurs]),
499 Remaining):-
500 get_more_occurs(MoreVariables,VarName,MoreOccurs,Remaining).
501
502get_more_occurs([],_,[],[]).
503get_more_occurs([variable(VarName1,Where,Type)|MoreVariables],
504 VarName,[occur(Where,Type)|MoreOccurs],Remaining):-
505 VarName1==VarName,
506 !,
507 get_more_occurs(MoreVariables,VarName,MoreOccurs,Remaining).
508get_more_occurs([Variable|MoreVariables],VarName,Occurs,
509 [Variable|MoreRemaining]):-
510 get_more_occurs(MoreVariables,VarName,Occurs,MoreRemaining).
511
520
532decide_variable_quantification(variable(_,OccurList),forall):-
533 in_head_and_body(OccurList),
534 !.
535decide_variable_quantification(variable(_,OccurList),Quantification):-
536 first_in_head(OccurList),
537 !,
538 head_quantify(OccurList,Quantification).
539decide_variable_quantification(variable(_,OccurList),Quantification):-
540 body_quantify(OccurList,Quantification).
541illegal(variable(_,Occurrences)):-
542 only_in_others(Occurrences).
543
544only_in_others([]).
545only_in_others([occur(_,other)|MoreOccurrences]):-
546 only_in_others(MoreOccurrences).
547
548
549in_head_and_body([occur(body,_)|MoreOccurs]):-
550 in_head(MoreOccurs).
551
552in_head([occur(head(_),_)|_]):-
553 !.
554in_head([_|MoreOccurrences]):-
555 in_head(MoreOccurrences).
556
557first_in_head([occur(head(_),_)|_]).
558
559head_quantify(OccurList,exists):-
560 in_e_or_note_or_abd_or_other(OccurList),
561 !.
562head_quantify(_,forall).
563
564body_quantify(OccurList,forall):-
565 in_h(OccurList),
566 !.
567body_quantify(OccurList,forall):-
568 in_e_or_note_or_abd(OccurList),
569 !.
570body_quantify(OccurList,forall):-
571 only_in_other(OccurList),
572 !.
573body_quantify(_,exists).
574
575only_in_other([]).
576only_in_other([occur(_,other)|Tail]):-
577 only_in_other(Tail).
578only_in_other([occur(_,clp_constraint)|Tail]):-
579 only_in_other(Tail).
580
581in_e_or_note_or_abd([occur(_,e)|_]):-
582 !.
583in_e_or_note_or_abd([occur(_,note)|_]):-
584 !.
585in_e_or_note_or_abd([occur(_,abd)|_]):-
586 !.
587in_e_or_note_or_abd([_|MoreOccurrences]):-
588 in_e_or_note_or_abd(MoreOccurrences).
589
590
591in_e_or_note_or_abd_or_other([occur(_,e)|_]):-
592 !.
593in_e_or_note_or_abd_or_other([occur(_,note)|_]):-
594 !.
595in_e_or_note_or_abd_or_other([occur(_,abd)|_]):-
596 !.
597in_e_or_note_or_abd_or_other([occur(_,other)|_]):-
598 !.
599in_e_or_note_or_abd_or_other([_|MoreOccurrences]):-
600 in_e_or_note_or_abd_or_other(MoreOccurrences).
601
602
603
604in_h([occur(_,h)|_]):-
605 !.
606in_h([_|MoreOccurrences]):-
607 in_h(MoreOccurrences).
608
618
619replace(T,O,R,T1):-
620 compound(T),
621 !,
622 T=..[F|Args],
623 replace_list(Args,O,R,Args1),
624 T1=..[F|Args1].
625
626replace(T,X,Y,Y):-
627 T==X,
628 !.
629replace(T,_,_,T).
630
631replace_list([],_,_,[]).
632replace_list([H|T],O,R,[H1|T1]):-
633 replace(H,O,R,H1),
634 replace_list(T,O,R,T1)