rishi/scryer-prolog
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Merge pull request #2258 from triska/faster_scalar_product

Browse Source 
ENHANCED: Suspend propagation during filtering in scalar product constraints.
This commit is contained in:
Mark Thom
2024-01-01 00:33:36 -07:00
committed by GitHub
parent 1e0fa56786 62b61107e0
commit d713456e29
1 changed files with 102 additions and 99 deletions
Download Patch File Download Diff File Expand all files Collapse all files

117
src/lib/clpz.pl
View File

@@ -1015,6 +1015,9 @@ X in inf..sup.
needed to schedule the propagators! needed to schedule the propagators!
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
:- meta_predicate(duophrase(4, ?, ?)).
:- meta_predicate(duophrase(4, ?, ?, ?, ?)).
duophrase(NT, As, Bs) :- duophrase(NT, As, Bs) :-
duophrase(NT, As, [], Bs, []). duophrase(NT, As, [], Bs, []).
@@ -2409,22 +2412,22 @@ sum_finite_domains([C|Cs], [V|Vs], Inf0, Sup0, Inf, Sup) ++>
), ),
sum_finite_domains(Cs, Vs, Inf2, Sup2, Inf, Sup). sum_finite_domains(Cs, Vs, Inf2, Sup2, Inf, Sup).
remove_dist_upper_lower([], _, _, _). remove_dist_upper_lower([], _, _, _) --> [].
remove_dist_upper_lower([C|Cs], [V|Vs], D1, D2) :- remove_dist_upper_lower([C|Cs], [V|Vs], D1, D2) -->
( fd_get(V, VD, VPs) -> ( { fd_get(V, VD, VPs) } ->
( C < 0 -> ( C < 0 ->
domain_supremum(VD, n(Sup)), { domain_supremum(VD, n(Sup)),
L is Sup + D1//C, L is Sup + D1//C,
domain_remove_smaller_than(VD, L, VD1), domain_remove_smaller_than(VD, L, VD1),
domain_infimum(VD1, n(Inf)), domain_infimum(VD1, n(Inf)),
G is Inf - D2//C, G is Inf - D2//C,
domain_remove_greater_than(VD1, G, VD2) domain_remove_greater_than(VD1, G, VD2) }
; domain_infimum(VD, n(Inf)), ; { domain_infimum(VD, n(Inf)),
G is Inf + D1//C, G is Inf + D1//C,
domain_remove_greater_than(VD, G, VD1), domain_remove_greater_than(VD, G, VD1),
domain_supremum(VD1, n(Sup)), domain_supremum(VD1, n(Sup)),
L is Sup - D2//C, L is Sup - D2//C,
domain_remove_smaller_than(VD1, L, VD2) domain_remove_smaller_than(VD1, L, VD2) }
), ),
fd_put(V, VD2, VPs) fd_put(V, VD2, VPs)
; true ; true
@@ -2432,16 +2435,16 @@ remove_dist_upper_lower([C|Cs], [V|Vs], D1, D2) :-
remove_dist_upper_lower(Cs, Vs, D1, D2). remove_dist_upper_lower(Cs, Vs, D1, D2).
remove_dist_upper_leq([], _, _). remove_dist_upper_leq([], _, _) --> [].
remove_dist_upper_leq([C|Cs], [V|Vs], D1) :- remove_dist_upper_leq([C|Cs], [V|Vs], D1) -->
( fd_get(V, VD, VPs) -> ( { fd_get(V, VD, VPs) } ->
( C < 0 -> ( C < 0 ->
domain_supremum(VD, n(Sup)), { domain_supremum(VD, n(Sup)),
L is Sup + D1//C, L is Sup + D1//C,
domain_remove_smaller_than(VD, L, VD1) domain_remove_smaller_than(VD, L, VD1) }
; domain_infimum(VD, n(Inf)), ; { domain_infimum(VD, n(Inf)),
G is Inf + D1//C, G is Inf + D1//C,
domain_remove_greater_than(VD, G, VD1) domain_remove_greater_than(VD, G, VD1) }
), ),
fd_put(V, VD1, VPs) fd_put(V, VD1, VPs)
; true ; true
@@ -2449,18 +2452,18 @@ remove_dist_upper_leq([C|Cs], [V|Vs], D1) :-
remove_dist_upper_leq(Cs, Vs, D1). remove_dist_upper_leq(Cs, Vs, D1).
remove_dist_upper([], _). remove_dist_upper([], _) --> [].
remove_dist_upper([C*V|CVs], D) :- remove_dist_upper([C*V|CVs], D) -->
( fd_get(V, VD, VPs) -> ( { fd_get(V, VD, VPs) } ->
( C < 0 -> ( C < 0 ->
( domain_supremum(VD, n(Sup)) -> ( { domain_supremum(VD, n(Sup)) } ->
L is Sup + D//C, { L is Sup + D//C,
domain_remove_smaller_than(VD, L, VD1) domain_remove_smaller_than(VD, L, VD1) }
; VD1 = VD ; VD1 = VD
) )
; ( domain_infimum(VD, n(Inf)) -> ; ( { domain_infimum(VD, n(Inf)) } ->
G is Inf + D//C, { G is Inf + D//C,
domain_remove_greater_than(VD, G, VD1) domain_remove_greater_than(VD, G, VD1) }
; VD1 = VD ; VD1 = VD
) )
), ),
@@ -2469,18 +2472,18 @@ remove_dist_upper([C*V|CVs], D) :-
), ),
remove_dist_upper(CVs, D). remove_dist_upper(CVs, D).
remove_dist_lower([], _). remove_dist_lower([], _) --> [].
remove_dist_lower([C*V|CVs], D) :- remove_dist_lower([C*V|CVs], D) -->
( fd_get(V, VD, VPs) -> ( { fd_get(V, VD, VPs) } ->
( C < 0 -> ( C < 0 ->
( domain_infimum(VD, n(Inf)) -> ( { domain_infimum(VD, n(Inf)) } ->
G is Inf - D//C, { G is Inf - D//C,
domain_remove_greater_than(VD, G, VD1) domain_remove_greater_than(VD, G, VD1) }
; VD1 = VD ; VD1 = VD
) )
; ( domain_supremum(VD, n(Sup)) -> ; ( { domain_supremum(VD, n(Sup)) } ->
L is Sup - D//C, { L is Sup - D//C,
domain_remove_smaller_than(VD, L, VD1) domain_remove_smaller_than(VD, L, VD1) }
; VD1 = VD ; VD1 = VD
) )
), ),
@@ -2489,26 +2492,26 @@ remove_dist_lower([C*V|CVs], D) :-
), ),
remove_dist_lower(CVs, D). remove_dist_lower(CVs, D).
remove_upper([], _). remove_upper([], _) --> [].
remove_upper([C*X|CXs], Max) :- remove_upper([C*X|CXs], Max) -->
( fd_get(X, XD, XPs) -> ( { fd_get(X, XD, XPs) } ->
D is Max//C, D is Max//C,
( C < 0 -> ( C < 0 ->
domain_remove_smaller_than(XD, D, XD1) { domain_remove_smaller_than(XD, D, XD1) }
; domain_remove_greater_than(XD, D, XD1) ; { domain_remove_greater_than(XD, D, XD1) }
), ),
fd_put(X, XD1, XPs) fd_put(X, XD1, XPs)
; true ; true
), ),
remove_upper(CXs, Max). remove_upper(CXs, Max).
remove_lower([], _). remove_lower([], _) --> [].
remove_lower([C*X|CXs], Min) :- remove_lower([C*X|CXs], Min) -->
( fd_get(X, XD, XPs) -> ( { fd_get(X, XD, XPs) } ->
D is -Min//C, D is -Min//C,
( C < 0 -> ( C < 0 ->
domain_remove_greater_than(XD, D, XD1) { domain_remove_greater_than(XD, D, XD1) }
; domain_remove_smaller_than(XD, D, XD1) ; { domain_remove_smaller_than(XD, D, XD1) }
), ),
fd_put(X, XD1, XPs) fd_put(X, XD1, XPs)
; true ; true
@@ -4753,10 +4756,10 @@ run_propagator(scalar_product_neq(Cs0,Vs0,P0), MState) -->
) }. ) }.
run_propagator(scalar_product_leq(Cs0,Vs0,P0), MState) --> run_propagator(scalar_product_leq(Cs0,Vs0,P0), MState) -->
{ coeffs_variables_const(Cs0, Vs0, Cs, Vs, 0, I), { coeffs_variables_const(Cs0, Vs0, Cs, Vs, 0, I) },
P is P0 - I, P is P0 - I,
( Vs = [] -> kill(MState), P >= 0 ( Vs = [] -> kill(MState), P >= 0
; duophrase(sum_finite_domains(Cs, Vs, 0, 0, Inf, Sup), Infs, Sups), ; { duophrase(sum_finite_domains(Cs, Vs, 0, 0, Inf, Sup), Infs, Sups) },
D1 is P - Inf, D1 is P - Inf,
disable_queue, disable_queue,
( Infs == [], Sups == [] -> ( Infs == [], Sups == [] ->
@@ -4769,27 +4772,27 @@ run_propagator(scalar_product_leq(Cs0,Vs0,P0), MState) -->
; true ; true
), ),
enable_queue enable_queue
) }. ).
run_propagator(scalar_product_eq(Cs0,Vs0,P0), MState) --> run_propagator(scalar_product_eq(Cs0,Vs0,P0), MState) -->
{ coeffs_variables_const(Cs0, Vs0, Cs, Vs, 0, I), { coeffs_variables_const(Cs0, Vs0, Cs, Vs, 0, I) },
P is P0 - I, P is P0 - I,
( Vs = [] -> kill(MState), P =:= 0 ( Vs = [] -> kill(MState), P =:= 0
; Vs = [V], Cs = [C] -> kill(MState), P mod C =:= 0, V is P // C ; Vs = [V], Cs = [C] -> kill(MState), P mod C =:= 0, V is P // C
; Cs == [1,1] -> kill(MState), Vs = [A,B], A + B #= P ; Cs == [1,1] -> kill(MState), Vs = [A,B], { A + B #= P }
; Cs == [1,-1] -> kill(MState), Vs = [A,B], A #= P + B ; Cs == [1,-1] -> kill(MState), Vs = [A,B], { A #= P + B }
; Cs == [-1,1] -> kill(MState), Vs = [A,B], B #= P + A ; Cs == [-1,1] -> kill(MState), Vs = [A,B], { B #= P + A }
; Cs == [-1,-1] -> kill(MState), Vs = [A,B], P1 is -P, A + B #= P1 ; Cs == [-1,-1] -> kill(MState), Vs = [A,B], P1 is -P, { A + B #= P1 }
; P =:= 0, Cs == [1,1,-1] -> kill(MState), Vs = [A,B,C], A + B #= C ; P =:= 0, Cs == [1,1,-1] -> kill(MState), Vs = [A,B,C], { A + B #= C }
; P =:= 0, Cs == [1,-1,1] -> kill(MState), Vs = [A,B,C], A + C #= B ; P =:= 0, Cs == [1,-1,1] -> kill(MState), Vs = [A,B,C], { A + C #= B }
; P =:= 0, Cs == [-1,1,1] -> kill(MState), Vs = [A,B,C], B + C #= A ; P =:= 0, Cs == [-1,1,1] -> kill(MState), Vs = [A,B,C], { B + C #= A }
; duophrase(sum_finite_domains(Cs, Vs, 0, 0, Inf, Sup), Infs, Sups), ; { duophrase(sum_finite_domains(Cs, Vs, 0, 0, Inf, Sup), Infs, Sups) },
% nl, writeln(Infs-Sups-Inf-Sup), % { nl, writeln(Infs-Sups-Inf-Sup) },
D1 is P - Inf, D1 is P - Inf,
D2 is Sup - P, D2 is Sup - P,
disable_queue, disable_queue,
( Infs == [], Sups == [] -> ( Infs == [], Sups == [] ->
between(Inf, Sup, P), { between(Inf, Sup, P) },
remove_dist_upper_lower(Cs, Vs, D1, D2) remove_dist_upper_lower(Cs, Vs, D1, D2)
; Sups = [] -> P =< Sup, remove_dist_lower(Infs, D2) ; Sups = [] -> P =< Sup, remove_dist_lower(Infs, D2)
; Infs = [] -> Inf =< P, remove_dist_upper(Sups, D1) ; Infs = [] -> Inf =< P, remove_dist_upper(Sups, D1)
@@ -4801,7 +4804,7 @@ run_propagator(scalar_product_eq(Cs0,Vs0,P0), MState) -->
; true ; true
), ),
enable_queue enable_queue
) }. ).
% X + Y = Z % X + Y = Z
run_propagator(pplus(X,Y,Z,Morph), MState) --> run_propagator(pplus(X,Y,Z,Morph), MState) -->