SWI-Prolog / issues

Dummy repository for issue tracking
8 stars 3 forks source link

Same constraint matched twice in CHR-Rule #116

Open SRechenberger opened 2 years ago

SRechenberger commented 2 years ago

Given the program

:- use_module(library(chr)).
:- chr_option(check_guard_bindings, on).

:- op(700, xfx, eq).
:- chr_constraint eq/2.

% 1)
find(A*X, B*Y, 0) :- X==Y, !, A=B.
find(A*X, (Ps + B*Y), Ps) :- X==Y, !, A=B.
find(A*X, (Ps + B*Y), (P + B*Y)) :- X\==Y, !, find(A*X, Ps, P).

% 2)
normalize(B, E, R) :- number(B), !, R is -B/E.
normalize(A*X, E, R*X) :- R is -A/E, !.
normalize((P+A*X), E, (P1+R*X)) :- R is -A/E, !, normalize(P,E,P1). % mit P-A*X ?

% 3)
compute(B, A*X, (B+A*X)) :- number(B), !.
compute(B, A, R) :- number(B), number(A), !, R is B+A.
compute(B, (P+A*X), (R+A*X)) :- number(B), !, compute(B,P,R).

compute(B*Y, A*X, R*X) :- X==Y, !, R is B+A.
compute(B*Y, Ps, R) :- find(A*Y, Ps, Ps1), !, Res is A+B, R=(Ps1+Res*Y).
compute(B*Y, Ps, (Ps+B*Y)) :- \+find(_*Y, Ps, _), !.

compute((P+B*Y), Ps, (R+Res*Y)) :- find(A*Y, Ps, Ps1), !, Res is A+B, compute(P,Ps1,R).
compute((P+B*Y), Ps, (R+B*Y)) :- \+find(_*Y, Ps, _), !, compute(P,Ps,R).

eliminate @ (P1+A1*X) eq 0 \ (P2+A2*Y) eq 0 <=> X==Y | E is A2/A1, normalize(P1,E,Pres), compute(Pres,P2,P3), P3 eq 0.
B eq 0 <=> number(B) | B=0.

The query

?- (5+1*X+3*Y) eq 0, (8+2*Y+3*X) eq 0.

causes the first constraint of the query to be matched to both head-constraints of the rule eliminate:

?- (5+1*X+3*Y) eq 0, (8+2*Y+3*X) eq 0.
CHR:   (0) Insert: 5+1*_152668+3*_152688 eq 0 # <98>
CHR:   (1) Call: 5+1*_152668+3*_152688 eq 0 # <98> ? [creep]
CHR:   (1) Exit: 5+1*_152668+3*_152688 eq 0 # <98> ? [creep]
CHR:   (0) Insert: 8+2*_152688+3*_152668 eq 0 # <99>
CHR:   (1) Call: 8+2*_152688+3*_152668 eq 0 # <99> ? [creep]
CHR:   (1) Exit: 8+2*_152688+3*_152668 eq 0 # <99> ? [creep]
CHR:   (1) Wake: 5+1*_152668+3*_152688 eq 0 # <98> ? [creep]
CHR:   (1) Try: 5+1*_152668+3*_152688 eq 0 # <98> \ 5+1*_152668+3*_152688 eq 0 # <98> <=> _152688==_152688 | _158932 is 3/3,normalize(5+1*_152668,_158932,_158954),compute(_158954,5+1*_152668,_158968),_158968 eq 0.
CHR:   (1) Apply: 5+1*_152668+3*_152688 eq 0 # <98> \ 5+1*_152668+3*_152688 eq 0 # <98> <=> _152688==_152688 | _158932 is 3/3,normalize(5+1*_152668,_158932,_158954),compute(_158954,5+1*_152668,_158968),_158968 eq 0. ? [creep]
CHR:   (1) Remove: 5+1*_152668+3*_152688 eq 0 # <98>
CHR:   (1) Insert: 0+0*_152668 eq 0 # <100>
CHR:   (2) Call: 0+0*_152668 eq 0 # <100> ? [creep]
CHR:   (2) Try: 8+2*_152688+3*_152668 eq 0 # <99> \ 0+0*_152668 eq 0 # <100> <=> _152668==_152668 | _163300 is 0/3,normalize(8+2*_152688,_163300,_163322),compute(_163322,0,_163336),_163336 eq 0.
CHR:   (2) Apply: 8+2*_152688+3*_152668 eq 0 # <99> \ 0+0*_152668 eq 0 # <100> <=> _152668==_152668 | _163300 is 0/3,normalize(8+2*_152688,_163300,_163322),compute(_163322,0,_163336),_163336 eq 0. ? [creep]
CHR:   (2) Remove: 0+0*_152668 eq 0 # <100>
ERROR: Arithmetic: evaluation error: `zero_divisor'