This repository has been archived on 2023-08-20. You can view files and clone it, but cannot push or open issues or pull requests.
yap-6.3/LGPL/chr/guard_entailment.chr

460 lines
15 KiB
Plaintext
Raw Normal View History

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Author: Jon Sneyers
% Email: jon@cs.kuleuven.ac.be
% Copyright: K.U.Leuven 2004
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
:- module(guard_entailment,
[
entails_guard/2,
simplify_guards/5
]).
%:- use_module(library(chr)).
:- use_module(library(lists)).
:- use_module(hprolog).
:- use_module(builtins).
option(debug,off).
option(optimize,full).
:- constraints known/1,test/1,cleanup/0,variables/1.
% knowing the same thing twice is redundant
idempotence @ known(G) \ known(G) <=> true.
%--------------------------------------
% Rules to check if the argument of
% test/1 is entailed by known stuff
%--------------------------------------
% everything follows from an inconsistent theory
fail_implies_everything @ known(fail) \ test(X) <=> true.
% if it's known, it's entailed
trivial_entailment @ known(G) \ test(G) <=> true.
varfirst_nmatch @ test(X\==A) <=> nonvar(X) | test(A\==X).
distribute_nmatch @ test(X\==A) <=> nonvar(A),functor(A,Fu,Ar) |
A =.. [F|AArgs],
length(XArgs,Ar), B =.. [Fu|XArgs],
add_args_nmatch(XArgs,AArgs,ArgCond),
C = (\+ functor(X,Fu,Ar) ; (functor(X,Fu,Ar),X=B,ArgCond)),
test(C).
% eq implies leq
eq_implies_leq1 @ known(X=:=Y) \ test(X=<Y) <=> true.
eq_implies_leq2 @ known(X=:=Z) \ test(X=<Y) <=> number(Y), number(Z), Z=<Y |true.
eq_implies_leq3 @ known(X=:=Z) \ test(Y=<X) <=> number(Y), number(Z), Y=<Z |true.
% stronger inequality implies a weaker one
leq_implies_leq1 @ known(X=<Z) \ test(X=<Y) <=> number(Y), number(Z), Z=<Y |true.
leq_implies_leq2 @ known(X=<Y) \ test(Z=<Y) <=> number(X), number(Z), Z=<X | true.
% X =< Z implies X =\= Y for all Y > Z
leq_implies_neq1 @ known(X=<Z) \ test(X=\=Y) <=> number(Y), number(Z), Y>Z | true.
leq_implies_neq2 @ known(X=<Y) \ test(Y=\=Z) <=> number(X), number(Z), Z<X | true.
%--------------------------------------
% Rules to translate some stuff
%--------------------------------------
% we only want =<, =:= and =\=
known_g2l @ known(X>Y) <=> known(Y<X).
known_geq2leq @ known(X>=Y) <=> known(Y=<X).
known_l2leq_neq @ known(X<Y) <=> known(X=<Y), known(X=\=Y).
known_is2eq @ known(X is Y) <=> known(X=:=Y).
test_g2l @ test(X>Y) <=> test(Y<X).
test_geq2leq @test(X>=Y) <=> test(Y=<X).
test_l2leq_neq @test(X<Y) <=> test(((X=<Y),(X=\=Y))).
test_is2eq @ test(X is Y) <=> test(X=:=Y).
% propagate == and \== to =:= and =\= (which is a weaker statement)
match2eq1 @ known(X==Y) ==> number(X) | known(X=:=Y).
match2eq2 @known(X==Y) ==> number(Y) | known(X=:=Y).
nmatch2neq1 @ known(X\==Y) ==> number(X) | known(X=\=Y).
nmatch2neq2 @ known(X\==Y) ==> number(Y) | known(X=\=Y).
%--------------------------------------
% Rules to extend the known stuff
%--------------------------------------
% if we derived inconsistency, all other knowledge is redundant
fail_is_better_than_anything_else @ known(fail) \ known(_) <=> true.
% conjunctions
conj @ known((A,B)) <=> known(A), known(B).
% no need to remember trivial stuff
forget_trivial01 @ known(X=:=X) <=> true.
forget_trivial02 @ known(X==X) <=> true.
forget_trivial03 @ known(X=<X) <=> true.
forget_trivial04 @ known(X=X) <=> true.
%--------------------------------------
% Rules for = and \= (and functor)
%--------------------------------------
unify_vars1 @ known(X=Y) <=> var(X) | X=Y.
unify_vars2 @ known(X=Y) <=> var(Y) | X=Y.
%functor @ known(functor(X,F,A)) <=> var(X),ground(F),ground(A) | functor(X,F,A).
inconsistency4 @ known(X\=Y) <=> var(X),var(Y),X=Y | known(fail).
inconsistency4 @ known(X\=Y) <=> ground(X),ground(Y),X=Y | known(fail).
functor @ variables(V),known(functor(X,F,A)) <=>
var(X), ground(F), ground(A) |
functor(X,F,A),
X =.. [_|Args],
append(Args,V,NewV),
variables(NewV).
functor_inconsistency1 @ known(functor(X,F1,A1)) <=> nonvar(X), \+ functor(X,F1,A1) | known(fail).
negfunctor_trivial @ known(\+ functor(X,F1,A1)) <=> nonvar(X), functor(X,F1,A1) | known(fail).
functor_inconsistency2 @ known(functor(X,F1,A1)), known(functor(X,F2,A2)) <=>
nonvar(F1),nonvar(A1),nonvar(F2),nonvar(A2)
% (F1 \= F2 ; A1 \= A2) is entailed by idempotence
| known(fail).
nunify_inconsistency @ known(X\=X) <=> known(fail).
nonvar_unification @ known(X=Y) <=> nonvar(X), nonvar(Y),functor(X,F,A) |
( functor(Y,F,A),X=Y ->
true
;
known(fail)
).
nunify_expand @ known(X\=Y) <=> var(X),nonvar(Y), functor(Y,F,A), A>0 |
length(Args,A),
Y =.. [F|YArgs],
Y1 =.. [F|Args],
add_args_nunif(YArgs,Args,Nunif),
C = (\+ functor(X,F,A) ; (X = Y1, Nunif )),
known(C).
nunify_expand2 @ known(X\=Y) <=> nonvar(X),nonvar(Y), functor(X,F,A) |
(functor(Y,F,A) ->
X =.. [F|XArgs],
Y =.. [F|YArgs],
add_args_nunif(XArgs,YArgs,Nunif),
known(Nunif)
;
true
).
nunify_symmetry @ known(X\=Y) ==> known(Y\=X).
%--------------------------------------
% Rules for =<
%--------------------------------------
groundleq2 @ known(X=<Y) <=> number(X), number(Y), X>Y | known(fail).
% only keep the strictest inequality
remove_redundant_leq1 @ known(X=<Y) \ known(X=<Z) <=> number(Y), number(Z), Y=<Z | true.
remove_redundant_leq1 @ known(Z=<Y) \ known(X=<Y) <=> number(X), number(Z), X=<Z | true.
leq_antisymmetry @ known(X=<Y), known(Y=<X) <=> known(X=:=Y).
leq_transitivity @ known(X=<Y), known(Y=<Z) ==> known(X=<Z).
strict_leq_transitivity @ known(X=<Y),known(X=\=Y),known(Y=<Z),known(Y=\=Z) ==> known(X=\=Z).
%--------------------------------------
% Rules for =:= (and =\=)
%--------------------------------------
groundeq2 @ known(X=:=Y) <=> number(X), number(Y), X=\=Y | known(fail).
groundneq2 @ known(X=\=Y) <=> number(X), number(Y), X=:=Y | known(fail).
neq_inconsistency @ known(X=\=X) <=> known(fail).
inconsistency @ known(X=:=Y), known(X=\=Y) <=> known(fail).
eq_transitivity @ known(X=:=Y), known(Y=:=Z) ==> X \== Z | known(X=:=Z).
eq_symmetry @ known(X=:=Y) ==> known(Y=:=X).
neq_symmetry @ known(X=\=Y) ==> known(Y=\=X).
%--------------------------------------
% Rules for number/1, float/1, integer/1
%--------------------------------------
notnumber @ known(number(X)) <=> nonvar(X), \+ number(X) | known(fail).
notfloat @ known(float(X)) <=> nonvar(X), \+ float(X)| known(fail).
notinteger @ known(integer(X)) <=> nonvar(X), \+ integer(X) | known(fail).
int2number @ known(integer(X)) ==> known(number(X)).
float2number @ known(float(X)) ==> known(number(X)).
%--------------------------------------
% Rules for \+
%--------------------------------------
inconsistency2 @ known(X), known(\+ X) <=> known(fail).
%--------------------------------------
% Rules for == and \==
%--------------------------------------
inconsistency3 @ known(X\==Y), known(X==Y) <=> known(fail).
eq_transitivity2 @ known(X==Y), known(Y==Z) ==> known(X==Z).
neq_substitution @ known(X==Y), known(Y\==Z) ==> known(X\==Z).
eq_symmetry2 @ known(X==Y) ==> known(Y==X).
neq_symmetry2 @ known(X\==Y) ==> known(Y\==X).
neq_inconsistency @ known(X\==X) ==> known(fail).
functorsmatch@ known(X\==Y) <=> nonvar(X), nonvar(Y), functor(X,F,A) |
(functor(Y,F,A) ->
X =.. [F|XArgs],
Y =.. [F|YArgs],
add_args_nmatch(XArgs,YArgs,ArgCond),
known(ArgCond)
;
true
).
eq_implies_unif @ known(X==Y) ==> known(X=Y).
%--------------------------------------
% Rules for var/1 and nonvar/1
%--------------------------------------
ground2nonvar @ known(ground(X)) ==> known(nonvar(X)).
compound2nonvar @ known(compound(X)) ==> known(nonvar(X)).
atomic2nonvar @ known(atomic(X)) ==> known(nonvar(X)).
number2nonvar @ known(number(X)) ==> known(nonvar(X)).
atom2nonvar @ known(atom(X)) ==> known(nonvar(X)).
var_inconsistency @ known(var(X)), known(nonvar(X)) <=> known(fail).
%--------------------------------------
% Rules for disjunctions
%--------------------------------------
%ad-hoc disjunction optimization:
simplify_disj1 @ known(A) \ known((\+ A; B)) <=> known(B).
simplify_disj1b @ known(A) \ known((\+ A, C; B)) <=> known(B).
simplify_disj1c @ known(\+ A) \ known((A; B)) <=> known(B).
simplify_disj1d @ known(\+ A) \ known((A, C; B)) <=> known(B).
simplify_disj2 @ known((fail; B)) <=> known(B).
simplify_disj3 @ known((B ; fail)) <=> known(B).
simplify_disj4 @ known(functor(X,F1,A1)) \ known((\+ functor(X,F,A); B)) <=>
% F1 \== F or A1 \== A
true. % the disjunction does not provide any additional information
simplify_disj5 @ known((\+ functor(X,F,A); B)) <=>
nonvar(X), functor(X,F,A) |
known(B).
simplify_disj6 @ known((\+ functor(X,F,A); B)) <=>
nonvar(X), \+ functor(X,F,A) |
true. % the disjunction does not provide any additional information
test_simplify_disj1 @test((fail;B)) <=> test(B).
test_simplify_disj2 @test((B;fail)) <=> test(B).
%--------------------------------------
% Rules to test unifications
%--------------------------------------
trivial_unif @ test(X=Y) <=> X=Y | X=Y.
testgroundunif @ test(X=A) <=> ground(X),ground(A) | X=A.
varfirst @ test(X=A) <=> nonvar(X),var(A) | test(A=X).
distribute_unif @ variables(V) \ test(X=A) <=> var(X),nonvar(A),
functor(A,F,Arit),Arit>0,
A =.. [F|AArgs],\+ all_unique_vars(AArgs,V) |
C=(functor(X,F,Arit),X=A),
test(C).
distribute_unif2 @ test(X=A) <=> var(X),nonvar(A),
functor(A,F,Arit),%Arit>0,
A =.. [F|AArgs] % , all_unique_vars(AArgs)
|
C=functor(X,F,Arit),
test(C).
distribute_unif3 @ test(X=A) <=> nonvar(X),nonvar(A),functor(A,F,Arit),
A =.. [F|AArgs] |
functor(X,F,Arit),
X =.. [F|XArgs],
add_args_unif(XArgs,AArgs,ArgCond),
test(ArgCond).
testvarunif @ variables(V) \ test(X=A) <=> \+ (memberchk_eq(A,V),memberchk_eq(X,V)) | X=A.
testvarunif @ variables(V) \ test(functor(X,F,A)) <=>
var(X),ground(F),ground(A),\+ memberchk_eq(X,V) |
functor(X,F,A). % X is a singleton variable
% trivial truths
true_is_true @ test(true) <=> true.
trivial01 @ test(X==Y) <=> X==Y | true.
trivial02 @ test(X=:=Y) <=> X==Y | true.
trivial03 @ test(X=<Y) <=> X==Y | true.
trivial04 @ test(X=<Y) <=> ground(X), ground(Y), X=<Y | true.
trivial05 @ test(X=<Y) <=> ground(X), ground(Y), X>Y | fail.
trivial06 @ test(X=:=Y) <=> ground(X), ground(Y), X=:=Y | true.
trivial07 @ test(X=:=Y) <=> ground(X), ground(Y), X=\=Y | fail.
trivial08 @ test(X=\=Y) <=> ground(X), ground(Y), X=\=Y | true.
trivial09 @ test(X=\=Y) <=> ground(X), ground(Y), X=:=Y | fail.
trivial10 @ test(functor(X,F1,A1)) <=> nonvar(X), functor(X,F1,A1) | true.
trivial11 @ test(functor(X,F1,A1)) <=> nonvar(X) | fail.
trivial12 @ test(ground(X)) <=> ground(X) | true.
trivial13 @ test(number(X)) <=> number(X) | true.
trivial14 @ test(float(X)) <=> float(X) | true.
trivial15 @ test(integer(X)) <=> integer(X) | true.
trivial16 @ test(number(X)) <=> nonvar(X) | fail.
trivial17 @ test(float(X)) <=> nonvar(X) | fail.
trivial18 @ test(integer(X)) <=> nonvar(X) | fail.
trivial19 @ test(\+ functor(X,F1,A1)) <=> nonvar(X), functor(X,F1,A1) | fail.
trivial20 @ test(\+ functor(X,F1,A1)) <=> nonvar(X) | true.
trivial21 @ test(\+ ground(X)) <=> ground(X) | fail.
trivial22 @ test(\+ number(X)) <=> number(X) | fail.
trivial23 @ test(\+ float(X)) <=> float(X) | fail.
trivial24 @ test(\+ integer(X)) <=> integer(X) | fail.
trivial25 @ test(\+ number(X)) <=> nonvar(X) | true.
trivial26 @ test(\+ float(X)) <=> nonvar(X) | true.
trivial27 @ test(\+ integer(X)) <=> nonvar(X) | true.
test_conjunction @ test((A,B)) <=> test(A), known(A), test(B).
test_disjunction @ test((A;B)) <=> true | negate_b(A,NotA),negate_b(B,NotB),
(known(NotB),test(A) ; known(NotA),test(B)).
% disjunctions in the known stuff --> both options should entail the goals
% delay disjunction unfolding until everything is added, perhaps we can
% find entailed things without using the disjunctions
disjunction @ test(X), known((A;B)) <=>
true |
\+ try(A,X),!,
negate_b(A,NotA),
known(NotA),
\+ try(B,X).
% not entailed or entailment not detected
could_not_prove_entailment @ test(_) <=> fail.
clean_store1 @ cleanup \ known(_) <=> true.
clean_store2 @ cleanup \ variables(_) <=> true.
clean_store3 @ cleanup <=> true.
%--------------------------------------
% End of CHR part
%--------------------------------------
entails_guard(List,Guard) :-
copy_term_nat((List,Guard),(CopyList,CopyGuard)),
term_variables(CopyList,CLVars),
variables(CLVars),
entails_guard2(CopyList),
!,test(CopyGuard),!,
cleanup.
entails_guard2([]).
entails_guard2([A|R]) :-
known(A), entails_guard2(R).
simplify_guards(List,Body,GuardList,SimplifiedGuards,NewBody) :-
% write(starting),nl,
copy_term_nat((List,GuardList),(CopyList,CopyGuard)),
term_variables(CopyList,CLVars),
% write(variables(CLVars)),nl,
variables(CLVars),
% write(gonna_add(CopyList)),nl,
entails_guard2(CopyList),
% write(ok_gonna_add),nl,
!,
% write(gonna_simplify(CopyGuard)),nl,
simplify(CopyGuard,L),
% write(ok_gonna_simplify(CopyGuard,L)),nl,
simplified(GuardList,L,SimplifiedGuards,Body,NewBody),
% write(ok_done),nl,
!,
cleanup.
simplified([],[],[],B,B).
simplified([G|RG],[keep|RL],[G|RSG],B,NB) :- simplified(RG,RL,RSG,B,NB).
simplified([G|RG],[fail|RL],fail,B,B).
simplified([G|RG],[true|RL],[X|RSG],B,NB) :-
builtins:binds_b(G,GVars), term_variables(RG,RGVars),
intersect_eq(GVars,RGVars,SharedWithRestOfGuard),!,
( SharedWithRestOfGuard = [] ->
term_variables(B,BVars),
intersect_eq(GVars,BVars,SharedWithBody),!,
( SharedWithBody = [] ->
X=true, % e.g. c(X) <=> Y=X | true.
NB=NB2
;
X=true, % e.g. c(X) <=> Y=X | writeln(Y).
NB=(G,NB2)
)
;
X=G, % e.g. c(X) <=> Y=X,p(Y) | true.
NB=NB2
),
simplified(RG,RL,RSG,B,NB2).
simplify([],[]).
simplify([G|R],[SG|RS]) :-
( \+ try(true,G) ->
SG = true
;
builtins:negate_b(G,NotG),
(\+ try(true,NotG) ->
SG = fail
;
SG = keep
)
),
known(G),
simplify(R,RS).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% AUXILIARY PREDICATES
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
try(A,X) :- (known(A) ->
true
;
format(' ERROR: entailment checker: this is not supposed to happen.\n',[])
),
(test(X) ->
fail
;
true).
lookup([],[],_,_) :- fail.
lookup([K|R],[V|R2],X,Y) :-
(X == K ->
Y=V
;
lookup(R,R2,X,Y)
).
add_args_unif([],[],true).
add_args_unif([X|RX],[Y|RY],(X=Y,RC)) :-
add_args_unif(RX,RY,RC).
add_args_nunif([],[],fail).
add_args_nunif([X|RX],[Y|RY],(X\=Y;RC)) :-
add_args_nunif(RX,RY,RC).
add_args_nmatch([],[],fail).
add_args_nmatch([X|RX],[Y|RY],(X\==Y;RC)) :-
add_args_nmatch(RX,RY,RC).
all_unique_vars(T,V) :- all_unique_vars(T,V,[]).
all_unique_vars([],V,C).
all_unique_vars([V|R],Vars,C) :-
var(V),
\+ memberchk_eq(V,Vars),
\+ memberchk_eq(V,C),
all_unique_vars(R,[V|C]).