1% MODULE var_utils EXPORTS 2:- module( var_utils, 3 [ inverse_substitute/2, 4 inverse_substitute1/2, 5 skolems/2, 6 7 skolemize/3, 8 skolemize/4, 9 deskolemize/3, 10 11 relevant_vars2/6, 12 relevant_vars3/6, 13 buildrelterms/6, 14 15 contains_vars/2, 16 flagged_contains_vars/3, 17 vars/2, 18 19 term_size/2, 20 21 replace/4, 22 inv_replace/4, 23 24 25 terms/3, 26 terms/4, 27 only_vars/2, 28 clause_terms/2, 29 only_vars1/2, 30 typed_only_vars1/2, 31 exists_intersect/3, 32 clean_subst/3, 33 findargs/3, 34 allarg/4]). 35 36% IMPORTS 37:- use_module(home(div_utils), 38 [effaceall/3,genterm_test/2,identical_member/2,mysetof/3, 39 clist_to_prolog/2,best/2,subterm_at_position/4,part_of_clause/2]). 40:- use_module(home(flatten), 41 [flatten_clause/2,unflatten_clause/2]). 42:- use_module(home(filter), 43 [truncate_unconnected/2]). 44:- use_module(home(lgg), 45 [lgg_terms/7]). 46:- use_module_if_exists(library(basics), 47 [member/2,nonmember/2,memberchk/2]). 48:- use_module_if_exists(library(sets), 49 [union/3,subtract/3,list_to_set/2,intersection/3]). 50:- use_module_if_exists(library(strings), 51 [gensym/2,string_append/3,substring/4]). 52:- use_module_if_exists(library(occurs), 53 [sub_term/2,contains_var/2]). 54:- use_module_if_exists(library(subsumes), 55 [variant/2]). 56 57 58% METAPREDICATES 59% none 60 61 62 63%*********************************************************************** 64%* 65%* module: var_utils.pl 66%* 67%* author: B.Jung, M.Mueller, I.Stahl, B.Tausend date:12/92 68%* 69%* changed: 70%* 71%* description: - utilities for variable and clause handling 72%* - determine relevant variables for predicate invention. 73%* - inverse_substitution 74%* - skolemization is a special substitution 75%* - replacement 76%* 77%* see also: 78%* 79%*********************************************************************** 80 81 82 83%*********************************************************************** 84%* 85%* predicate: vars/2 86%* 87%* syntax: vars(+Term,-Vars) 88%* 89%* args: Term: any prolog term 90%* Vars: list of variables in Term 91%* 92%* description: 93%* 94%* example: 95%* 96%* peculiarities: setof changed to mysetof (IS) 97%* 98%* 99%* see also: 100%* 101%*********************************************************************** 102 103vars(Term,Vars):- 104 mysetof(V, ( sub_term(V,Term), var(V) ), Vars). 105 106 107%*********************************************************************** 108%* 109%* predicate: clause_terms/2 110%* 111%* syntax: clause_terms(+Clause,-Termlist) 112%* 113%* args: 114%* 115%* description: returns list of all non-ground terms in Clause 116%* 117%* example: clause_terms((p(f(X),a,g(Y,b)):- r(f(X),Y)), 118%* [f(X),X,g(Y,b),Y]) 119%* 120%* peculiarities: none 121%* 122%* see also: 123%* 124%*********************************************************************** 125 126clause_terms((H:-B),L):- !, 127 functor(H,_,N), 128 terms(N,H,[],L0), 129 clause_terms(B,L0,L). 130clause_terms(H,L):- 131 functor(H,_,N), 132 terms(N,H,[],L). 133 134clause_terms((A,B),L,L2):- !, 135 clause_terms(A,L,L1), 136 clause_terms(B,L1,L2). 137clause_terms(A,L,L1):- 138 functor(A,_,N), 139 terms(N,A,L,L1). 140 141 142%*********************************************************************** 143%* 144%* predicate: terms/3,4 145%* 146%* syntax: terms(+Term,+Accu,-Accu) 147%* terms(+Count,+Term,+Accu,-Accu) 148%* 149%* args: 150%* 151%* description: returns all non-ground subterms within Term 152%* 153%* example: 154%* 155%* peculiarities: none 156%* 157%* see also: 158%* 159%*********************************************************************** 160 161terms(V,L,L1):- 162 var(V),!, 163 ( identical_member(V,L) -> 164 L1 = L 165 ; L1 = [V|L] 166 ). 167terms(T,L,L1):- 168 functor(T,_,N), 169 ( (ground(T); identical_member(T,L)) -> 170 L1 = L 171 ; terms(N,T,[T|L],L1) 172 ). 173 174terms(0,_,L,L):- !. 175terms(N,T,L,L2):- 176 N1 is N - 1, 177 terms(N1,T,L,L1), 178 arg(N,T,Tn), 179 terms(Tn,L1,L2). 180 181 182%*********************************************************************** 183%* 184%* predicate: only_vars/2 185%* 186%* syntax: only_vars(+Term,-Varlist) 187%* 188%* args: 189%* 190%* description: returns all variables within Term 191%* 192%* example: 193%* 194%* peculiarities: 195%* 196%* see also: 197%* 198%*********************************************************************** 199 200only_vars(T,L):- 201 terms(T,[],L1), 202 only_vars1(L1,L). 203 204only_vars1([],[]). 205only_vars1([X|R],[X|R1]):- 206 var(X),!, 207 only_vars1(R,R1). 208only_vars1([_|R],R1):- 209 only_vars1(R,R1). 210 211 212%*********************************************************************** 213%* 214%* predicate: typed_only_vars1/2 215%* 216%* syntax: typed_only_vars1(+TypedTermlist,-TypedVarlist) 217%* 218%* args: TypedTermlist: [T:typeT,...] 219%* Vars: [Var:typeVar 220%* 221%* description: extracts each term T that is a variable 222%* from a list TypedTermlist of terms with type definition 223%* 224%* example: only_vars2([X:type16,Y:type14,f(Z):type23],[X:type16,Y:type14]) 225%* 226%* peculiarities: none 227%* 228%* see also: 229%* 230%*********************************************************************** 231 232typed_only_vars1([],[]). 233typed_only_vars1([X:T|R],[X:T|R1]):- 234 var(X),!, 235 typed_only_vars1(R,R1). 236typed_only_vars1([_|R],R1):- 237 typed_only_vars1(R,R1). 238 239 240 241%*********************************************************************** 242%* 243%* predicate: replace/3 244%* 245%* syntax: replace(+C1,+S1,-C2,-S2) 246%* 247%* args: C1, C2: clauses in list notation 248%* S1, S2: replacements [ X / Term, .. ] 249%* If all X's are variables, this is actually a 250%* substitution, but we also allow other terms. 251%* 252%* description: C2 is a copy of C1 with S1 applied. 253%* S2 is a copy of S1. 254%* 255%* example: replace( [p(A,B):p], [A/a], [p(a,D):p], [C/a]). 256%* 257%* peculiarities: 258%* 259%* see also: 260%* 261%*********************************************************************** 262 263replace(C,S1,D,S2):- 264 copy_term( (C,S1) , (E,S2) ), 265 do_replace( E, S2, D). 266 267 268do_replace( [], _, []). 269 270do_replace( [ L|More], S, [L1|More1]):- 271 do_replace1( L, S, L1),!, 272 do_replace(More, S, More1). 273 274do_replace1( T1,S,T2 ):- 275 ( member( X/T, S), X==T1 -> T2 = T 276 ; 277 var(T1) -> T1 = T2 278 ; 279 functor( T1, F, N) -> functor(T2,F,N), do_replace1(N,T1,T2,S) 280 ). 281 282do_replace1(0,_,_,_). 283 284do_replace1(N,T1,T2,S):- 285 arg(N,T1,A), 286 arg(N,T2,B), 287 do_replace1(A,S,B), 288 M is N - 1, 289 do_replace1(M,T1,T2,S). 290 291 292 293 294%*********************************************************************** 295%* 296%* predicate: inv_replace/4 297%* 298%* syntax: inv_replace(+C1,+S1,-C2,-S2) 299%* 300%* args: C1, C2: clauses in list notation 301%* S1, S2: replacements [ X / Term, .. ] 302%* 303%* description: C2 is a copy of C1 with term of S1 replaced by ass. vars 304%* S2 is a copy of S1,s.t. vars(S2) in vars(C2). 305%* 306%* example: inv_replace( [p(a,B):p], [A/a], [p(C,D):p], [C/a]). 307%* 308%* peculiarities: this is not the inverse operation for replacement : 309%* We don't distinguish the between places of terms. 310%* 311%* see also: 312%* 313%*********************************************************************** 314 315 316inv_replace(C,S1,D,S2):- 317 copy_term( (C,S1) , (E,S2) ), 318 do_inv_replace( E, S2, D). 319 320 321do_inv_replace( [], _, []). 322 323do_inv_replace( [ L|More], S, [L1|More1]):- 324 do_inv_replace1( L, S, L1), 325 do_inv_replace(More, S, More1). 326 327do_inv_replace1( T1,S,T2 ):- 328 ( var(T1) -> T1 = T2 329 ; 330 member( X / T, S), T == T1 -> T2 = X 331 ; 332 functor( T1, F, N) -> functor(T2,F,N), do_inv_replace1(N,T1,T2,S) 333 ). 334 335do_inv_replace1(0,_,_,_). 336 337do_inv_replace1(N,T1,T2,S):- 338 arg(N,T1,A), 339 arg(N,T2,B), 340 do_inv_replace1(A,S,B), 341 M is N - 1, 342 do_inv_replace1(M,T1,T2,S). 343 344 345do_inv_replace1(2,[T],T2,S) :- 346 arg(2,T2,[]), 347 do_inv_replace1(1,[T],T2,S). 348 349 350%*********************************************************************** 351%* 352%* predicate: term_size/2 353%* 354%* syntax: term_size(+Term,-Size) 355%* 356%* args: 357%* 358%* description: the folllowing code is a debugged copy from the Quintus library 359%* 'termdepth' 360%* term_size(+Term, ?Size) calculates the Size of a Term, defined 361%* to be the number of constant and function symbol occurrences in it. 362%* 363%* example: 364%* 365%* peculiarities: none 366%* 367%* see also: 368%* 369%*********************************************************************** 370 371term_size(Term, Size) :- 372 ( var(Term) -> Size = 0 373 ;/* nonvar(Term) */ 374 functor(Term, _F, Arity), % Here was the bug 375 term_size(Arity, Term, 1, Size) % " 376 ). 377 378 379term_size(N, NonVar, SoFar, Size) :- 380 ( N =:= 0 -> 381 Size is SoFar 382 ; arg(N, NonVar, Arg), 383 term_size(Arg, ArgSize), 384 Accum is SoFar+ArgSize, 385 M is N-1, 386 term_size(M, NonVar, Accum, Size) 387 ). 388 389 390%*************************************************************************** 391%* 392%* predicate: contains_vars/2 393%* 394%* syntax: contains_vars(+Term,+Terms) 395%* 396%* args: Term: any prolog term 397%* Vars: list of prolog terms (also variables) 398%* 399%* description: succeeds if all terms in Terms occur in Term 400%* 401%* example: 402%* 403%* peculiarities: 404%* 405%* 406%* see also: 407%* 408%*********************************************************************** 409 410contains_vars([],_). 411contains_vars([V|Vars],Term):- 412 contains_var(V,Term), 413 contains_vars(Vars,Term). 414 415 416%*************************************************************************** 417%* 418%* predicate: flagged_contains_vars/3 419%* 420%* syntax: flagged_contains_vars(+Term,+Terms,-Flag) 421%* 422%* args: Term: any prolog term, Flag in {true,false} 423%* Vars: list of prolog terms (also variables) 424%* 425%* description: returns true if all terms in Terms occur in Term, else false 426%* 427%* example: 428%* 429%* peculiarities: 430%* 431%* 432%* see also: 433%* 434%*********************************************************************** 435 436flagged_contains_vars(Vars,Term,true):- contains_vars(Vars,Term),!. 437flagged_contains_vars(_Vars,_Term,false). 438 439 440%*********************************************************************** 441%* 442%* predicate: inverse_substitute/2 443%* 444%* syntax: inverse_substitute(+ClauseIn,-ClauseOut) 445%* 446%* args: clauses in list notation, i.e. [ head(A):p, b1(A):n, .. ] 447%* 448%* description: replace one term in ClauseIn by a variable. 449%* Thru backtracking all solutions can be obtained. 450%* Implementation: flatten Clause, 451%* truncate one literal, 452%* truncate unconnected literals, 453%* unflatten Clause. 454%* 455%* example: 456%* 457%* peculiarities: Since identical terms are represented only once in 458%* our flattening, we cannot tell between different 459%* places the terms appear at. 460%* 461%* see also: Muggleton,1988 462%* 463%*********************************************************************** 464 465inverse_substitute(Clause,Clause). % empty inverse substitution 466 467inverse_substitute(ClauseIn,ClauseOut):- 468 flatten_clause(ClauseIn,C1), 469 remove_type_literal(C1,C2), 470 truncate_unconnected(C2,C3), 471 unflatten_clause(C3,ClauseOut). 472 473 474%*********************************************************************** 475%* 476%* predicate: remove_type_literal/2 477%* 478%* syntax: remove_type_literal(+CL,-CL1) 479%* 480%* args: CL,CL1: clause in list notation 481%* 482%* description: drop a "type literal" functor_p(...) 483%* the next rules allow to perform inverse substitutions on several terms, 484%* at the cost of an exploding search space. 485%* A better strategy is to trunacte literals one by one and 486%* only to truncate the promising clauses further. 487%* 488%* example: 489%* 490%* peculiarities: none 491%* 492%* see also: 493%* 494%*********************************************************************** 495 496remove_type_literal([ L_p:n | More ] , More):- % drop this literal 497 functor( L_p, F, _), 498 string_append( _ , '_p', F). 499 500 501 502remove_type_literal([ L:S | More ] , [L:S|More1] ):- % drop another literal 503 remove_type_literal(More,More1). 504 505 506 507 508%*********************************************************************** 509%* 510%* predicate: inverse_substitute1/2 511%* 512%* syntax: inverse_substitute1(+CL,-CL) 513%* 514%* args: CL,CL1: clauses in list notation 515%* 516%* description: this is an alternative approach without flattening 517%* it replaces terms by variables. 518%* (This does of course not work on flat clauses) 519%* 520%* example: 521%* 522%* peculiarities: none 523%* 524%* see also: 525%* 526%*********************************************************************** 527 528inverse_substitute1(CLin,CLout):- 529 copy_term(CLin,CLin1), 530 clist_to_prolog(CLin1,Clause), 531 mysetof(Sub:Pos,( subterm_at_position(Clause,Sub,[],Pos), 532 \+(part_of_clause(Sub,Clause)), 533 nonvar(Sub) % this rule disallows variable renaming to constrain 534 % search space at the cost of incompleteness 535 ), Sublist), 536 isub1_list(Sublist,Sublist1), 537 best(Sublist1,T:Positions), 538 do_inverse_sub1(T,Positions,_,Clause,Clause1), 539 clist_to_prolog(CLout,Clause1), 540 \+(variant(CLout,CLin)). 541 542 543isub1_list([],[]). 544isub1_list([T:Pos|R],[T:[Pos|Pos1]|R2]):- 545 isub1_l(T,R,R1,Pos1), 546 isub1_list(R1,R2). 547 548isub1_l(_,[],[],[]). 549isub1_l(T,[T1:Pos|R],R2,Pos1):- 550 isub1_l(T,R,R1,Pos0), 551 ( T == T1 -> 552 R2 = R1,Pos1 = [Pos|Pos0] 553 ; R2 = [T1:Pos|R1], Pos1 = Pos0 554 ). 555 556 557%*********************************************************************** 558%* 559%* predicate: do_inverse_substitute1/5 560%* 561%* syntax: do_inverse_substitute(+Term,+Positions,+Var,+Clause,-Clause) 562%* 563%* args: Clause: Prolog clause 564%* Term: the term in Clause to be replaced with variable Var 565%* Positions: list of positions of Term within Clause where it might 566%* be replaced. A position is a list of numbers 567%* 568%* description: replaces Term by a Var 569%* preference is to replace all occurrences of Term by Var; 570%* thru backtracking, clauses may be obtained where 571%* only some occurences of term are replaced. 572%* 573%* example: 574%* 575%* peculiarities: none 576%* 577%* see also: 578%* 579%*********************************************************************** 580 581do_inverse_sub1(_,[],_,Clause,Clause). 582do_inverse_sub1(T,[P|R],Var,Clause,Clause2):- 583 do_inverse_sub1(T,R,Var,Clause,Clause1), 584 do_isub1(T,P,Var,Clause1,Clause2). 585do_inverse_sub1(T,[_|R],Var,Clause,Clause1):- 586 do_inverse_sub1(T,R,Var,Clause,Clause1). 587 588do_isub1(_,[],Var,_,Var). 589do_isub1(T,[P|R],V,C,C1):- 590 functor(C,F,N),functor(C1,F,N), 591 do_isub_copy(N,P,C,C1), 592 arg(P,C1,C1p),arg(P,C,Cp), 593 do_isub1(T,R,V,Cp,C1p). 594 595do_isub_copy(0,_,_,_):- !. 596do_isub_copy(N,P,C,C1):- 597 N1 is N - 1, 598 do_isub_copy(N1,P,C,C1), 599 ( N == P -> 600 true 601 ; arg(N,C,Cn),arg(N,C1,Cn) 602 ). 603 604 605%*********************************************************************** 606%* 607%* predicate: skolemize/3, deskolemize/3 608%* 609%* syntax: skolemize(+Term1,-Subst,-Term2) 610%* 611%* args: Term1,Term2: arbiraty prolog terms 612%* Subst : substitution [ V1/t1, V2/t2, .. ] 613%* where Vi are variables, ti skolem atoms 614%* 615%* description: skolemization is a special substitution: all variables 616%* of Term1 are substituted by atoms. One keeps track of 617%* the substitution thru Subst. 618%* 619%* example: 620%* 621%* peculiarities: none 622%* 623%* see also: Rouveirol,1991: ITOU. 624%* 625%*********************************************************************** 626 627skolemize(T1,S,T2):- 628 skolemize(T1,[],S,T2). 629 630skolemize(T1,S,S,Sk_Atom):- 631 var(T1), 632 already_skolem_covered(T1,S,Sk_Atom), 633 !. 634skolemize(Var,S,[Var/Sk_Atom|S],Sk_Atom):- 635 var(Var), 636 !, 637 gensym(sk_atom,Sk_Atom). 638skolemize(T1,S1,S2,T2):- 639 functor(T1,F,N), 640 functor(T2,F,N), 641 skolemize(N,T1,S1,S2,T2). 642skolemize(0,_,S,S,_). 643skolemize(N,T,S1,S2,U):- 644 arg(N,T,Tn), 645 arg(N,U,Un), 646 skolemize(Tn,S1,S3,Un), 647 M is N - 1, 648 skolemize(M,T,S3,S2,U). 649 650 651%*********************************************************************** 652%* 653%* predicate: already_skolem_covered/3 654%* 655%* syntax: already_skolem_covered(+Var,+Subst,-Skolem_atom) 656%* 657%* args: 658%* 659%* description: if Var has already been skolemized, i.e. Var:Skolem_atom in Subst, 660%* the corresponding Skolem_atom is returned 661%* 662%* example: 663%* 664%* peculiarities: alter Name: already_covered 665%* 666%* see also: 667%* 668%*********************************************************************** 669 670already_skolem_covered( Var, [ Var1/Sk_Atom | _ ], Sk_Atom):- 671 Var == Var1,!. 672 673already_skolem_covered( Var, [ _| S ], Sk_Atom):- 674 already_skolem_covered( Var,S, Sk_Atom). 675 676 677%*********************************************************************** 678%* 679%* predicate: deskolemize/3 680%* 681%* syntax: deskolemize(+Term1,+Subst,-Term2) 682%* 683%* 684%* args: Term1,Term2: arbiraty prolog terms 685%* Subst : substitution [ V1/t1, V2/t2, .. ] 686%* where Vi are variables, ti skolem atoms 687%* description: Deskolemization reverses skolemization, if the 688%* skolem substitution is given as input. 689%* 690%* example: 691%* 692%* peculiarities: none 693%* 694%* see also: 695%* 696%*********************************************************************** 697 698deskolemize(Sk_Atom,S,Var):- 699 atom(Sk_Atom), 700 skolem_covered(Sk_Atom,S,Var), 701 !. 702deskolemize(Atom,_,Atom):- 703 atom(Atom), 704 !. 705deskolemize(Var,_S,Var):- 706 var(Var), 707 !. 708deskolemize(T1,S,T2):- 709 functor(T1,F,N), 710 functor(T2,F,N), 711 deskolemize(N,T1,S,T2). 712deskolemize(0,_,_,_). 713deskolemize(N,T,S,U):- 714 arg(N,T,Tn), 715 arg(N,U,Un), 716 deskolemize(Tn,S,Un), 717 M is N - 1, 718 deskolemize(M,T,S,U). 719 720 721%*********************************************************************** 722%* 723%* predicate: skolem_covered/3 724%* 725%* syntax: skolem_covered(+Skolem_atom,+Subst,-Var) 726%* 727%* args: 728%* 729%* description: returns the variable that has been skolemized with Skolem_atom, 730%* i.e. Var/Skolem_atom in Subst 731%* 732%* example: 733%* 734%* peculiarities: none 735%* 736%* see also: alter Name: covered 737%* 738%*********************************************************************** 739 740skolem_covered(Sk_Atom, [ Var/Sk_Atom | _ ], Var):- !. 741skolem_covered(Sk_Atom, [ _| S ], Var):- 742 skolem_covered(Sk_Atom,S,Var). 743 744 745%*********************************************************************** 746%* 747%* predicate: skolems/2 748%* 749%* syntax: skolems(+Term,-Skolems) 750%* 751%* args: Term: skolemized term, Skolems: all skolem atoms in Term 752%* 753%* description: returns skolem atoms occuring in Term 754%* 755%* example: 756%* 757%* peculiarities: 758%* 759%* see also: 760%* 761%*********************************************************************** 762 763skolems(Term,Skolems):- 764 setof( Skolem, Len^( sub_term(Skolem,Term),atom(Skolem), 765 substring(Skolem,sk_atom,0,Len) 766 ), 767 Skolems),!. 768skolems(_,[]). 769 770 771%*********************************************************************** 772%* 773%* predicate: relevant_vars2/6 774%* 775%* syntax: relevant_vars2(+C1,+C2,+Gen,+S1,+S2,-RelVars) 776%* 777%* args: C1,C2,Gen: clauses in list notation. C1,C2 at bottom of W. 778%* S1,S2: substitutions [V1=T1, .. ]. 779%* RelVars: list of vars [ V1, V2, .. ] 780%* 781%* description: determine relevant vars with CIGOL heuristics. 782%* A variable V in Gen is relevant if 783%* one of the terms T1, T2 it is substituted by in S1, S2 784%* contains a variable that also appears elsewhere 785%* in S1 or S2. 786%* 787%* example: 788%* 789%* peculiarities: none 790%* 791%* see also: 792%* 793%*********************************************************************** 794 795relevant_vars2(_,_,C,S1,S2,RelVars):- 796 vars(C,AllVars), 797 relevant_vars2(AllVars,S1,S2,RelVars). 798 799 800relevant_vars2([],_,_,[]). 801 802relevant_vars2([V|MoreVars],S1,S2,[V|RelVars]):- 803 ( member( W/T1, S1), V == W, member( X/T1a, S1), V \== X, 804 sub_term(Subterm1,T1), var(Subterm1), contains_var(Subterm1,T1a) 805 ; 806 member( W/T2, S2), V == W, member( Y/T2a, S2), V \== Y, 807 sub_term(Subterm2,T2), var(Subterm2), contains_var(Subterm2,T2a) 808 ),!, 809 relevant_vars2(MoreVars, S1,S2,RelVars). 810 811relevant_vars2([_V|MoreVars],S1,S2,RelVars):- 812 relevant_vars2(MoreVars, S1,S2,RelVars). 813 814 815 816%*********************************************************************** 817%* 818%* predicate: relevant_vars3/6 819%* 820%* syntax: relevant_vars3(+C1,+C2,+Gen,+S1,+S2,-RelVars) 821%* 822%* args: C1,C2,Gen: clauses in list notation 823%* S1,S2: substititions 824%* RelVars : set of relevant vars 825%* 826%* description: Gen is a common generaliztion of C1,C2 , 827%* s.t. S1(Gen) is a subsetof C1, and analogously for C2. 828%* 829%* A variable is relevant if 830%* it appears in both Gen and ( C1 - Gen ) 831%* or Gen and ( C2 - Gen ). 832%* 833%* example: 834%* 835%* peculiarities: none 836%* 837%* see also: IRES,ITOU 838%* 839%*********************************************************************** 840 841relevant_vars3(C1,C2,Gen,S1,S2,Vars):- 842 skolemize( (C1,C2,Gen,S1,S2), Phi, (D1,D2,Gen1,R1,R2) ), 843 relevant_vars3a(D1,Gen1,R1,Vars1), 844 relevant_vars3a(D2,Gen1,R2,Vars2), 845 length(Vars1,Len1), 846 length(Vars2,Len2), 847 Len1 == Len2, 848 union(Vars1,Vars2,Vars0), 849 deskolemize(Vars0,Phi,Vars). 850 851relevant_vars3a(Spec,Gen,S,Skolems):- %%changed Irene 852 replace(Gen,S,Gen1,S), 853 subtract( Spec,Gen1, Rest), 854 inv_replace(Rest,S,Rest1,S), 855 skolems(Rest1, Skolems1), 856 skolems(Gen, Skolems2), 857 intersection(Skolems1,Skolems2,Skolems). 858 859 860 861%*********************************************************************** 862%* 863%* predicate: findargs/3 864%* 865%* syntax: findargs(+CL,+Accu,-Accu) 866%* 867%* args: CL: clause in list notation, Accu: arguments of the literals in CL 868%* 869%* description: find all arguments of the literals of a given clause 870%* 871%* example: 872%* 873%* peculiarities: 874%* 875%* see also: 876%* 877%*********************************************************************** 878 879findargs([],Result,Result) :- !. 880findargs([Lit1:_|Rest],Accu,Result) :- 881 functor(Lit1,_,N), 882 allarg(N,Lit1,[],Args), 883 union(Accu,Args,Newaccu), % set operator 884 findargs(Rest,Newaccu,Result). 885 886allarg(0,_,Accu,Accu) :- !. 887allarg(N,Lit,Args,Result) :- 888 arg(N,Lit,Arg1), 889 M is N - 1, 890 nonmember(Arg1,Args) -> 891 allarg(M,Lit,[Arg1|Args],Result); 892 allarg(M,Lit,Args,Result). 893 894 895%************************************************************************ 896%* 897%* predicate: buildrelterms/6 898%* 899%* syntax: buildrelterms(+CL1,+CL2,+Clgg,+Subst1,+Subst2,-TermList) 900%* 901%* args: CL1, CL2, Clgg .. clauses in list representation 902%* Subst1,Subst2 ... substitutions such that Clgg Subst1 = CL1 903%* and Clgg Subst2 = CL2 904%* TermList ... list of relevant terms for the new predicate 905%* 906%* description: determines the relevant terms for the new predicate 907%* as described in R. Wirth's 1989 PhD thesis 908%* 909%* example: 910%* 911%* peculiarities: 912%* 913%* see also: 914%* 915%************************************************************************ 916 917buildrelterms(SpecC1,SpecC2,Gen,S1,S2,Terms) :- 918 skolemize((Gen,SpecC1,SpecC2,S1,S2),SS,(Gen1,Spec1,Spec2,SS1,SS2)), 919 findterms(Gen1,Spec1,SS1,Terms1), % Terms1 = RArgs1 != {} 920 findterms(Gen1,Spec2,SS2,Terms2), % Terms2 = RArgs2 != {} 921% union(Terms1,Terms2,TermsS), 922% deskolemize(TermsS,SS,Terms). % changed Irene 923 deskolemize((Terms1,Terms2),SS,(T1,T2)), 924 general_terms(T1,T2,Terms,S1,S2). 925 926 927findterms(Gen,Spec,SS1,RArgsG) :- 928 replace(Gen,SS1,Gen2,_), 929 subtract(Spec,Gen2,RestSpec), % RestSpec = Ci^r ( Spec - Gen ) 930 subtract(Spec,RestSpec,SpecG), % SpecG = Ci^g 931 findargs(SpecG,[],ArgsG), 932 findargs(RestSpec,[],ArgsR), 933 exists_intersect(ArgsG,ArgsR,RArgsG). % RArgs = relevant argument terms (not []) 934% inv_replace(RArgsG0,SS1,RArgsG,SS1). % changed (Irene) 935 936%************************************************************************ 937%* 938%* predicate: general_terms/5 939%* 940%* syntax: general_terms(+T1,+T2,-TG,+Subst1,+Subst2) 941%* 942%* args: T1, T2 .. relevant terms in CL1, CL2 (cf. above) 943%* Subst1, Subst2 .. substitutions (cf. above) 944%* TG .. relevant terms in Clgg 945%* 946%* description: determines the relevant terms in Clgg that 947%* correspond to the relevant terms in CL1 and CL2 948%* here, inv_replace is used!! 949%* 950%* example: 951%* 952%* peculiarities: 953%* 954%* see also: 955%* 956%************************************************************************ 957 958%* general_terms (like a shotgun wedding between lgg for terms and inverse replacement...) 959general_terms([],[],[],_,_) :- !. 960 961general_terms([T1|R1],[],[T|R3],S1,_) :- 962 ( genterm_test(T/T1,S1) -> true; 963 inv_replace(T1,S1,T,_)), 964 !, general_terms(R1,[],R3,S1,_). 965 966general_terms([],[T2|R2],[T|R3],_,S2) :- 967 (genterm_test(T/T2,S2) -> true; 968 inv_replace(T2,S2,T,_)), 969 !, general_terms([],R2,R3,_,S2). 970 971general_terms([T1|R1],L2,[T|R3],S1,S2) :- 972 gen_term(T1,L2,L2Rest,T,S1,S2), !, 973 general_terms(R1,L2Rest,R3,S1,S2). 974 975gen_term(T1,L2,L2new,T,S1,S2) :- 976 nonvar(T1), 977 functor(T1,F,N), 978 effaceall(T2,L2,L2new), 979 functor(T2,F,N), 980 lgg_terms(T1,T2,T,_,_,S1,S2). 981 982gen_term(T1,L2,L2new,X,S1,S2) :- 983 effaceall(T2,L2,L2new), 984 genterm_test(X/T1,S1), 985 genterm_test(Y/T2,S2), 986 X == Y. 987 988gen_term(T1,L2,L2,T,S1,_) :- 989 genterm_test(T/T1,S1) -> true; 990 inv_replace(T1,S1,T,_). 991 992 993%************************************************************************ 994%* 995%* predicate: exists_intersect/3 996%* 997%* syntax: exists_intersect(+L1,+L2,-L) 998%* 999%* args: L1,L2,L: lists 1000%* 1001%* description: if nonempty intersection exists, succeeds and returns 1002%* intersection, fails else 1003%* 1004%* example: 1005%* 1006%* peculiarities: 1007%* 1008%* see also: 1009%* 1010%************************************************************************ 1011 1012exists_intersect(X,Y,Z) :- exi(X,Y,Z,_),!. 1013exi([],_,[],Flag) :- Flag == yes. 1014exi([],_,[],_) :- !,fail. 1015exi([X|R],Y,[X|Z],yes) :- 1016 memberchk(X,Y),!, 1017 exi(R,Y,Z,yes). 1018exi([_|R],Y,Z,Flag) :- 1019 exi(R,Y,Z,Flag). 1020 1021 1022 1023%************************************************************************ 1024%* 1025%* predicate: clean_subst/3 1026%* 1027%* syntax: clean_subst(+CL,+Subst,-Subst) 1028%* 1029%* args: CL: clause in list notation, Subst: a substitution [X/Term,...] 1030%* 1031%* description: removes all X/T from Subst such that X does not occur in CL 1032%* 1033%* example: 1034%* 1035%* peculiarities: 1036%* 1037%* see also: 1038%* 1039%************************************************************************ 1040 1041clean_subst(_,[],[]). 1042clean_subst(CL,[X/T|R],R2):- 1043 clean_subst(CL,R,R1), 1044 ( contains_var(X,CL) -> 1045 R2 = [X/T|R1] 1046 ; R2 = R1 1047 )