4d94446c25
git-svn-id: https://yap.svn.sf.net/svnroot/yap/trunk@1416 b08c6af1-5177-4d33-ba66-4b1c6b8b522a
460 lines
15 KiB
Plaintext
460 lines
15 KiB
Plaintext
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
% 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]).
|