guard_entailment.chr

   1 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   2 % Author:       Jon Sneyers
   3 % Email:        jon@cs.kuleuven.ac.be
   4 % Copyright:    K.U.Leuven 2004
   5 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   6
   7 :- module(guard_entailment,
   8         [
   9                 entails_guard/2,
  10                 simplify_guards/5
  11         ]).
  12
  13 %:- use_module(library(chr)).
  14 :- use_module(library(lists)).
  15 :- use_module(hprolog).
  16 :- use_module(builtins).
  17
  18 option(debug,off).
  19 option(optimize,full).
  20
  21
  22 :- constraints known/1,test/1,cleanup/0,variables/1.
  23
  24 % knowing the same thing twice is redundant
  25 idempotence @ known(G) \ known(G) <=> true.
  26
  27
  28 %--------------------------------------
  29 % Rules to check if the argument of
  30 % test/1 is entailed by known stuff
  31 %--------------------------------------
  32
  33 % everything follows from an inconsistent theory
  34 fail_implies_everything @ known(fail) \ test(X) <=> true.
  35
  36 % if it's known, it's entailed
  37 trivial_entailment @ known(G) \ test(G) <=> true.
  38
  39 varfirst_nmatch @ test(X\==A) <=> nonvar(X) | test(A\==X).
  40 distribute_nmatch @ test(X\==A) <=> nonvar(A),functor(A,Fu,Ar) |
  41                 A =.. [F|AArgs],
  42                 length(XArgs,Ar), B =.. [Fu|XArgs],
  43                 add_args_nmatch(XArgs,AArgs,ArgCond),
  44                 C = (\+ functor(X,Fu,Ar) ; (functor(X,Fu,Ar),X=B,ArgCond)),
  45                 test(C).
  46
  47 % eq implies leq
  48 eq_implies_leq1 @ known(X=:=Y) \ test(X=<Y) <=> true.
  49 eq_implies_leq2 @ known(X=:=Z) \ test(X=<Y) <=> number(Y), number(Z), Z=<Y |true.
  50 eq_implies_leq3 @ known(X=:=Z) \ test(Y=<X) <=> number(Y), number(Z), Y=<Z |true.
  51
  52 % stronger inequality implies a weaker one
  53 leq_implies_leq1 @ known(X=<Z) \ test(X=<Y) <=> number(Y), number(Z), Z=<Y |true.
  54 leq_implies_leq2 @ known(X=<Y) \ test(Z=<Y) <=> number(X), number(Z), Z=<X | true.
  55
  56 % X =< Z implies X =\= Y for all Y > Z
  57 leq_implies_neq1 @ known(X=<Z) \ test(X=\=Y) <=> number(Y), number(Z), Y>Z | true.
  58 leq_implies_neq2 @ known(X=<Y) \ test(Y=\=Z) <=> number(X), number(Z), Z<X | true.
  59
  60
  61 %--------------------------------------
  62 % Rules to translate some stuff
  63 %--------------------------------------
  64
  65 % we only want =<, =:= and =\=
  66 known_g2l @ known(X>Y) <=> known(Y<X).
  67 known_geq2leq @ known(X>=Y) <=> known(Y=<X).
  68 known_l2leq_neq @ known(X<Y) <=> known(X=<Y), known(X=\=Y).
  69 known_is2eq @ known(X is Y) <=> known(X=:=Y).
  70 test_g2l @ test(X>Y) <=> test(Y<X).
  71 test_geq2leq @test(X>=Y) <=> test(Y=<X).
  72 test_l2leq_neq @test(X<Y) <=> test(((X=<Y),(X=\=Y))).
  73 test_is2eq @ test(X is Y) <=> test(X=:=Y).
  74
  75 % propagate == and \== to =:= and =\=  (which is a weaker statement)
  76 match2eq1 @ known(X==Y) ==> number(X) | known(X=:=Y).
  77 match2eq2 @known(X==Y) ==> number(Y) | known(X=:=Y).
  78 nmatch2neq1 @ known(X\==Y) ==> number(X) | known(X=\=Y).
  79 nmatch2neq2 @ known(X\==Y) ==> number(Y) | known(X=\=Y).
  80
  81
  82 %--------------------------------------
  83 % Rules to extend the known stuff
  84 %--------------------------------------
  85
  86 % if we derived inconsistency, all other knowledge is redundant
  87 fail_is_better_than_anything_else @ known(fail) \ known(_) <=> true.
  88
  89 % conjunctions
  90 conj @ known((A,B)) <=> known(A), known(B).
  91
  92 % no need to remember trivial stuff
  93 forget_trivial01 @ known(X=:=X) <=> true.
  94 forget_trivial02 @ known(X==X) <=> true.
  95 forget_trivial03 @ known(X=<X) <=> true.
  96 forget_trivial04 @ known(X=X) <=> true.
  97
  98
  99 %--------------------------------------
 100 % Rules for = and \= (and functor)
 101 %--------------------------------------
 102 unify_vars1 @ known(X=Y) <=> var(X) | X=Y.
 103 unify_vars2 @ known(X=Y) <=> var(Y) | X=Y.
 104 %functor @ known(functor(X,F,A)) <=> var(X),ground(F),ground(A) | functor(X,F,A).
 105 inconsistency4     @ known(X\=Y) <=> var(X),var(Y),X=Y | known(fail).
 106 inconsistency4     @ known(X\=Y) <=> ground(X),ground(Y),X=Y | known(fail).
 107
 108 functor @ variables(V),known(functor(X,F,A)) <=>
 109             var(X), ground(F), ground(A) |
 110             functor(X,F,A),
 111             X =.. [_|Args],
 112             append(Args,V,NewV),
 113             variables(NewV).
 114
 115 functor_inconsistency1 @ known(functor(X,F1,A1)) <=> nonvar(X), \+ functor(X,F1,A1) | known(fail).
 116 negfunctor_trivial @ known(\+ functor(X,F1,A1)) <=> nonvar(X), functor(X,F1,A1) | known(fail).
 117 functor_inconsistency2 @ known(functor(X,F1,A1)), known(functor(X,F2,A2)) <=>
 118                         nonvar(F1),nonvar(A1),nonvar(F2),nonvar(A2)
 119                         % (F1 \= F2 ; A1 \= A2) is entailed by idempotence
 120                         | known(fail).
 121 nunify_inconsistency @ known(X\=X) <=> known(fail).
 122 nonvar_unification @ known(X=Y) <=> nonvar(X), nonvar(Y),functor(X,F,A) |
 123                     ( functor(Y,F,A),X=Y ->
 124                         true
 125                     ;
 126                         known(fail)
 127                     ).
 128 nunify_expand    @ known(X\=Y) <=> var(X),nonvar(Y), functor(Y,F,A), A>0 |
 129                     length(Args,A),
 130                     Y =.. [F|YArgs],
 131                     Y1 =.. [F|Args],
 132                     add_args_nunif(YArgs,Args,Nunif),
 133                     C = (\+ functor(X,F,A) ; (X = Y1, Nunif )),
 134                     known(C).
 135 nunify_expand2    @ known(X\=Y) <=> nonvar(X),nonvar(Y), functor(X,F,A) |
 136                     (functor(Y,F,A) ->
 137                         X =.. [F|XArgs],
 138                         Y =.. [F|YArgs],
 139                         add_args_nunif(XArgs,YArgs,Nunif),
 140                         known(Nunif)
 141                     ;
 142                         true
 143                     ).
 144 nunify_symmetry    @ known(X\=Y) ==> known(Y\=X).
 145
 146
 147 %--------------------------------------
 148 % Rules for =<
 149 %--------------------------------------
 150
 151 groundleq2 @ known(X=<Y) <=> number(X), number(Y), X>Y | known(fail).
 152
 153 % only keep the strictest inequality
 154 remove_redundant_leq1 @ known(X=<Y) \ known(X=<Z) <=> number(Y), number(Z), Y=<Z | true.
 155 remove_redundant_leq1 @ known(Z=<Y) \ known(X=<Y) <=> number(X), number(Z), X=<Z | true.
 156
 157 leq_antisymmetry @ known(X=<Y), known(Y=<X) <=> known(X=:=Y).
 158 leq_transitivity @ known(X=<Y), known(Y=<Z) ==> known(X=<Z).
 159
 160 strict_leq_transitivity @ known(X=<Y),known(X=\=Y),known(Y=<Z),known(Y=\=Z) ==> known(X=\=Z).
 161
 162
 163 %--------------------------------------
 164 % Rules for =:=   (and =\=)
 165 %--------------------------------------
 166
 167 groundeq2 @ known(X=:=Y) <=> number(X), number(Y), X=\=Y | known(fail).
 168 groundneq2 @ known(X=\=Y) <=> number(X), number(Y), X=:=Y | known(fail).
 169
 170 neq_inconsistency  @ known(X=\=X) <=> known(fail).
 171 inconsistency @ known(X=:=Y), known(X=\=Y) <=> known(fail).
 172
 173 eq_transitivity @ known(X=:=Y), known(Y=:=Z) ==> X \== Z | known(X=:=Z).
 174
 175 eq_symmetry  @ known(X=:=Y) ==> known(Y=:=X).
 176 neq_symmetry @ known(X=\=Y) ==> known(Y=\=X).
 177
 178 %--------------------------------------
 179 % Rules for number/1, float/1, integer/1
 180 %--------------------------------------
 181
 182 notnumber @ known(number(X)) <=> nonvar(X), \+ number(X) | known(fail).
 183 notfloat @ known(float(X)) <=> nonvar(X), \+ float(X)| known(fail).
 184 notinteger @ known(integer(X)) <=> nonvar(X), \+ integer(X) | known(fail).
 185 int2number @ known(integer(X)) ==> known(number(X)).
 186 float2number @ known(float(X)) ==> known(number(X)).
 187
 188
 189 %--------------------------------------
 190 % Rules for \+
 191 %--------------------------------------
 192
 193 inconsistency2 @ known(X), known(\+ X) <=> known(fail).
 194
 195
 196 %--------------------------------------
 197 % Rules for == and \==
 198 %--------------------------------------
 199
 200 inconsistency3 @ known(X\==Y), known(X==Y) <=> known(fail).
 201 eq_transitivity2 @ known(X==Y), known(Y==Z) ==> known(X==Z).
 202 neq_substitution @ known(X==Y), known(Y\==Z) ==> known(X\==Z).
 203 eq_symmetry2   @ known(X==Y) ==> known(Y==X).
 204 neq_symmetry2  @ known(X\==Y) ==> known(Y\==X).
 205 neq_inconsistency @ known(X\==X) ==> known(fail).
 206 functorsmatch@ known(X\==Y) <=> nonvar(X), nonvar(Y), functor(X,F,A) |
 207                                 (functor(Y,F,A) ->
 208                                     X =.. [F|XArgs],
 209                                     Y =.. [F|YArgs],
 210                                     add_args_nmatch(XArgs,YArgs,ArgCond),
 211                                     known(ArgCond)
 212                                 ;
 213                                     true
 214                                 ).
 215 eq_implies_unif @ known(X==Y) ==> known(X=Y).
 216
 217
 218 %--------------------------------------
 219 % Rules for var/1 and nonvar/1
 220 %--------------------------------------
 221
 222 ground2nonvar @ known(ground(X)) ==> known(nonvar(X)).
 223 compound2nonvar @ known(compound(X)) ==> known(nonvar(X)).
 224 atomic2nonvar @ known(atomic(X)) ==> known(nonvar(X)).
 225 number2nonvar @ known(number(X)) ==> known(nonvar(X)).
 226 atom2nonvar @ known(atom(X)) ==> known(nonvar(X)).
 227
 228 var_inconsistency @ known(var(X)), known(nonvar(X)) <=> known(fail).
 229
 230
 231 %--------------------------------------
 232 % Rules for disjunctions
 233 %--------------------------------------
 234
 235 %ad-hoc disjunction optimization:
 236 simplify_disj1 @ known(A) \ known((\+ A; B)) <=> known(B).
 237 simplify_disj1b @ known(A) \ known((\+ A, C; B)) <=> known(B).
 238 simplify_disj1c @ known(\+ A) \ known((A; B)) <=> known(B).
 239 simplify_disj1d @ known(\+ A) \ known((A, C; B)) <=> known(B).
 240
 241 simplify_disj2 @ known((fail; B)) <=> known(B).
 242 simplify_disj3 @ known((B ; fail)) <=> known(B).
 243
 244 simplify_disj4 @ known(functor(X,F1,A1)) \ known((\+ functor(X,F,A); B)) <=>
 245     % F1 \== F or A1 \== A
 246     true.       % the disjunction does not provide any additional information
 247
 248 simplify_disj5 @ known((\+ functor(X,F,A); B)) <=>
 249     nonvar(X), functor(X,F,A) |
 250     known(B).
 251 simplify_disj6 @ known((\+ functor(X,F,A); B)) <=>
 252     nonvar(X), \+ functor(X,F,A) |
 253     true.       % the disjunction does not provide any additional information
 254
 255 test_simplify_disj1 @test((fail;B)) <=> test(B).
 256 test_simplify_disj2 @test((B;fail)) <=> test(B).
 257
 258
 259 %--------------------------------------
 260 % Rules to test unifications
 261 %--------------------------------------
 262
 263 trivial_unif @ test(X=Y) <=> X=Y | X=Y.
 264 testgroundunif @ test(X=A) <=> ground(X),ground(A) | X=A.
 265 varfirst @ test(X=A) <=> nonvar(X),var(A) | test(A=X).
 266 distribute_unif @ variables(V) \ test(X=A) <=>   var(X),nonvar(A),
 267                 functor(A,F,Arit),Arit>0,
 268                 A =.. [F|AArgs],\+ all_unique_vars(AArgs,V) |
 269                 C=(functor(X,F,Arit),X=A),
 270                 test(C).
 271 distribute_unif2 @ test(X=A) <=>   var(X),nonvar(A),
 272                 functor(A,F,Arit),%Arit>0,
 273                 A =.. [F|AArgs] % , all_unique_vars(AArgs)
 274                 |
 275                 C=functor(X,F,Arit),
 276                 test(C).
 277 distribute_unif3 @ test(X=A) <=>   nonvar(X),nonvar(A),functor(A,F,Arit),
 278                 A =.. [F|AArgs] |
 279                 functor(X,F,Arit),
 280                 X =.. [F|XArgs],
 281                 add_args_unif(XArgs,AArgs,ArgCond),
 282                 test(ArgCond).
 283
 284 testvarunif @ variables(V) \ test(X=A) <=> \+ (memberchk_eq(A,V),memberchk_eq(X,V)) | X=A.
 285 testvarunif @ variables(V) \ test(functor(X,F,A)) <=>
 286                 var(X),ground(F),ground(A),\+ memberchk_eq(X,V) |
 287                 functor(X,F,A).       % X is a singleton variable
 288
 289 % trivial truths
 290 true_is_true @ test(true) <=> true.
 291 trivial01 @ test(X==Y) <=> X==Y | true.
 292 trivial02 @ test(X=:=Y) <=> X==Y | true.
 293 trivial03 @ test(X=<Y) <=> X==Y | true.
 294 trivial04 @ test(X=<Y) <=> ground(X), ground(Y), X=<Y | true.
 295 trivial05 @ test(X=<Y) <=> ground(X), ground(Y), X>Y | fail.
 296 trivial06 @ test(X=:=Y) <=> ground(X), ground(Y), X=:=Y | true.
 297 trivial07 @ test(X=:=Y) <=> ground(X), ground(Y), X=\=Y | fail.
 298 trivial08 @ test(X=\=Y) <=> ground(X), ground(Y), X=\=Y | true.
 299 trivial09 @ test(X=\=Y) <=> ground(X), ground(Y), X=:=Y | fail.
 300 trivial10 @ test(functor(X,F1,A1)) <=> nonvar(X), functor(X,F1,A1) | true.
 301 trivial11 @ test(functor(X,F1,A1)) <=> nonvar(X) | fail.
 302 trivial12 @ test(ground(X)) <=> ground(X) | true.
 303 trivial13 @ test(number(X)) <=> number(X) | true.
 304 trivial14 @ test(float(X)) <=> float(X) | true.
 305 trivial15 @ test(integer(X)) <=> integer(X) | true.
 306 trivial16 @ test(number(X)) <=> nonvar(X) | fail.
 307 trivial17 @ test(float(X)) <=> nonvar(X) | fail.
 308 trivial18 @ test(integer(X)) <=> nonvar(X) | fail.
 309 trivial19 @ test(\+ functor(X,F1,A1)) <=> nonvar(X), functor(X,F1,A1) | fail.
 310 trivial20 @ test(\+ functor(X,F1,A1)) <=> nonvar(X) | true.
 311 trivial21 @ test(\+ ground(X)) <=> ground(X) | fail.
 312 trivial22 @ test(\+ number(X)) <=> number(X) | fail.
 313 trivial23 @ test(\+ float(X)) <=> float(X) | fail.
 314 trivial24 @ test(\+ integer(X)) <=> integer(X) | fail.
 315 trivial25 @ test(\+ number(X)) <=> nonvar(X) | true.
 316 trivial26 @ test(\+ float(X)) <=> nonvar(X) | true.
 317 trivial27 @ test(\+ integer(X)) <=> nonvar(X) | true.
 318
 319 test_conjunction @ test((A,B)) <=> test(A),  known(A), test(B).
 320 test_disjunction @ test((A;B)) <=> true | negate_b(A,NotA),negate_b(B,NotB),
 321                      (known(NotB),test(A) ; known(NotA),test(B)).
 322
 323 % disjunctions in the known stuff --> both options should entail the goals
 324 % delay disjunction unfolding until everything is added, perhaps we can
 325 % find entailed things without using the disjunctions
 326 disjunction @ test(X), known((A;B)) <=>
 327     true |
 328     \+ try(A,X),!,
 329     negate_b(A,NotA),
 330     known(NotA),
 331     \+ try(B,X).
 332
 333
 334 % not entailed or entailment not detected
 335 could_not_prove_entailment @ test(_) <=>  fail.
 336
 337
 338 clean_store1 @ cleanup \ known(_) <=> true.
 339 clean_store2 @ cleanup \ variables(_) <=> true.
 340 clean_store3 @ cleanup <=> true.
 341
 342
 343 %--------------------------------------
 344 % End of CHR part
 345 %--------------------------------------
 346
 347
 348 entails_guard(List,Guard) :-
 349     copy_term_nat((List,Guard),(CopyList,CopyGuard)),
 350     term_variables(CopyList,CLVars),
 351     variables(CLVars),
 352     entails_guard2(CopyList),
 353     !,test(CopyGuard),!,
 354     cleanup.
 355
 356 entails_guard2([]).
 357 entails_guard2([A|R]) :-
 358     known(A), entails_guard2(R).
 359
 360 simplify_guards(List,Body,GuardList,SimplifiedGuards,NewBody) :-
 361 %    write(starting),nl,
 362     copy_term_nat((List,GuardList),(CopyList,CopyGuard)),
 363     term_variables(CopyList,CLVars),
 364 %    write(variables(CLVars)),nl,
 365     variables(CLVars),
 366 %    write(gonna_add(CopyList)),nl,
 367     entails_guard2(CopyList),
 368 %    write(ok_gonna_add),nl,
 369     !,
 370 %    write(gonna_simplify(CopyGuard)),nl,
 371     simplify(CopyGuard,L),
 372 %    write(ok_gonna_simplify(CopyGuard,L)),nl,
 373     simplified(GuardList,L,SimplifiedGuards,Body,NewBody),
 374 %    write(ok_done),nl,
 375     !,
 376     cleanup.
 377
 378 simplified([],[],[],B,B).
 379 simplified([G|RG],[keep|RL],[G|RSG],B,NB) :- simplified(RG,RL,RSG,B,NB).
 380 simplified([G|RG],[fail|RL],fail,B,B).
 381 simplified([G|RG],[true|RL],[X|RSG],B,NB) :-
 382         builtins:binds_b(G,GVars), term_variables(RG,RGVars),
 383         intersect_eq(GVars,RGVars,SharedWithRestOfGuard),!,
 384         ( SharedWithRestOfGuard = []    ->
 385             term_variables(B,BVars),
 386             intersect_eq(GVars,BVars,SharedWithBody),!,
 387             ( SharedWithBody = []       ->
 388                 X=true,         % e.g. c(X) <=> Y=X | true.
 389                 NB=NB2
 390             ;
 391                 X=true,         % e.g. c(X) <=> Y=X | writeln(Y).
 392                 NB=(G,NB2)
 393             )
 394         ;
 395             X=G,                % e.g. c(X) <=> Y=X,p(Y) | true.
 396             NB=NB2
 397         ),
 398         simplified(RG,RL,RSG,B,NB2).
 399
 400 simplify([],[]).
 401 simplify([G|R],[SG|RS]) :-
 402     ( \+ try(true,G) ->
 403         SG = true
 404     ;
 405         builtins:negate_b(G,NotG),
 406         (\+ try(true,NotG) ->
 407             SG = fail
 408         ;
 409             SG = keep
 410         )
 411     ),
 412     known(G),
 413     simplify(R,RS).
 414
 415
 416 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 417 %%  AUXILIARY PREDICATES
 418 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 419
 420 try(A,X) :- (known(A) ->
 421                 true
 422             ;
 423                 format(' ERROR: entailment checker: this is not supposed to happen.\n',[])
 424             ),
 425          (test(X) ->
 426                 fail
 427             ;
 428                 true).
 429
 430
 431 lookup([],[],_,_) :- fail.
 432 lookup([K|R],[V|R2],X,Y) :-
 433     (X == K ->
 434         Y=V
 435     ;
 436         lookup(R,R2,X,Y)
 437     ).
 438
 439
 440 add_args_unif([],[],true).
 441 add_args_unif([X|RX],[Y|RY],(X=Y,RC)) :-
 442     add_args_unif(RX,RY,RC).
 443
 444 add_args_nunif([],[],fail).
 445 add_args_nunif([X|RX],[Y|RY],(X\=Y;RC)) :-
 446     add_args_nunif(RX,RY,RC).
 447
 448 add_args_nmatch([],[],fail).
 449 add_args_nmatch([X|RX],[Y|RY],(X\==Y;RC)) :-
 450     add_args_nmatch(RX,RY,RC).
 451
 452 all_unique_vars(T,V) :- all_unique_vars(T,V,[]).
 453
 454 all_unique_vars([],V,C).
 455 all_unique_vars([V|R],Vars,C) :-
 456     var(V),
 457     \+ memberchk_eq(V,Vars),
 458     \+ memberchk_eq(V,C),
 459     all_unique_vars(R,[V|C]).