instead of prdiv, use ptimes directly

This commit is contained in:
Markus Triska
2023-10-08 09:43:59 +02:00
parent 4d910f6bfe
commit 8121dce2a4

View File

@@ -2572,7 +2572,7 @@ parse_clpz(E, R,
m(A mod B) => [g(B #\= 0), p(pmod(A, B, R))],
m(A rem B) => [g(B #\= 0), p(prem(A, B, R))],
m(abs(A)) => [g(#R #>= 0), p(pabs(A, R))],
m(A/B) => [g(B #\= 0), p(prdiv(A, B, R))],
m(A/B) => [g(B #\= 0), p(ptimes(R, B, A))],
m(A//B) => [g(B #\= 0), p(ptzdiv(A, B, R))],
m(A div B) => [g(#R #= (A - (A mod B)) // B)],
m(A^B) => [p(pexp(A, B, R))],
@@ -4918,11 +4918,6 @@ run_propagator(ptimes(X,Y,Z), MState) -->
run_propagator(pdiv(X,Y,Z), MState) -->
{ kill(MState), Z #= (X-(X mod Y)) // Y }.
% X rdiv Y = Z
run_propagator(prdiv(X,Y,Z), MState) -->
{ kill(MState), Z*Y #= X }.
% X // Y = Z (round towards zero)
run_propagator(ptzdiv(X,Y,Z), MState) -->
( nonvar(X) ->
@@ -7786,7 +7781,6 @@ attribute_goal_(x_neq_y_plus_z(X,Y,Z)) --> [#X #\= #Y + #Z].
attribute_goal_(x_leq_y_plus_c(X,Y,C)) --> [#X #=< #Y + C].
attribute_goal_(ptzdiv(X,Y,Z)) --> [#X // #Y #= #Z].
attribute_goal_(pdiv(X,Y,Z)) --> [#X div #Y #= #Z].
attribute_goal_(prdiv(X,Y,Z)) --> [#X / #Y #= #Z].
attribute_goal_(pexp(X,Y,Z)) --> [#X ^ #Y #= #Z].
attribute_goal_(psign(X,Y)) --> [#Y #= sign(#X)].
attribute_goal_(pabs(X,Y)) --> [#Y #= abs(#X)].