1:- module(arith_partial_eval,[]). 2
21
26
27
29
30elim_term(A, B, 0) :- A==B.
31elim_term(A, B, X) :- nonvar(B, X+Y), A==Y.
32elim_term(A, B, Z+Y):- nonvar(B, X+Y), elim_term(A, X, Z).
34nonvar(X, Y):- nonvar(X), Y=X.
36ground_compound_basic_exp(E):- compound(E),
37 arg(1, E, A),
38 integer(A),
39 ( arg(2, E, B) -> integer(B)
40 ; true
41 ).
43arith_partial_eval(X, Y):- arith_rule(X, X0), !,
44 arith_partial_eval(X0, Y).
45arith_partial_eval(X, X).
47arith_rule(A, _) :- var(A), !, fail.
48arith_rule(A - B, A + -(B)).
49arith_rule(E*C, A*C+B*C) :- nonvar(E, A+B).
50arith_rule(C*E, C*A+C*B) :- nonvar(E, A+B).
51arith_rule(A+E, (A+B)+C) :- nonvar(E, B+C).
52arith_rule(A*E, (A*B)*C) :- nonvar(E, B*C).
53arith_rule(A+B, A0+B) :- arith_rule(A, A0).
54arith_rule(A+B, A+B0) :- arith_rule(B, B0).
55arith_rule(+(A), +(A0)) :- arith_rule(A, A0).
56arith_rule(-E, -A + -B) :- nonvar(E, A+B).
57arith_rule(-E, A) :- nonvar(E, -A).
58arith_rule(-(A), -(A0)) :- arith_rule(A, A0).
59arith_rule(E, V) :- ground_compound_basic_exp(E), V is E.
60arith_rule(A*B, A0*B) :- arith_rule(A, A0).
61arith_rule(A*B, A*B0) :- arith_rule(B, B0).
62arith_rule(A//B, A0//B) :- arith_rule(A, A0).
63arith_rule(A//B, A//B0) :- arith_rule(B, B0).
64arith_rule(A<<B, A0<<B) :- arith_rule(A, A0).
65arith_rule(A<<B, A<<B0) :- arith_rule(B, B0).
66arith_rule(A>>B, A0>>B) :- arith_rule(A, A0).
67arith_rule(A>>B, A>>B0) :- arith_rule(B, B0).
68arith_rule(A^B, A0^B) :- arith_rule(A, A0).
69arith_rule(A^B, A^B0) :- arith_rule(B, B0).
70arith_rule(A mod B, A0 mod B) :- arith_rule(A, A0).
71arith_rule(A mod B, A mod B0) :- arith_rule(B, B0).
72arith_rule(E*_, 0) :- E == 0.
73arith_rule(_*E, 0) :- E == 0.
74arith_rule(E+X, X) :- E == 0.
75arith_rule(X+E, X) :- E == 0.
76arith_rule(X>>E, X) :- E == 0.
77arith_rule(X<<E, X) :- E == 0.
78arith_rule(E//_, 0) :- E == 0.
79arith_rule(E*X, X) :- E == 1.
80arith_rule(X*E, X) :- E == 1.
81arith_rule(_^E, 1) :- E == 0.
82arith_rule(A^E, A) :- E == 1.
83arith_rule(E^_, 1) :- E == 1.
84arith_rule(A+B, B+A) :- integer(A).
85arith_rule(A*B, B*A) :- integer(A).
86arith_rule(A+B, B+A) :- nonvar(A, A0*H), nonvar(B, B0*K),
87 integer(H), integer(K),
88 A0 @< B0.
89arith_rule(A+B, A0*D) :- nonvar(A, A0*H), nonvar(B, B0*K),
90 A0 == B0,
91 D is H+K.
92arith_rule(A+B, B+A) :- arith_mono_compare(<, A, B).
93arith_rule(A+B, (U+B)+V) :- nonvar(A, U+V),
94 arith_mono_compare(<, V, B).
95
97arith_mono_compare(=, A, B):-integer(A), integer(B).
98arith_mono_compare(<, A, _):-integer(A).
99arith_mono_compare(>, _, B):-integer(B).
100arith_mono_compare(C, A, B):- nonvar(A, A0*I), nonvar(B, B0*K),
101 integer(I),
102 integer(K),
103 compare(C, B0, A0).
104arith_mono_compare(C, A, B):- nonvar(A, A0*I),
105 integer(I),
106 B0 = B,
107 compare(C, B0, A0).
108arith_mono_compare(C, A, B):- nonvar(B, B0*I),
109 integer(I),
110 A0 = A,
111 compare(C, B0, A0).
112arith_mono_compare(C, A, B):- compare(C, A, B)