Merge pull request #677 from notoria/clpz_mod

Made mod stronger and addressed #675
This commit is contained in:
Mark Thom
2020-08-15 13:55:48 -03:00
committed by GitHub

View File

@@ -4928,7 +4928,7 @@ run_propagator(pmod(X,Y,Z), MState) -->
( Y == 0 -> { false } ( Y == 0 -> { false }
; Y == Z -> { false } ; Y == Z -> { false }
% ; nonvar(Y), Z == X -> true % ; nonvar(Y), Z == X -> true
; X == Y -> kill(MState), Z = 0 ; X == Y -> kill(MState), queue_goal(Z = 0)
; true ; true
), ),
( nonvar(X), nonvar(Y) -> ( nonvar(X), nonvar(Y) ->
@@ -4940,20 +4940,20 @@ run_propagator(pmod(X,Y,Z), MState) -->
), ),
( { fd_get(X, _, n(XL), _, _) } -> ( { fd_get(X, _, n(XL), _, _) } ->
( (XL - Z) mod Y =\= 0 -> ( (XL - Z) mod Y =\= 0 ->
{ XMin is Z + Y * ((XL - Z) div Y + 1) } XMin is Z + Y * ((XL - Z) div Y + 1)
; { XMin is Z + Y * ((XL - Z) div Y) } ; XMin is XL
), ),
{ fd_get(X, XD0, XPs), { fd_get(X, XD0, XPs),
domain_remove_smaller_than(XD0, XMin, XD2), domain_remove_smaller_than(XD0, XMin, XD2) },
fd_put(X, XD2, XPs) } fd_put(X, XD2, XPs)
% queue_goal(X #>= XMin) % queue_goal(X #>= XMin)
; true ; true
), ),
( { fd_get(X, _, _, n(XU), _) } -> ( { fd_get(X, _, _, n(XU), _) } ->
{ XMax is Z + Y * ((XU - Z) div Y) }, XMax is Z + Y * ((XU - Z) div Y),
{ fd_get(X, XD1, XPs), { fd_get(X, XD1, XPs),
domain_remove_greater_than(XD1, XMax, XD3), domain_remove_greater_than(XD1, XMax, XD3) },
fd_put(X, XD3, XPs) } fd_put(X, XD3, XPs)
% queue_goal(X #=< XMax) % queue_goal(X #=< XMax)
; true ; true
) )
@@ -4973,14 +4973,14 @@ run_propagator(pmod(X,Y,Z), MState) -->
( Z > 0 -> ( Z > 0 ->
{ fd_get(Y, YD, YPs), { fd_get(Y, YD, YPs),
YMin is Z + 1, YMin is Z + 1,
domain_remove_smaller_than(YD, YMin, YD1), domain_remove_smaller_than(YD, YMin, YD1) },
fd_put(Y, YD1, YPs) } fd_put(Y, YD1, YPs)
% queue_goal(Y #> Z) % queue_goal(Y #> Z)
; Z < 0 -> ; Z < 0 ->
{ fd_get(Y, YD, YPs), { fd_get(Y, YD, YPs),
YMax is Z - 1, YMax is Z - 1,
domain_remove_greater_than(YD, YMax, YD1), domain_remove_greater_than(YD, YMax, YD1) },
fd_put(Y, YD1, YPs) } fd_put(Y, YD1, YPs)
% queue_goal(Y #< Z) % queue_goal(Y #< Z)
; true ; true
) )
@@ -4992,120 +4992,126 @@ run_propagator(pmod(X,Y,Z), MState) -->
run_propagator(pmodz(X,Y,Z), MState) --> run_propagator(pmodz(X,Y,Z), MState) -->
( nonvar(Z) -> true % Nothing to do. ( nonvar(Z) -> true % Nothing to do.
; nonvar(X) -> ; nonvar(X) ->
( X =:= 0 -> kill(MState), Z = X ( X =:= 0 -> kill(MState), queue_goal(Z = X)
; X > 0 -> ; ( X > 0 ->
( { fd_get(Y, _, n(YL), _, _), YL > X } -> ( { fd_get(Y, _, n(YL), _, _), YL > X } ->
kill(MState), kill(MState),
Z = X queue_goal(Z = X)
; { fd_get(Z, ZD0, ZPs), ; { fd_get(Z, ZD0, ZPs),
domain_remove_greater_than(ZD0, X, ZD2), domain_remove_greater_than(ZD0, X, ZD2) },
fd_put(Z, ZD2, ZPs) } fd_put(Z, ZD2, ZPs)
% queue_goal(Z #=< X) % queue_goal(Z #=< X)
)
; X < 0 ->
( { fd_get(Y, _, _, n(YU), _), YU < X } ->
kill(MState),
queue_goal(Z = X)
; { fd_get(Z, ZD0, ZPs),
domain_remove_smaller_than(ZD0, X, ZD2) },
fd_put(Z, ZD2, ZPs)
% queue_goal(Z #>= X)
)
),
( { fd_get(Y, _, n(YL), n(YU), _), YL > 0 } ->
ZMax is YU - 1,
{ fd_get(Z, ZD1, ZPs),
domain_remove_smaller_than(ZD1, 0, ZD3),
domain_remove_greater_than(ZD3, ZMax, ZD5) },
fd_put(Z, ZD5, ZPs)
% queue_goal(Z in 0..ZMax)
; { fd_get(Y, _, n(YL), n(YU), _), YU < 0 } ->
ZMin is YL + 1,
{ fd_get(Z, ZD1, ZPs),
domain_remove_greater_than(ZD1, 0, ZD3),
domain_remove_smaller_than(ZD3, ZMin, ZD5) },
fd_put(Z, ZD5, ZPs)
% queue_goal(Z in ZMin..0)
; true
) )
; X < 0 ->
( { fd_get(Y, _, _, n(YU), _), YU < X } ->
kill(MState),
Z = X
; { fd_get(Z, ZD0, ZPs),
domain_remove_smaller_than(ZD0, X, ZD2),
fd_put(Z, ZD2, ZPs) }
% queue_goal(Z #>= X)
)
),
( { fd_get(Y, _, n(YL), n(YU), _), YL > 0 } ->
{ ZMax is YU - 1 },
{ fd_get(Z, ZD1, ZPs),
domain_remove_smaller_than(ZD1, 0, ZD3),
domain_remove_greater_than(ZD3, ZMax, ZD5),
fd_put(Z, ZD5, ZPs) }
% queue_goal(Z in 0..ZMax)
; { fd_get(Y, _, n(YL), n(YU), _), YU < 0 } ->
{ ZMin is YL + 1 },
{ fd_get(Z, ZD1, ZPs),
domain_remove_greater_than(ZD1, 0, ZD3),
domain_remove_smaller_than(ZD3, ZMin, ZD5),
fd_put(Z, ZD5, ZPs) }
% queue_goal(Z in ZMin..0)
; true
) )
; nonvar(Y) -> ; nonvar(Y) ->
( abs(Y) =:= 1 -> kill(MState), Z = 0 ( abs(Y) =:= 1 -> kill(MState), queue_goal(Z = 0)
; Y < 0 -> ; Y < 0 ->
{ ZMin is Y + 1 }, ( { fd_get(X, _, n(XL), n(XU), _), XU =< 0, Y < XL } ->
{ fd_get(Z, ZD1, ZPs), kill(MState),
domain_remove_greater_than(ZD1, 0, ZD3), queue_goal(Z = X)
domain_remove_smaller_than(ZD3, ZMin, ZD5), ; ZMin is Y + 1,
fd_put(Z, ZD5, ZPs) } { fd_get(Z, ZD1, ZPs),
% queue_goal(Z in ZMin..0) domain_remove_greater_than(ZD1, 0, ZD3),
domain_remove_smaller_than(ZD3, ZMin, ZD5) },
fd_put(Z, ZD5, ZPs)
% queue_goal(Z in ZMin..0)
)
; Y > 0 -> ; Y > 0 ->
{ ZMax is Y - 1 }, ( { fd_get(X, _, n(XL), n(XU), _), XL >= 0, Y > XU } ->
{ fd_get(Z, ZD1, ZPs), kill(MState),
domain_remove_smaller_than(ZD1, 0, ZD3), queue_goal(Z = X)
domain_remove_greater_than(ZD3, ZMax, ZD5), ; ZMax is Y - 1,
fd_put(Z, ZD5, ZPs) } { fd_get(Z, ZD1, ZPs),
% queue_goal(Z in 0..ZMax) domain_remove_smaller_than(ZD1, 0, ZD3),
), domain_remove_greater_than(ZD3, ZMax, ZD5) },
( { fd_get(X, _, n(XL), n(XU), _), XL >= 0 } -> fd_put(Z, ZD5, ZPs)
{ fd_get(Z, ZD0, ZPs), % queue_goal(Z in 0..ZMax)
domain_remove_greater_than(ZD0, XU, ZD2), )
fd_put(Z, ZD2, ZPs) }
% queue_goal(Z #=< XU)
; { fd_get(X, _, n(XL), n(XU), _), XU =< 0 } ->
{ fd_get(Z, ZD0, ZPs),
domain_remove_smaller_than(ZD0, XL, ZD2),
fd_put(Z, ZD2, ZPs) }
% queue_goal(Z #>= XL)
; true
) )
; ( { fd_get(X, _, n(XL), n(XU), _), XL >= 0 } -> ; ( { fd_get(X, _, n(XL), n(XU), _), XL >= 0,
{ fd_get(Z, ZD0, ZPs), fd_get(Y, _, n(YL), _, _), XU < YL } ->
domain_remove_greater_than(ZD0, XU, ZD2), kill(MState),
fd_put(Z, ZD2, ZPs) } queue_goal(Z = X)
% queue_goal(Z #=< XU) ; { fd_get(X, _, n(XL), n(XU), _), XU =< 0,
; { fd_get(X, _, n(XL), n(XU), _), XU =< 0 } -> fd_get(Y, _, _, n(YU), _), XL > YU } ->
{ fd_get(Z, ZD0, ZPs), kill(MState),
domain_remove_smaller_than(ZD0, XL, ZD2), queue_goal(Z = X)
fd_put(Z, ZD2, ZPs) } ; ( { fd_get(X, _, n(XL), n(XU), _), XL >= 0 } ->
% queue_goal(Z #>= XL) { fd_get(Z, ZD0, ZPs),
; true domain_remove_greater_than(ZD0, XU, ZD2) },
), fd_put(Z, ZD2, ZPs)
( { fd_get(Y, _, n(YL), n(YU), _), YL > 0 } -> % queue_goal(Z #=< XU)
{ ZMax is YU - 1 }, ; { fd_get(X, _, n(XL), n(XU), _), XU =< 0 } ->
{ fd_get(Z, ZD1, ZPs), { fd_get(Z, ZD0, ZPs),
domain_remove_smaller_than(ZD1, 0, ZD3), domain_remove_smaller_than(ZD0, XL, ZD2) },
domain_remove_greater_than(ZD3, ZMax, ZD5), fd_put(Z, ZD2, ZPs)
fd_put(Z, ZD5, ZPs) } % queue_goal(Z #>= XL)
% queue_goal(Z in 0..ZMax) ; true
; { fd_get(Y, _, n(YL), n(YU), _), YU < 0 } -> ),
{ ZMin is YL + 1 }, ( { fd_get(Y, _, n(YL), n(YU), _), YL > 0 } ->
{ fd_get(Z, ZD1, ZPs), ZMax is YU - 1,
domain_remove_greater_than(ZD1, 0, ZD3), { fd_get(Z, ZD1, ZPs),
domain_remove_smaller_than(ZD3, ZMin, ZD5), domain_remove_smaller_than(ZD1, 0, ZD3),
fd_put(Z, ZD5, ZPs) } domain_remove_greater_than(ZD3, ZMax, ZD5) },
% queue_goal(Z in ZMin..0) fd_put(Z, ZD5, ZPs)
; { fd_get(Y, _, n(YL), n(YU), _) } -> % queue_goal(Z in 0..ZMax)
{ ZMin is YL + 1, ; { fd_get(Y, _, n(YL), n(YU), _), YU < 0 } ->
ZMax is YU - 1 }, ZMin is YL + 1,
{ fd_get(Z, ZD1, ZPs), { fd_get(Z, ZD1, ZPs),
domain_remove_greater_than(ZD1, ZMax, ZD3), domain_remove_greater_than(ZD1, 0, ZD3),
domain_remove_smaller_than(ZD3, ZMin, ZD5), domain_remove_smaller_than(ZD3, ZMin, ZD5) },
fd_put(Z, ZD5, ZPs) } fd_put(Z, ZD5, ZPs)
% queue_goal(Z in ZMin..ZMax) % queue_goal(Z in ZMin..0)
%/* This doesn't work very well. ; { fd_get(Y, _, n(YL), n(YU), _) } ->
; { fd_get(Y, _, _, n(YU), _), YU > 0 } -> ZMin is YL + 1,
{ fd_get(Z, ZD1, ZPs), ZMax is YU - 1,
ZMax is YU - 1, { fd_get(Z, ZD1, ZPs),
domain_remove_greater_than(ZD1, ZMax, ZD3), domain_remove_greater_than(ZD1, ZMax, ZD3),
fd_put(Z, ZD3, ZPs) } domain_remove_smaller_than(ZD3, ZMin, ZD5) },
% queue_goal(Z #< YU) fd_put(Z, ZD5, ZPs)
; { fd_get(Y, _, n(YL), _, _), YL < 0 } -> % queue_goal(Z in ZMin..ZMax)
{ fd_get(Z, ZD1, ZPs), %/* This doesn't work very well.
ZMin is YL + 1, ; { fd_get(Y, _, _, n(YU), _), YU > 0 } ->
domain_remove_smaller_than(ZD1, ZMin, ZD3), { fd_get(Z, ZD1, ZPs),
fd_put(Z, ZD3, ZPs) } ZMax is YU - 1,
% queue_goal(Z #> YL) domain_remove_greater_than(ZD1, ZMax, ZD3) },
% */ fd_put(Z, ZD3, ZPs)
; true % queue_goal(Z #< YU)
; { fd_get(Y, _, n(YL), _, _), YL < 0 } ->
{ fd_get(Z, ZD1, ZPs),
ZMin is YL + 1,
domain_remove_smaller_than(ZD1, ZMin, ZD3) },
fd_put(Z, ZD3, ZPs)
% queue_goal(Z #> YL)
% * /
; true
)
) )
). ).
@@ -5116,26 +5122,26 @@ run_propagator(pmody(X,Y,Z), MState) -->
( Z > 0 -> % queue_goal(Y #> Z) ( Z > 0 -> % queue_goal(Y #> Z)
{ fd_get(Y, YD, YPs), { fd_get(Y, YD, YPs),
YMin is Z + 1, YMin is Z + 1,
domain_remove_smaller_than(YD, YMin, YD1), domain_remove_smaller_than(YD, YMin, YD1) },
fd_put(Y, YD1, YPs) } fd_put(Y, YD1, YPs)
; Z < 0 -> % queue_goal(Y #< Z) ; Z < 0 -> % queue_goal(Y #< Z)
{ fd_get(Y, YD, YPs), { fd_get(Y, YD, YPs),
YMax is Z - 1, YMax is Z - 1,
domain_remove_greater_than(YD, YMax, YD1), domain_remove_greater_than(YD, YMax, YD1) },
fd_put(Y, YD1, YPs) } fd_put(Y, YD1, YPs)
; Z =:= 0 -> kill(MState), queue_goal(X / Y #= _) ; Z =:= 0 -> kill(MState), queue_goal(X / Y #= _)
) )
; ( { fd_get(Z, _, n(ZL), _, _), ZL > 0 } -> ; ( { fd_get(Z, _, n(ZL), _, _), ZL > 0 } ->
{ fd_get(Y, YD, YPs), { fd_get(Y, YD, YPs),
YMin is ZL + 1, YMin is ZL + 1,
domain_remove_smaller_than(YD, YMin, YD1), domain_remove_smaller_than(YD, YMin, YD1) },
fd_put(Y, YD1, YPs) } fd_put(Y, YD1, YPs)
% queue_goal(Y #> ZL) % queue_goal(Y #> ZL)
; { fd_get(Z, _, _, n(ZU), _), ZU < 0 } -> ; { fd_get(Z, _, _, n(ZU), _), ZU < 0 } ->
{ fd_get(Y, YD, YPs), { fd_get(Y, YD, YPs),
YMax is ZU - 1, YMax is ZU - 1,
domain_remove_greater_than(YD, YMax, YD1), domain_remove_greater_than(YD, YMax, YD1) },
fd_put(Y, YD1, YPs) } fd_put(Y, YD1, YPs)
% queue_goal(Y #< ZU) % queue_goal(Y #< ZU)
; true ; true
) )