420 lines
11 KiB
Prolog
420 lines
11 KiB
Prolog
:- module(clpfd, [
|
|
op(760, yfx, #<==>),
|
|
op(750, xfy, #==>),
|
|
op(750, yfx, #<==),
|
|
op(740, yfx, #\/),
|
|
op(730, yfx, #\),
|
|
op(720, yfx, #/\),
|
|
op(710, fy, #\),
|
|
op(700, xfx, #>),
|
|
op(700, xfx, #<),
|
|
op(700, xfx, #>=),
|
|
op(700, xfx, #=<),
|
|
op(700, xfx, #=),
|
|
op(700, xfx, #\=),
|
|
op(700, xfx, in),
|
|
op(700, xfx, ins),
|
|
op(450, xfx, ..), % should bind more tightly than \/
|
|
(#>)/2,
|
|
(#<)/2,
|
|
(#>=)/2,
|
|
(#=<)/2,
|
|
(#=)/2,
|
|
(#\=)/2,
|
|
(#<==>)/2,
|
|
(#==>)/2,
|
|
(#<==)/2,
|
|
(#\)/1,
|
|
(#\/)/2,
|
|
(#/\)/2,
|
|
in/2 ,
|
|
ins/2,
|
|
all_different/1,
|
|
all_distinct/1,
|
|
all_distinct/2,
|
|
maximize/1,
|
|
sum/3, /*
|
|
scalar_product/4,
|
|
tuples_in/2, */
|
|
labeling/2 /*,
|
|
label/1,
|
|
indomain/1,
|
|
lex_chain/1,
|
|
serialized/2,
|
|
global_cardinality/2,
|
|
global_cardinality/3,
|
|
circuit/1,
|
|
element/3,
|
|
automaton/3,
|
|
automaton/8,
|
|
transpose/2,
|
|
zcompare/3,
|
|
chain/2,
|
|
fd_var/1,
|
|
fd_inf/2,
|
|
fd_sup/2,
|
|
fd_size/2,
|
|
fd_dom/2 */
|
|
]).
|
|
|
|
:- use_module(library(gecode)).
|
|
:- use_module(library(maplist)).
|
|
|
|
constraint( (_ #> _) ).
|
|
constraint( (_ #< _) ).
|
|
constraint( (_ #>= _) ).
|
|
constraint( (_ #=< _) ).
|
|
constraint( (_ #= _) ).
|
|
constraint( (_ #\= _) ).
|
|
constraint( (_ #\ _) ).
|
|
constraint( (_ #<==> _) ).
|
|
constraint( (_ #==> _) ).
|
|
constraint( (_ #<== _) ).
|
|
constraint( (_ #\/ _) ).
|
|
constraint( (_ #/\ _) ).
|
|
constraint( in(_, _) ). %2,
|
|
constraint( ins(_, _) ). %2,
|
|
constraint( all_different(_) ). %1,
|
|
constraint( all_distinct(_) ). %1,
|
|
constraint( all_distinct(_,_) ). %1,
|
|
constraint( sum(_, _, _) ). %3,
|
|
constraint( scalar_product(_, _, _, _) ). %4,
|
|
constraint( tuples_in(_, _) ). %2,
|
|
constraint( labeling(_, _) ). %2,
|
|
constraint( label(_) ). %1,
|
|
constraint( indomain(_) ). %1,
|
|
constraint( lex_chain(_) ). %1,
|
|
constraint( serialized(_, _) ). %2,
|
|
constraint( global_cardinality(_, _) ). %2,
|
|
constraint( global_cardinality(_, _, _) ). %3,
|
|
constraint( circuit(_) ). %1,
|
|
constraint( element(_, _, _) ). %3,
|
|
constraint( automaton(_, _, _) ). %3,
|
|
constraint( automaton(_, _, _, _, _, _, _, _) ). %8,
|
|
constraint( transpose(_, _) ). %2,
|
|
constraint( zcompare(_, _, _) ). %3,
|
|
constraint( chain(_, _) ). %2,
|
|
constraint( fd_var(_) ). %1,
|
|
constraint( fd_inf(_, _) ). %2,
|
|
constraint( fd_sup(_, _) ). %2,
|
|
constraint( fd_size(_, _) ). %2,
|
|
constraint( fd_dom(_, _) ). %2
|
|
|
|
|
|
|
|
process_constraints((B0,B1), (NB0, NB1), Env) :-
|
|
process_constraints(B0, NB0, Env),
|
|
process_constraints(B1, NB1, Env).
|
|
process_constraints(B, B, env(_Space)) :-
|
|
constraint(B), !.
|
|
process_constraints(B, B, _Env).
|
|
% process_constraint(B, NB, Space).
|
|
|
|
( A #= B) :-
|
|
get_home(Env),
|
|
post( (A #= B), Env, _).
|
|
( A #\= B) :-
|
|
get_home(Env),
|
|
post( (A #\= B), Env, _).
|
|
( A #< B) :-
|
|
get_home(Env),
|
|
post( (A #< B), Env, _).
|
|
( A #> B) :-
|
|
get_home(Env),
|
|
post( (A #< B), Env, _).
|
|
( A #=< B) :-
|
|
get_home(Env),
|
|
post( (A #=< B), Env, _).
|
|
( A #>= B) :-
|
|
get_home(Env),
|
|
post( (A #> B), Env, _).
|
|
sum( L, Op, V) :-
|
|
get_home( Env ),
|
|
post( sum(L, Op, V), Env, _).
|
|
( A #<==> VBool) :-
|
|
get_home(Space-Map),
|
|
Bool := boolvar(Space),
|
|
m( VBool, Bool, 0, 1, Map),
|
|
Space += reify(Bool, 'RM_EQV', R),
|
|
post(A, Space-Map, R).
|
|
( A #==> VBool) :-
|
|
get_home(Space-Map),
|
|
Bool := boolvar(Space),
|
|
m( VBool, Bool, 0, 1, Map),
|
|
Space += reify(Bool, 'RM_IMP', R),
|
|
post(A, Space-Map, R).
|
|
( A #<== VBool) :-
|
|
get_home(Space-Map),
|
|
Bool := boolvar(Space),
|
|
m( VBool, Bool, 0, 1, Map),
|
|
Space += reify(Bool, 'RM_PMI', R),
|
|
post(A, Space-Map, R).
|
|
'#\\'(A) :-
|
|
get_home(Space-Map),
|
|
B := boolvar(Space),
|
|
Space += reify(B, 'RM_EQV', R),
|
|
Space += rel(B, 'BOT_EQV', 0),
|
|
post(A, Space-Map, R).
|
|
( A1 #\/ A2 ) :-
|
|
get_home(Space-Map),
|
|
B1 := boolvar(Space),
|
|
B2 := boolvar(Space),
|
|
Space += reify(B1, 'RM_EQV', R1),
|
|
Space += reify(B2, 'RM_EQV', R2),
|
|
post(A1, Space-Map, R1),
|
|
post(A2, Space-Map, R2),
|
|
Space += rel(B1, B2, 'BOT_OR', 1).
|
|
( A1 #/\ A2 ) :-
|
|
get_home(Space-Map),
|
|
B1 := boolvar(Space),
|
|
B2 := boolvar(Space),
|
|
Space += reify(B1, 'RM_EQV', R1),
|
|
Space += reify(B2, 'RM_EQV', R2),
|
|
post(A1, Space-Map, R1),
|
|
post(A2, Space-Map, R2),
|
|
Space += rel(B1, B2, 'BOT_AND', 1).
|
|
( X in A..B) :-
|
|
get_home(Space-Map),
|
|
m(X, NX, A, B, Map),
|
|
NX := intvar(Space, A, B).
|
|
( Xs ins A..B) :-
|
|
get_home(Space-Map),
|
|
maplist(lm(A, B, Map), Xs, NXs),
|
|
length(Xs, N),
|
|
NXs := intvars(Space, N, A, B).
|
|
all_different( Xs ) :-
|
|
get_home(Env),
|
|
post( all_different( Xs ), Env, _ ).
|
|
all_distinct( Xs ) :-
|
|
get_home(Env),
|
|
post( all_distinct( Xs ), Env, _ ).
|
|
all_distinct( Cs, Xs ) :-
|
|
get_home(Env),
|
|
post( all_distinct( Cs, Xs ), Env, _ ).
|
|
labeling(_Opts, Xs) :-
|
|
get_home(Space-Map),
|
|
maplist(ll(Map), Xs, NXs),
|
|
Space += branch(NXs, 'INT_VAR_SIZE_MIN', 'INT_VAL_MIN').
|
|
maximize(V) :-
|
|
get_home(Space-Map),
|
|
l(V, I, Map),
|
|
Space += maximize(I).
|
|
|
|
post( (A #= B), Space-Map, Reify):-
|
|
integer(B),
|
|
linear(A, 1, [NA], [], [1], [], B, A0, Space-Map), !,
|
|
(var(Reify) ->
|
|
Space += rel(NA, 'IRT_EQ', A0);
|
|
Space += rel(NA, 'IRT_EQ', A0, Reify)
|
|
).
|
|
post( (A #= B), Space-Map, Reify):-
|
|
linear(A, 1, As, Bs, CAs, CBs, 0, A0, Space-Map),
|
|
linear(B, -1, Bs, [], CBs, [], A0, B0, Space-Map),
|
|
(var(Reify) ->
|
|
Space += linear(CAs, As, 'IRT_EQ', B0);
|
|
Space += linear(CAs, As, 'IRT_EQ', B0, Reify)
|
|
).
|
|
post( (A #\= B), Space-Map, Reify):-
|
|
linear(A, 1, As, Bs, CAs, CBs, 0, A0, Space-Map),
|
|
linear(B, -1, Bs, [], CBs, [], A0, B0, Space-Map),
|
|
(var(Reify) ->
|
|
Space += linear(CAs, As, 'IRT_NQ', B0);
|
|
Space += linear(CAs, As, 'IRT_NQ', B0, Reify)
|
|
).
|
|
post( (A #>B), Space-Map, Reify):-
|
|
linear(A, 1, As, Bs, CAs, CBs, 0, A0, Space-Map),
|
|
linear(B, -1, Bs, [], CBs, [], A0, B0, Space-Map),
|
|
(var(Reify) ->
|
|
Space += linear(CAs, As, 'IRT_GE', B0);
|
|
Space += linear(CAs, As, 'IRT_GE', B0, Reify)
|
|
).
|
|
post( (A #>=B), Space-Map, Reify):-
|
|
linear(A, 1, As, Bs, CAs, CBs, 0, A0, Space-Map),
|
|
linear(B, -1, Bs, [], CBs, [], A0, B0, Space-Map),
|
|
(var(Reify) ->
|
|
Space += linear(CAs, As, 'IRT_GQ', B0);
|
|
Space += linear(CAs, As, 'IRT_GQ', B0, Reify)
|
|
).
|
|
post( (A #<B), Space-Map, Reify):-
|
|
linear(A, 1, As, Bs, CAs, CBs, 0, A0, Space-Map),
|
|
linear(B, -1, Bs, [], CBs, [], A0, B0, Space-Map),
|
|
(var(Reify) ->
|
|
Space += linear(CAs, As, 'IRT_LE', B0);
|
|
Space += linear(CAs, As, 'IRT_LE', B0, Reify)
|
|
).
|
|
post( (A #=<B), Space-Map, Reify):-
|
|
linear(A, 1, As, Bs, CAs, CBs, 0, A0, Space-Map),
|
|
linear(B, -1, Bs, [], CBs, [], A0, B0, Space-Map),
|
|
(var(Reify) ->
|
|
Space += linear(CAs, As, 'IRT_LQ', B0);
|
|
Space += linear(CAs, As, 'IRT_LQ', B0, Reify)
|
|
).
|
|
post( sum(L, Op, Out), Space-Map, Reify):-
|
|
maplist(ll(Map), [Out|L], [IOut|IL] ),
|
|
gecode_arith_op( Op, GOP ),
|
|
(var(Reify) ->
|
|
Space += linear(IL, GOP, IOut);
|
|
Space += linear(IL, GOP, IOut, Reify)
|
|
).
|
|
post( all_different( Xs ), Space-Map, Reify) :-
|
|
maplist(ll(Map), Xs, NXs),
|
|
(var(Reify) ->
|
|
Space += distinct(NXs)
|
|
;
|
|
throw(error(domain(not_reifiable),all_different( Xs )))
|
|
).
|
|
post( all_distinct( Xs ), Space-Map, Reify) :-
|
|
maplist(ll(Map), Xs, NXs),
|
|
(var(Reify) ->
|
|
Space += distinct(NXs)
|
|
;
|
|
throw(error(domain(not_reifiable),all_distinct( Xs )))
|
|
).
|
|
post( all_distinct( Cs , Xs ), Space-Map, Reify) :-
|
|
maplist(ll(Map), Xs, NXs),
|
|
(var(Reify) ->
|
|
Space += distinct(Cs,NXs)
|
|
;
|
|
throw(error(domain(not_reifiable),all_distinct( Cs , Xs )))
|
|
).
|
|
|
|
gecode_arith_op( (#=) , 'IRT_EQ' ).
|
|
gecode_arith_op( (#\=) , 'IRT_NQ' ).
|
|
gecode_arith_op( (#>) , 'IRT_GE' ).
|
|
gecode_arith_op( (#>=) , 'IRT_GQ' ).
|
|
gecode_arith_op( (#<) , 'IRT_LE' ).
|
|
gecode_arith_op( (#=<) , 'IRT_LQ' ).
|
|
|
|
linear(V, C, [A|As], As, [C|CAs], CAs, I, I, _-Map) :-
|
|
var(V), !,
|
|
l(V, A, Map).
|
|
linear(A+B, C, As, Bs, CAs, CBs, I, IF, Env) :-
|
|
linear(A, C, As, A1s, CAs, CA1s, I, I1, Env),
|
|
linear(B, C, A1s, Bs, CA1s, CBs, I1, IF, Env).
|
|
linear(A-B, C, As, Bs, CAs, CBs, I, IF, Env) :-
|
|
NC is -C,
|
|
linear(A, C, As, A1s, CAs, CA1s, I, I1, Env),
|
|
linear(B, NC, A1s, Bs, CA1s, CBs, I1, IF, Env).
|
|
linear(A, C, As, As, CAs, CAs, I, IF, _) :-
|
|
integer(A), !,
|
|
IF is I-C*A.
|
|
linear(A, C, As, As, CAs, CAs, I, IF, _) :-
|
|
ground(A),
|
|
catch( (B is eval(A)), _, fail ), !,
|
|
IF is I-C*B.
|
|
linear(C1*B, C, As, Bs, CAs, CBs, I, IF, Env) :-
|
|
integer(C1), !,
|
|
NC is C*C1,
|
|
linear(B, NC, As, Bs, CAs, CBs, I, IF, Env).
|
|
linear(B*C1, C, As, Bs, CAs, CBs, I, IF, Env) :-
|
|
integer(C1), !,
|
|
NC is C*C1,
|
|
linear(B, NC, As, Bs, CAs, CBs, I, IF, Env).
|
|
linear(AC, C, [A|Bs], Bs, [C|CBs], CBs, I, I, Env) :-
|
|
arith(AC),
|
|
equality(AC, V, Env),
|
|
Env = _-Map,
|
|
l(V, A, Map).
|
|
|
|
arith(abs(_)).
|
|
arith(_ + _).
|
|
arith(_ - _).
|
|
|
|
equality(abs(V), NV, Env) :-
|
|
( var(V) -> VA = V ; equality(V, VA, Env) ),
|
|
new_abs(VA, NV, Env).
|
|
equality(V1+V2, NV, Env) :-
|
|
( var(V1) -> V1A = V1 ; equality(V1, V1A, Env) ),
|
|
( var(V2) -> V2A = V2 ; equality(V2, V2A, Env) ),
|
|
new_plus(V1A, V2A, NV, ENV).
|
|
equality(V1-V2, NV, Env) :-
|
|
( var(V1) -> V1A = V1 ; equality(V1, V1A, Env) ),
|
|
( var(V2) -> V2A = V2 ; equality(V2, V2A, Env) ),
|
|
new_minus(V1A, V2A, NV, Env).
|
|
|
|
new_abs( V, NV, Space-Map) :-
|
|
l(V, X, Min0, Max0, Map),
|
|
( Min0 < 0 ->
|
|
( Max0 < 0 -> Min is -Max0, Max is -Min0 ;
|
|
Min = 0 , Max is max( -Min0, Max0 ) )
|
|
;
|
|
Min = Min0, Max = Max0
|
|
),
|
|
NX := intvar(Space, Min, Max),
|
|
m(NV, NX, Min, Max, Map),
|
|
Space += abs(X, NX).
|
|
|
|
new_minus( V1, V2, NV, Space-Map) :-
|
|
l(V1, X1, Min1, Max1, Map),
|
|
l(V2, X2, Min2, Max2, Map),
|
|
Min is Min1-Max2,
|
|
Max is Max1-Min2,
|
|
NX := intvar(Space, Min, Max),
|
|
m(NV, NX, Min, Max, Map),
|
|
Space += linear([1,-1], [X1,X2], 'IRT_EQ', NX).
|
|
|
|
new_plus( V1, V2, NV, Space-Map) :-
|
|
l(V1, X1, Min1, Max1, Map),
|
|
l(V2, X2, Min2, Max2, Map),
|
|
Min is Min1+Min2,
|
|
Max is Max1+Max2,
|
|
NX := intvar(Space, Min, Max),
|
|
m(NV, NX, Min, Max, Map),
|
|
Space += linear([1,1], [X1,X2], 'IRT_EQ', NX).
|
|
|
|
|
|
user:term_expansion( ( H :- B), (H :- (clpfd:init_gecode(Space, Me), NB, clpfd:close_gecode(Space, Vs, Me)) ) ) :-
|
|
process_constraints(B, NB, Env),
|
|
term_variables(H, Vs),
|
|
nonvar( Env ), !,
|
|
Env = env( Space ).
|
|
|
|
init_gecode(Space, old) :-
|
|
nb_current(gecode_space, Space), nonvar(Space), !.
|
|
init_gecode(Space-Map, new) :-
|
|
Space := space,
|
|
b_setval(gecode_space, Space-Map).
|
|
|
|
close_gecode(_Space, _Vs, old) :- !.
|
|
close_gecode(Space-Map, Vs0, new) :-
|
|
term_variables(Vs0, Vs),
|
|
selectlist(intvar(Map), Vs, CVs),
|
|
maplist(ll(Map), CVs, IVs),
|
|
SolSpace := search(Space),
|
|
CVs := val(SolSpace,IVs).
|
|
|
|
intvar(Map, V) :-
|
|
l(V, _IV, Map).
|
|
|
|
get_home(Home) :-
|
|
b_getval(gecode_space, Home).
|
|
|
|
m(NV, OV, NA, NB, Vs) :-
|
|
var(Vs), !,
|
|
Vs = [v(NV,OV,NA,NB)|_].
|
|
m(NV, OV, NA, NB, [_|Vs]) :-
|
|
m(NV, OV, NA, NB, Vs).
|
|
|
|
lm(A, B, Map, X, Y) :-
|
|
m(X, Y, A, B, Map).
|
|
|
|
l(NV, OV, Vs) :-
|
|
var(Vs), !,
|
|
fail.
|
|
l(NV, OV, [v(V, OV, _A, _B)|_Vs]) :-
|
|
V == NV, !.
|
|
l(NV, OV, [_|Vs]) :-
|
|
l(NV, OV, Vs).
|
|
|
|
ll(Map, X, Y) :-
|
|
l(X, Y, Map).
|
|
|
|
l(NV, OV, _, _, Vs) :-
|
|
var(Vs), !,
|
|
fail.
|
|
l(NV, OV, A, B, [v(V, OV, A, B)|_Vs]) :-
|
|
V == NV, !.
|
|
l(NV, OV, A, B, [_|Vs]) :-
|
|
l(NV, OV, A, B, Vs).
|
|
|