guard_entailment.chr

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