1% MODULE tdref_it EXPORTS 2:- module(tdref_it, 3 [ refinement_unify_variables/3, 4 refinement_unify_variables/2, 5 refinement_instantiate_variables/3, 6 refinement_instantiate_variables/2, 7 refinement_add_body_literal/3, 8 refinement_add_body_literal/2, 9 refinement/2, 10 possible_body_literals/3 11 ]). 12 13 14% IMPORTS 15:- use_module(home(kb), 16 [get_clause/5, get_evaluation/2, get_predlist/1]). 17:- use_module(home(td_basic), 18 [distribute_vars/3,enumerate_t/3,append_body/3]). 19:- use_module(home(filter), 20 [noduplicate_atoms/1,noduplicate_atom/2,select_var_sharing_lits/2]). 21:- use_module(home(div_utils), 22 [mysetof/3]). 23:- use_module(home(var_utils), 24 [typed_only_vars1/2,clause_terms/2]). 25:- use_module(home(argument_types), 26 [compare_types/3,types_of/3]). 27:- use_module(home(show_utils), 28 [write_list/1]). 29 30 31% METAPREDICATES 32% none 33 34 35%*********************************************************************** 36%* 37%* module: tdref_it.pl 38%* 39%* author: I.Stahl date:12/92 40%* 41%* changed: comments BT; 11/10/92 42%* 43%* description: top-down refinement operators for Horn clauses 44%* work iteratively 45%* 46%* 47%* see also: 48%* 49%* 50%*********************************************************************** 51 52 53%*********************************************************************** 54%* 55%* predicates: refinement_unify_variables/2, 56%* refinement_instantiate_variables/2, 57%* refinement_add_body_literal/2 58%* 59%* syntax: refinement_...(+ClauseID,-(ClauseID,CL)) 60%* 61%* args: ClauseID ... ID of the clause to be specialized 62%* CL .... list of specialisations of Clause 63%* 64%* description: refines clause by unifying variables/instantiating 65%* variables with terms/adding a body literal. Returns 66%* list of specialised clauses 67%* 68%* example: 69%* 70%* peculiarities: none 71%* 72%* see also: 73%* 74%*********************************************************************** 75 76refinement_unify_variables(ID,(ID,CL)):- 77 get_clause(ID,H,B,_,_), 78 C = (H:-B), 79 clause_terms(C,Terms), 80 types_of(Terms,C,TTerms), 81 refinement_unify_variables(C,TTerms,CL). 82 83refinement_instantiate_variables(ID,(ID,CL)):- 84 get_clause(ID,H,B,_,_), 85 C = (H:-B), 86 clause_terms(C,Terms), 87 types_of(Terms,C,TTerms), 88 refinement_instantiate_variables(C,TTerms,CL). 89 90refinement_add_body_literal(ID,(ID,CL)):- 91 get_clause(ID,H,B,_,_), 92 C = (H:-B), 93 clause_terms(C,Terms), 94 types_of(Terms,C,TTerms), 95 refinement_add_body_literal(C,TTerms,CL1), 96 select_var_sharing_lits(CL1,CL). 97 98 99 100%*********************************************************************** 101%* 102%* predicates: refinement_unify_variables/3, 103%* refinement_instantiate_variables/3, 104%* refinement_add_body_literal/3 105%* 106%* syntax: refinement_...(+Clause,+Terms,-CL) 107%* 108%* args: Clause ... the clause to be specialized 109%* Terms ... the terms that shall be used in refinement 110%* of the form [T:Type,...] 111%* CL .... list of specialisations of Clause 112%* 113%* description: refines clause by unifying variables/instantiating 114%* variables with terms/adding a body literal. Returns 115%* list of specialised clauses 116%* 117%* example: 118%* 119%* peculiarities: none 120%* 121%* see also: 122%* 123%*********************************************************************** 124 125refinement_unify_variables(C,T,CL):- 126 typed_only_vars1(T,Vars), 127 ref_unify_vars(C,Vars,Vars,[],CL). 128 129refinement_instantiate_variables(C,T,CL):- 130 typed_only_vars1(T,Vars), 131 ref_instantiate_vars(C,Vars,[],CL). 132 133refinement_add_body_literal(C,T,CL):- 134 ( C = (_:-_) -> 135 ref_add_body_literal(C,T,[],CL) 136 ; ref_add_body_literal((C:-true),T,[],CL) 137 ). 138 139 140 141%*********************************************************************** 142%* 143%* predicates: possible_body_literals/3 144%* 145%* syntax: possible_body_literals(+Clause,+Terms,-LL) 146%* 147%* args: Clause ... the clause to be specialized 148%* Terms ... the terms that shall be used in refinement 149%* of the form [T:Type,...] 150%* LL .... list of literals that might be added 151%* 152%* description: Returns the list of literals that might be used to refine 153%* Clause 154%* 155%* example: 156%* 157%* peculiarities: none 158%* 159%* see also: 160%* 161%*********************************************************************** 162 163possible_body_literals(C,Terms,LL):- 164 get_predlist(Predlist), 165 enumerate_terms(Predlist,Terms,C,[],LL). 166 167 168%*********************************************************************** 169%* predicate: ref_unify_vars/5 170%* syntax: ref_unify_vars(+C,+[X:T|R],+V,+CL,-CL2) 171%* 172%* args: C: the clause to be refined 173%* [X:T|R]: all variables with their types in C 174%* V: all variables X:T in C 175%* 176%* CL: initial clause set 177%* CL2: CL + copies of C where variables are unified 178%* 179%* description: unifies clause variables of the same type 180%* 181%* example: 182%* 183%* peculiarities: none 184%* 185%* see also: 186%* 187%*********************************************************************** 188 189ref_unify_vars(_,[],_,CL,CL). 190ref_unify_vars(C,[X|R],V,CL,CL2):- 191 ref_unify_vars(C,R,V,CL,CL1), 192 ref_unify_vars1(C,X,V,CL1,CL2). 193 194 195%*********************************************************************** 196%* 197%* predicate: ref_unify_vars1/5 198%* 199%* syntax: ref_unify_vars1(+C,+X:Tx,+[Y:Ty|R],+CL,-CL2) 200%* 201%* args: C: the clause to be refined 202%* X:Tx: variable X of type Tx in C 203%* [Y:Ty|R]: all variables Y:Ty in C 204%* 205%* CL: initial clause set 206%* CL2: copies of the clause C where X is unified with each 207%* matching Y 208%* 209%* description: makes copies of the clause C with unified variables 210%* if the type of the variables is can be matched 211%* 212%* example: 213%* 214%* peculiarities: none 215%* 216%* see also: 217%* 218%*********************************************************************** 219 220ref_unify_vars1(_,_,[],CL,CL). 221ref_unify_vars1(C,X:Tx,[Y:Ty|R],CL,CL2):- 222 ref_unify_vars1(C,X:Tx,R,CL,CL1), 223 ( (compare_types(Tx,Ty,_),X @< Y) -> 224 copy_term((C,X,Y),(C1,Z,Z)), 225 ( noduplicate_atoms(C1) -> 226 CL2 = [C1|CL1] 227 ; CL2 = CL1 228 ) 229 ; CL2 = CL1 230 ). 231 232 233%*********************************************************************** 234%* 235%* predicate: ref_instantiate_vars/4 236%* 237%* syntax: ref_instantiate_vars(+C,+[X:T|R]+CL,-CL2) 238%* 239%* args: C: the clause to be refined 240%* [X:T|R]: variables X of type T in C 241%* 242%* CL: initial clause set 243%* CL2: CL + copies of C where variables are instantiated 244%* 245%* description: instantiates variables by terms according to the 246%* variables' type 247%* 248%* example: 249%* 250%* peculiarities: none 251%* 252%* see also: 253%* 254%*********************************************************************** 255 256ref_instantiate_vars(_,[],CL,CL). 257ref_instantiate_vars(C,[X:T|R],CL,CL2):- 258 ref_instantiate_vars(C,R,CL,CL1), 259 H =.. [T,X], 260 H1 =.. [T,X1], 261 mysetof(H1,I^B^BL^Lab^(get_clause(I,H1,B,BL,Lab),nonvar(X1)),HL), 262 ref_inst_vars(HL,H,C,HL1), 263 append(HL1,CL1,CL2). 264 265ref_inst_vars([],_,_,[]). 266ref_inst_vars([H1|R],H,C,HL2):- 267 ref_inst_vars(R,H,C,HL1), 268 ( (copy_term((H,C),(H1,C1)),noduplicate_atoms(C1)) -> 269 HL2 = [C1|HL1] 270 ; HL2 = HL1 271 ). 272 273 274%*********************************************************************** 275%* 276%* predicate: ref_add_body_literal/4 277%* 278%* syntax: ref_add_body_literal(+C,+Terms,+CL,-CL1) 279%* 280%* args: C: the clause to be refined 281%* [TT:T|R]: all terms TT and subterms with their types T in C 282%* 283%* CL: initial clause set 284%* CL2: CL + copies of C with additional body literals 285%* 286%* description: adds a body literal to C by 287%* - selecting all predicates with a type restriction contained in the kb 288%* - enumerating literals where (at least one) argument of the new 289%* literal is unfied with terms in the clause 290%* - for each literal L: copy C and L, append the copied 291%* literal to the copy of C and add the resulting clause to CL 292%* 293%* example: 294%* 295%* peculiarities: none 296%* 297%* see also: 298%* 299%*********************************************************************** 300 301ref_add_body_literal(C,Terms,CL,CL1):- 302 get_predlist(Predlist), 303 enumerate_terms(Predlist,Terms,C,[],L), 304 add_to_bodies(L,C,CL,CL1). 305 306 307%*********************************************************************** 308%* 309%* predicate: add_to_bodies/4 310%* 311%* syntax: add_to_bodies(+[Lit|R],+C,+CL,-CL1) 312%* 313%* args: [Lit|R]: a set of literals Lit to be added to the body 314%* C: the clause to be refined 315%* 316%* CL: initial clause list 317%* CL1: CL + refined clauses 318%* 319%* description: adds each literal to a copy of C, if it is not 320%* duplicate in C 321%* 322%* example: 323%* 324%* peculiarities: none 325%* 326%* see also: 327%* 328%*********************************************************************** 329 330add_to_bodies([],_,CL,CL). 331add_to_bodies([Pred|R],C,CL,CL2):- 332 add_to_bodies(R,C,CL,CL1), 333 copy_term((Pred,C),(Pred1,(H1:-B1))), 334 ( noduplicate_atom(Pred1,(H1,B1)) -> 335 append_body((H1:-B1),Pred1,C2), 336 CL2 = [C2|CL1] 337 ; CL2 = CL1 338 ). 339 340 341%*********************************************************************** 342%* 343%* predicate: enumerate_terms/5 344%* 345%* syntax: enumerate_terms(+[P:PVars|R],+Terms,+C,+L,-L2) 346%* 347%* args: [P:PVars|R]: predicate P & its variables PVars=[PV1:Tpv1,...] 348%* Terms: all terms with types in C 349%* C: clause to be refined 350%* L: initial literal list 351%* 352%* L2: new literal list 353%* 354%* description: builds all literals from all predicates to be added by 355%* - collecting all variables that could be unified with any variable of PVars 356%* - building all literals with these variables replaced 357%* - eliminating all those literals that already occur in C 358%* - appending the literals to L2 359%* 360%* example: 361%* 362%* peculiarities: none 363%* 364%* see also: 365%* 366%*********************************************************************** 367 368enumerate_terms([],_,_,L,L). 369enumerate_terms([P:PVars|R],V,C,L,L2):- 370 enumerate_terms(R,V,C,L,L1), 371 distribute_vars(PVars,V,PVars1), 372 enumerate_t(PVars1,[P],Plist), 373 append(Plist,L1,L2). 374 375 376%*********************************************************************** 377%* 378%* predicate: refinement/2 379%* 380%* syntax: refinement(+ID,-CL) 381%* 382%* args: ID: ID of a clause to be refined 383%* CL: a list with refinements of the clause with ID 384%* 385%* description: shapiro's general refinement operator for a clause 386%* with ID (all terms are eligible for refinement): 387%* if there are covered positive examples: 388%* - prepare for refinement: 389%* a list of all terms and subterms augmented by their types 390%* and a list of all variables in the clause with types 391%* - refine clause by 392%* - unifying variables within the clause 393%* - instantiating variables within the clause to terms 394%* - adding body literals. Only literals sharing at least a 395%* variable with clause ID are allowed. 396%* 397%* example: 398%* 399%* peculiarities: none 400%* 401%* see also: 402%* 403%*********************************************************************** 404 405refinement(ID,CL):- 406 number(ID),!, 407 get_clause(ID,H,B,_,_), 408 get_evaluation(ID,evaluation(_,_,Pos,_,_,_,_,_,_)), 409 ( Pos == [] -> 410 CL = [] 411 ; clause_terms((H:-B),Terms), 412 types_of(Terms,(H:-B),TTerms), 413 refinement_unify_variables((H:-B),TTerms,CL0), 414 refinement_instantiate_variables((H:-B),TTerms,CL1), 415 refinement_add_body_literal((H:-B),TTerms,CL2), 416 select_var_sharing_lits(CL2,CL3), 417 append(CL0,CL1,CL4),append(CL4,CL3,CL) 418 ). 419 420refinement((H:-B),CL):- 421 clause_terms((H:-B),Terms), 422 types_of(Terms,(H:-B),TTerms), 423 refinement_unify_variables((H:-B),TTerms,CL0), 424 refinement_instantiate_variables((H:-B),TTerms,CL1), 425 refinement_add_body_literal((H:-B),TTerms,CL2), 426 select_var_sharing_lits(CL2,CL3), 427 append(CL0,CL1,CL4),append(CL4,CL3,CL)