This repository has been archived on 2023-08-20. You can view files and clone it, but cannot push or open issues or pull requests.
yap-6.3/packages/gecode/clpfd.yap
2015-04-13 13:28:17 +01:00

1319 lines
34 KiB
Prolog
Raw Blame History

This file contains invisible Unicode characters

This file contains invisible Unicode characters that are indistinguishable to humans but may be processed differently by a computer. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

/**
@defgroup Gecode_and_ClPbBFDbC Programming Finite Domain Constraints in YAP/Gecode
@ingroup Gecode
@{
The gecode/clp(fd) interface is designed to use the GECODE functionality
in a more CLP like style. It requires
~~~~~{.prolog}
:- use_module(library(gecode/clpfd)).
~~~~~
Several example programs are available with the distribution.
Integer variables are declared as:
+ _V_ in _A_.. _B_
declares an integer variable _V_ with range _A_ to _B_.
+ _Vs_ ins _A_.. _B_
declares a set of integer variabless _Vs_ with range _A_ to _B_.
+ boolvar( _V_)
declares a boolean variable.
+ boolvars( _Vs_)
declares a set of boolean variable.
Constraints supported are:
*/
:- module(gecode_clpfd, [
op(100, yf, []),
op(760, yfx, #<==>),
op(750, xfy, #==>),
op(750, yfx, #<==),
op(740, yfx, #\/),
op(730, yfx, #\),
op(720, yfx, #/\),
op(710, fy, #\),
op(705, xfx, where),
op(700, xfx, #>),
op(700, xfx, #<),
op(700, xfx, #>=),
op(700, xfx, #=<),
op(700, xfx, #=),
op(700, xfx, #\=),
op(700, xf, #>),
op(700, xf, #<),
op(700, xf, #>=),
op(700, xf, #=<),
op(700, xf, #=),
op(700, xf, #\=),
op(500, yfx, '<=>'),
op(500, yfx, '=>'),
op(450, xfx, ..), % should bind more tightly than \/
(#>)/2,
(#<)/2,
(#>=)/2,
(#=<)/2,
(#=)/2,
(#\=)/2,
(#>)/1,
(#<)/1,
(#>=)/1,
(#=<)/1,
(#=)/1,
(#\=)/1,
(#<==>)/2,
(#==>)/2,
(#<==)/2,
(#\)/1,
(#\/)/2,
(#/\)/2,
in/2 ,
ins/2,
boolvar/1,
boolvars/1,
all_different/1,
all_distinct/1,
all_distinct/2,
maximize/1,
minimize/1,
sum/3,
lex_chain/1,
minimum/2,
min/2,
maximum/2,
max/2,
scalar_product/4,
element/2,
extensional_constraint/2,
in_relation/2,
clause/4,
dfa/4,
in_dfa/2,
in_dfa/4, /*
tuples_in/2, */
labeling/2 /*,
label/1,
indomain/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 */
]).
/** @pred _X_ #< _B_ is det
reified implication
As an example. consider finding out the people who wanted to sit
next to a friend and that are are actually sitting together:
~~~~~{.prolog}
preference_satisfied(X-Y, B) :-
abs(X - Y) #= 1 #<==> B.
~~~~~
Note that not all constraints may be reifiable.
*/
/** @pred _X_ #< _Y_ is semidet
smaller or equal
Arguments to this constraint may be an arithmetic expression with <tt>+</tt>,
<tt>-</tt>, <tt>\\*</tt>, integer division <tt>/</tt>, <tt>min</tt>, <tt>max</tt>, <tt>sum</tt>,
<tt>count</tt>, and
<tt>abs</tt>. Boolean variables support conjunction (/\), disjunction (\/),
implication (=>), equivalence (<=>), and xor. The <tt>sum</tt> constraint allows a two argument version using the
`where` conditional, in Zinc style.
The send more money equation may be written as:
~~~~~{.prolog}
1000*S + 100*E + 10*N + D +
1000*M + 100*O + 10*R + E #=
10000*M + 1000*O + 100*N + 10*E + Y,
~~~~~
This example uses `where` to select from
column _I_ the elements that have value under _M_:
~~~~~{.prolog}
OutFlow[I] #= sum(J in 1..N where D[J,I]<M, X[J,I])
~~~~~
The <tt>count</tt> constraint counts the number of elements that match a
certain constant or variable (integer sets are not available).
*/
/** @pred _X_ #<==> _B_ is det
reified equivalence
*/
/** @pred _X_ #= _Y_ is semidet
equality
*/
/** @pred _X_ #=< _Y_ is semidet
smaller
*/
/** @pred _X_ #==> _B_ is det
Reified implication
*/
/** @pred _X_ #> _Y_ is semidet
larger
*/
/** @pred _X_ #>= _Y_ is semidet
larger or equal
*/
/** @pred _X_ #\= _Y_ is semidet
disequality
*/
/** @pred labeling( _Opts_, _Xs_)
performs labeling, several variable and value selection options are
available. The defaults are `min` and `min_step`.
Variable selection options are as follows:
+ leftmost
choose the first variable
+ min
choose one of the variables with smallest minimum value
+ max
choose one of the variables with greatest maximum value
+ ff
choose one of the most constrained variables, that is, with the smallest
domain.
Given that we selected a variable, the values chosen for branching may
be:
+ min_step
smallest value
+ max_step
largest value
+ bisect
median
+ enum
all value starting from the minimum.
*/
/** @pred scalar_product(+ _Cs_, + _Vs_, + _Rel_, ? _V_ )
The product of constant _Cs_ by _Vs_ must be in relation
_Rel_ with _V_ .
*/
:- use_module(library(gecode)).
:- use_module(library(maplist)).
:- reexport(library(matrix), [(<==)/2, op(800, xfx, '<=='),
op(700, xfx, in),
op(700, xfx, ins),
op(450, xfx, ..), % should bind more tightly than \/
op(710, xfx, of),
foreach/2, foreach/4, of/2]).
% build array of constraints
%
matrix:array_extension(_.._ , gecode_clpfd:build).
build( I..J, _, Size, L) :-
length( L, Size ),
L ins I..J.
matrix:rhs_opaque(X) :- constraint(X).
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( min(_, _) ). %2,
constraint( minimum(_, _) ). %2,
constraint( max(_, _) ). %2,
constraint( maximum(_, _) ). %2,
constraint( in_relation(_, _) ). %2,
constraint( in_dfa(_, _) ). %2,
constraint( in_dfa(_, _, _, _) ). %2,
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( element(_, _) ). %2,
constraint( fd_var(_) ). %1,
constraint( fd_inf(_, _) ). %2,
constraint( fd_sup(_, _) ). %2,
constraint( fd_size(_, _) ). %2,
constraint( fd_dom(_, _) ). %2
constraint( clause(_, _, _, _) ). %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),
check(A, NA),
check(B, NB),
post( rel(NA, (#=), NB), Env, _).
( A #\= B) :-
get_home(Env),
check(A, NA),
check(B, NB),
post( rel(NA, (#\=), NB), Env, _).
( A #< B) :-
get_home(Env),
check(A, NA),
check(B, NB),
post( rel(NA, (#<), NB), Env, _).
( A #> B) :-
get_home(Env),
check(A, NA),
check(B, NB),
post( rel(NA, (#>), NB), Env, _).
( A #=< B) :-
get_home(Env),
check(A, NA),
check(B, NB),
post( rel(NA, (#=<), NB), Env, _).
( A #>= B) :-
get_home(Env),
check(A, NA),
check(B, NB),
post( rel(NA, (#>=), NB), Env, _).
( A #= ) :-
get_home(Env),
check(A, NA),
post( rel(NA, (#=)), Env, _).
/** @pred _X_ #= is det
all elements of _X_ must take the same value
*/
( A #\= ) :-
get_home(Env),
check(A, NA),
post( rel(NA, (#\=)), Env, _).
/** @pred _X_ #< is det
elements of _X_ must be decreasing or equal
*/
( A #< ) :-
get_home(Env),
check(A, NA),
post( rel(NA, (#<)), Env, _).
/** @pred _X_ #> is det
elements of _X_ must be increasing
*/
( A #> ) :-
get_home(Env),
check(A, NA),
post( rel(NA, (#>)), Env, _).
/** @pred _X_ #=< is det
elements of _X_ must be decreasing
*/
( A #=< ) :-
get_home(Env),
check(A, NA),
post( rel(NA, (#=<) ), Env, _).
/** @pred _X_ #>= is det
elements of _X_ must be increasinga or equal
*/
( A #>= ) :-
get_home(Env),
check(A, NA),
post( rel(NA, (#>=)), Env, _).
sum( L, Op, V) :-
get_home( Env ),
check(L, NL),
check(V, NV),
post( rel(sum(NL), Op, NV), Env, _).
( ( A #<==> VBool )) :-
get_home(Space-Map),
check(A, NA),
check(VBool, NVBool),
Bool := boolvar(Space),
m( NVBool, Bool, 0, 1, Map),
Space += reify(Bool, 'RM_EQV', R),
post(NA, Space-Map, R).
( A #==> VBool) :-
get_home(Space-Map),
check(A, NA),
check(VBool, NVBool),
Bool := boolvar(Space),
m( NVBool, Bool, 0, 1, Map),
Space += reify(Bool, 'RM_IMP', R),
post(NA, Space-Map, R).
( A #<== VBool) :-
get_home(Space-Map),
check(A, NA),
check(VBool, NVBool),
Bool := boolvar(Space),
m( NVBool, Bool, 0, 1, Map),
Space += reify(Bool, 'RM_PMI', R),
post(NA, Space-Map, R).
'#\\'(A) :-
get_home(Space-Map),
check(A, NA),
B := boolvar(Space),
Space += reify(B, 'RM_EQV', R),
Space += rel(B, 'BOT_EQV', 0),
post(NA, Space-Map, R).
( A1 #\/ A2 ) :-
get_home(Space-Map),
check(A1, NA1),
check(A2, NA2),
B1 := boolvar(Space),
B2 := boolvar(Space),
Space += reify(B1, 'RM_EQV', R1),
Space += reify(B2, 'RM_EQV', R2),
post(NA1, Space-Map, R1),
post(NA2, Space-Map, R2),
Space += rel(B1, B2, 'BOT_OR', 1).
( A1 #/\ A2 ) :-
get_home(Space-Map),
check(A1, NA1),
check(A2, NA2),
B1 := boolvar(Space),
B2 := boolvar(Space),
Space += reify(B1, 'RM_EQV', R1),
Space += reify(B2, 'RM_EQV', R2),
post(NA1, Space-Map, R1),
post(NA2, Space-Map, R2),
Space += rel(B1, B2, 'BOT_AND', 1).
( X in A..B) :-
get_home(Space-Map),
check(A, NA),
check(B, NB),
m(X, NX, NA, NB, Map),
NX := intvar(Space, NA, NB).
( Xs ins A..B) :-
get_home(Space-Map),
check(A, NA),
check(B, NB),
maplist(lm(NA, NB, Map), Xs, NXs),
length(Xs, N),
NXs := intvars(Space, N, NA, NB).
boolvar( X ) :-
get_home(Space-Map),
m(X, NX, 0, 1, Map),
NX := boolvar( Space ).
boolvars( Xs ) :-
get_home(Space-Map),
maplist(lm(0, 1, Map), Xs, NXs),
length(Xs, N),
NXs := boolvars( Space, N ).
/** @pred all_different( _Vs_ )
Verifies whether all elements of a list are different.
*/
all_different( Xs ) :-
get_home(Env),
check(Xs, NXs),
post( all_different( NXs ), Env, _ ).
all_distinct( Xs ) :-
get_home(Env),
check(Xs, NXs),
post( all_distinct( NXs ), Env, _ ).
all_distinct( Cs, Xs ) :-
get_home(Env),
check(Xs, NXs),
post( all_distinct( Cs, NXs ), Env, _ ).
scalar_product( Cs, Vs, Rels, X ) :-
get_home(Env),
check(Vs, NVs),
post( scalar_product( Cs, NVs, Rels, X ), Env, _ ).
lex_chain( Cs ) :-
get_home(Env),
check(Cs, NCs),
post( rel( NCs, '#=<' ), Env, _ ).
minimum( V, Xs ) :-
get_home(Env),
check(Xs, NXs),
check(V, NV),
post( rel( min(NXs), (#=), NV ), Env, _ ).
min( Xs, V ) :-
get_home(Env),
check(Xs, NXs),
check(V, NV),
post( rel( min(NXs), (#=), NV ), Env, _ ).
maximum( V, Xs ) :-
get_home(Env),
check(Xs, NXs),
check(V, NV),
post( rel( max(NXs), (#=), NV ), Env, _ ).
max( Xs, V ) :-
get_home(Env),
check(Xs, NXs),
check(V, NV),
post( rel( max(NXs), (#=), NV ), Env, _ ).
element( V, Xs ) :-
get_home(Env),
check(Xs, NXs),
check(V, NV),
post( element( NV, NXs ), Env, _ ).
in_relation( Xs, Rel ) :-
get_home(Env),
check(Xs, NXs),
post(in_tupleset(NXs, Rel), Env, _ ).
in_dfa( Xs, Rel ) :-
get_home(Env),
check(Xs, NXs),
post(in_dfa(NXs, Rel), Env, _ ).
in_dfa( Xs, S0, Ts, Fs ) :-
get_home(Env),
check(Xs, NXs),
post(in_dfa(NXs, S0, Ts, Fs), Env, _ ).
clause( and, Ps, Ns, V ) :-
get_home(Env),
check(Ps, NPs),
check(Ns, NNs),
check(V, NV),
post(clause( 'BOT_AND', NPs, NNs, NV), Env, _ ).
clause( or, Ps, Ns, V ) :-
get_home(Env),
check(Ps, NPs),
check(Ns, NNs),
check(V, NV),
post(clause( 'BOT_OR', NPs, NNs, NV), Env, _ ).
labeling(Opts, Xs) :-
get_home(Space-Map),
foldl2( processs_lab_opt, Opts, 'INT_VAR_SIZE_MIN', BranchVar, 'INT_VAL_MIN', BranchVal),
term_variables(Xs, Vs),
check( Vs, X1s ),
( X1s == [] -> true ;
maplist(ll(Map), X1s, NXs),
Space += branch(NXs, BranchVar, BranchVal) ).
processs_lab_opt(leftmost, _, 'INT_VAR_NONE', BranchVal, BranchVal).
processs_lab_opt(min, _, 'INT_VAR_SIZE_MIN', BranchVal, BranchVal).
processs_lab_opt(max, _, 'INT_VAR_SIZE_MAX', BranchVal, BranchVal).
processs_lab_opt(ff, _, 'INT_VAR_DEGREE_MIN', BranchVal, BranchVal).
processs_lab_opt(min_step, BranchVar, BranchVar, _, 'INT_VAL_MIN').
processs_lab_opt(max_step, BranchVar, BranchVar, _, 'INT_VAL_MIN').
processs_lab_opt(bisect, BranchVar, BranchVar, _, 'INT_VAL_MED').
processs_lab_opt(enum, BranchVar, BranchVar, _, 'INT_VALUES_MIN').
maximize(V) :-
get_home(Space-Map),
l(V, I, Map),
Space += maximize(I).
minimize(V) :-
get_home(Space-Map),
l(V, I, Map),
Space += minimize(I).
extensional_constraint( Tuples, TupleSet) :-
TupleSet := tupleset( Tuples ).
dfa( S0, Transitions, Finals, DFA) :-
DFA := dfa( S0, Transitions, Finals ).
check(V, NV) :-
( var(V) -> V = NV ;
number(V) -> V = NV ;
is_list(V) -> maplist(check, V, NV) ;
V = sum(_,_) -> V = NV ;
V = '[]'(Indx, Mat) -> NV <== '[]'(Indx, Mat) ;
V = '$matrix'(_, _, _, _, C) -> C =.. [_|L], maplist(check, L, NV) ;
V = A+B -> check(A,NA), check(B, NB), NV = NB+NA ;
V = A-B -> check(A,NA), check(B, NB), NV = NB-NA ;
arith(V, _) -> V =.. [C|L], maplist(check, L, NL), NV =.. [C|NL] ;
constraint(V) -> V =.. [C|L], maplist(check, L, NL), NV =.. [C|NL] ).
post( ( A #= B), Env, Reify) :-
post( rel( A, (#=), B), Env, Reify).
post( ( A #\= B), Env, Reify) :-
post( rel( A, (#\=), B), Env, Reify).
post( ( A #> B), Env, Reify) :-
post( rel( A, (#>), B), Env, Reify).
post( ( A #< B), Env, Reify) :-
post( rel( A, (#<), B), Env, Reify).
post( ( A #>= B), Env, Reify) :-
post( rel( A, (#>=), B), Env, Reify).
post( ( A #=< B), Env, Reify) :-
post( rel( A, (#=<), B), Env, Reify).
% [X,Y,Z] #<
post( rel( A, Op), Space-Map, Reify):-
( var( A ) -> l(A, IA, Map) ; checklist( var, A ) -> maplist(ll(Map), A, IA ) ),
gecode_arith_op( Op, GOP ),
(var(Reify) -> Space += rel(IA, GOP) ;
Space += rel(IA, GOP, Reify) ).
% X #< Y
% X #< 2
post( rel( A, Op, B), Space-Map, Reify):-
var(A),
( var(B) -> l(B, IB, Map) ; integer(B) -> IB = B ), !,
l(A, IA, Map),
gecode_arith_op( Op, GOP ),
(var(Reify) -> Space += rel(IA, GOP, IB) ;
Space += rel(IA, GOP, IB, Reify) ).
% 2 #\= B -> reverse
post( rel( A, Op, B), Space-Map, Reify) :-
( var(A) ; integer(A) ), !,
reverse_arith_op( Op, ROp ),
post( rel( B, ROp, A), Space-Map, Reify).
% A is never unbound
% [A,B,C,D] #< 3
post( rel( A, Op, B ), Space-Map, Reify):-
checklist( var, A ), !,
maplist(ll(Map), A, IL ),
( var(B) -> l(B, IB, Map) ; integer(B) -> IB = B ; equality(B, NB, Space-Map), l(NB, IB, Map) ), !,
gecode_arith_op( Op, GOP ),
(var(Reify) -> Space += rel(IL, GOP) ;
Space += rel(IL, GOP, IB) ).
% sum([A,B,C]) #= X
post( rel( sum(L), Op, Out), Space-Map, Reify):- !,
checklist( var, L ), !,
maplist(ll(Map), L, IL ),
( var(Out) -> l(Out, IOut, Map) ; integer(Out) -> IOut = Out ; equality(Out, NOut, Space-Map), l(NOut, IOut, Map) ),
gecode_arith_op( Op, GOP ),
(var(Reify) ->
Space += linear(IL, GOP, IOut);
Space += linear(IL, GOP, IOut, Reify)
).
% count([A,B,C], 3) #= X
post( rel( count(X, Y), Op, Out), Space-Map, Reify):- !,
( checklist( var, X ) -> maplist(ll(Map), X, IX ) ),
( var(Y) -> l(Y, IY, Map) ; integer(Y) -> IY = Y ; equality(Y, NY, Space-Map), l(NY, IY, Map) ),
( var(Out) -> l(Out, IOut, Map) ; integer(Out) -> IOut = Out ; equality(Out, NOut, Space-Map), l(NOut, IOut, Map) ), !,
gecode_arith_op( Op, GOP ),
(var(Reify) ->
Space += count(IX, IY, GOP, IOut);
Space += count(IX, IY, GOP, IOut, Reify)
).
% sum([I in 0..N-1, M[I]]) #= X
post( rel( sum(Foreach, Cond), Op, Out), Space-Map, Reify):- !,
( var(Out) -> l(Out, IOut, Map) ; integer(Out) -> IOut = Out ; equality(Out, NOut, Space-Map), l(NOut, IOut, Map) ),
cond2list( Foreach, Cond, Cs, L),
maplist(ll(Map), [Out|L], [IOut|IL] ),
gecode_arith_op( Op, GOP ),
(L = [] -> true ;
var(Reify) ->
Space += linear(Cs, IL, GOP, IOut);
Space += linear(Cs, IL, GOP, IOut, Reify)
).
post( rel(A1+A2, Op, B), Space-Map, Reify):-
( nonvar(B) ; B = _ + _ ; B = _-_), !,
linearize(A1+A2, 1, As, Bs, CAs, CBs, 0, A0, Space-Map),
linearize(B, -1, Bs, [], CBs, [], A0, B0, Space-Map),
gecode_arith_op( Op, GOP ),
(var(Reify) ->
( checklist(is_one, CAs) ->
Space += linear(As, GOP, B0);
Space += linear(CAs, As, GOP, B0)
)
;
( checklist(is_one, CAs) ->
Space += linear(As, GOP, B0, Reify);
Space += linear(CAs, As, GOP, B0, Reify)
)
).
post( rel(A1-A2, Op, B), Space-Map, Reify):-
( nonvar(B) ; B = _ + _ ; B = _-_), !,
linearize(A1-A2, 1, As, Bs, CAs, CBs, 0, A0, Space-Map),
linearize(B, -1, Bs, [], CBs, [], A0, B0, Space-Map),
gecode_arith_op( Op, GOP ),
(var(Reify) ->
( checklist(is_one, CAs) ->
Space += linear(As, GOP, B0);
Space += linear(CAs, As, GOP, B0)
)
;
( checklist(is_one, CAs) ->
Space += linear(As, GOP, B0, Reify);
Space += linear(CAs, As, GOP, B0, Reify)
)
).
post( rel(A, Op, B), Space-Map, Reify):-
arith(A, Name),
A =.. [_Op,A1],
is_list(A1), !,
( _Op = min -> true ; _Op = max ),
maplist(equality_l( Space-Map), A1, NA1),
maplist(in_c_l( Space-Map), NA1, VA1),
equality(B, B1, Space-Map),
out_c(Name, VA1, B1, Op, Space-Map, Reify).
post( rel(A, Op, B), Space-Map, Reify):-
arith(A, Name),
A =.. [_Op,A1], !,
equality(A1, NA1, Space-Map),
in_c(NA1, VA1, Space-Map), !,
equality(B, B1, Space-Map),
out_c(Name, VA1, B1, Op, Space-Map, Reify).
post( rel(A, Op, B), Space-Map, Reify):-
arith(A, Name),
A =.. [_Op,A1,A2], !,
equality(A1, NA1, Space-Map),
in_c(NA1, VA1, Space-Map),
equality(A2, NA2, Space-Map),
in_c(NA2, VA2, Space-Map),
equality(B, B1, Space-Map),
out_c(Name, VA1, VA2, B1, Op, Space-Map, Reify).
post( scalar_product(Cs, L, Op, Out), Space-Map, Reify):-
var(Out), !,
maplist(ll(Map), [Out|L], [IOut|IL] ),
gecode_arith_op( Op, GOP ),
(var(Reify) ->
Space += linear(Cs, IL, GOP, IOut);
Space += linear(Cs, IL, GOP, IOut, Reify)
).
post( scalar_product(Cs, L, Op, Out), Space-Map, Reify):-
integer(Out), !,
maplist(ll(Map), L, IL ),
gecode_arith_op( Op, GOP ),
(var(Reify) ->
Space += linear(Cs, IL, GOP, Out);
Space += linear(Cs, IL, GOP, Out, 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 )))
).
post(in_tupleset(Xs, Tuples), Space-Map, Reify) :-
is_list( Tuples ), !,
TS := tupleset( Tuples ),
maplist(ll(Map), Xs, IXs),
(var(Reify) ->
Space += extensional(IXs, TS)
;
throw(error(domain(not_reifiable),in_relation(Xs, Tuples)))
).
post(in_tupleset(Xs, TS), Space-Map, Reify) :-
maplist(ll(Map), Xs, IXs),
(var(Reify) ->
Space += extensional(IXs, TS)
;
throw(error(domain(not_reifiable),in_relation(Xs, TS)))
).
post(in_dfa(Xs, S0, Trs, Fs), Space-Map, Reify) :-
TS := dfa( S0, Trs, Fs ),
maplist(ll(Map), Xs, IXs),
(var(Reify) ->
Space += extensional(IXs, TS)
;
throw(error(domain(not_reifiable),in_dfa(Xs, S0, Trs, Fs)))
).
post(in_dfa(Xs, TS), Space-Map, Reify) :-
maplist(ll(Map), Xs, IXs),
(var(Reify) ->
Space += extensional(IXs, TS)
;
throw(error(domain(not_reifiable),in_dfa(Xs, TS)))
).
post(element(V, Xs), Space-Map, Reify) :-
l(V, IV, Map),
maplist(ll(Map), Xs, IXs),
(var(Reify) ->
Space += element(IV, IXs)
;
Space += element(IV, IXs, Reify)
).
post(clause( Type, Ps, Ns, V), Space-Map, Reify) :-
(integer(V) -> V = IV ; l(V, IV, Map) ),
maplist(ll(Map), Ps, IPs),
maplist(ll(Map), Ns, INs),
(var(Reify) ->
Space += clause(Type, IPs, INs, IV)
;
Space += clause(Type, IPs, INs, IV, Reify)
).
gecode_arith_op( (#=) , 'IRT_EQ' ).
gecode_arith_op( (#\=) , 'IRT_NQ' ).
gecode_arith_op( (#>) , 'IRT_GR' ).
gecode_arith_op( (#>=) , 'IRT_GQ' ).
gecode_arith_op( (#<) , 'IRT_LE' ).
gecode_arith_op( (#=<) , 'IRT_LQ' ).
reverse_arith_op( (#=) , (#=) ).
reverse_arith_op( (#\=) , (#\=) ).
reverse_arith_op( (#>) , (#<) ).
reverse_arith_op( (#>=) , (#=<) ).
reverse_arith_op( (#<) , (#>) ).
reverse_arith_op( (#=<) , (#>=) ).
linearize(V, C, [A|As], As, [C|CAs], CAs, I, I, _-Map) :-
var(V), !,
l(V, A, Map).
linearize(A+B, C, As, Bs, CAs, CBs, I, IF, Env) :-
linearize(A, C, As, A1s, CAs, CA1s, I, I1, Env),
linearize(B, C, A1s, Bs, CA1s, CBs, I1, IF, Env).
linearize(A-B, C, As, Bs, CAs, CBs, I, IF, Env) :-
NC is -C,
linearize(A, C, As, A1s, CAs, CA1s, I, I1, Env),
linearize(B, NC, A1s, Bs, CA1s, CBs, I1, IF, Env).
linearize(A, C, As, As, CAs, CAs, I, IF, _) :-
integer(A), !,
IF is I-C*A.
linearize(A, C, As, As, CAs, CAs, I, IF, _) :-
ground(A),
catch( (B is eval(A)), _, fail ), !,
IF is I-C*B.
linearize(C1*B, C, As, Bs, CAs, CBs, I, IF, Env) :-
integer(C1), !,
NC is C*C1,
linearize(B, NC, As, Bs, CAs, CBs, I, IF, Env).
linearize(B*C1, C, As, Bs, CAs, CBs, I, IF, Env) :-
integer(C1), !,
NC is C*C1,
linearize(B, NC, As, Bs, CAs, CBs, I, IF, Env).
linearize(AC, C, [A|Bs], Bs, [C|CBs], CBs, I, I, Env) :-
arith(AC, _),
equality(AC, V, Env),
Env = _-Map,
l(V, A, Map).
arith('/\\'(_,_), (/\)).
arith('\\/'(_,_), (\/)).
arith('=>'(_,_), (=>)).
arith('<=>'(_,_), (<=>)).
arith(xor(_,_), xor).
arith(abs(_), abs).
arith(min(_), min).
arith(max(_), max).
arith(min(_,_), min).
arith(max(_,_), max).
arith((_ * _), times).
arith((_ / _), div).
arith(sum(_), sum).
arith(sum(_,_), sum).
arith(count(_,_), count).
% replace abs(min(A,B)-max(A,B)) by
% min(A,B,A1), max(A,B,A2), linear([1,-1],[A1,B1],=,A3), abs(A3,AN)
equality(V, V, _Env) :-
var( V ), !.
equality(V, V, _Env) :-
integer( V ), !.
equality(abs(V), NV, Env) :-
equality(V, VA, Env),
new_arith(abs, VA, NV, Env).
equality(min(V), NV, Env) :-
maplist( equality_l(Env), V, VA ),
new_arith(min, VA, NV, Env).
equality(max(V), NV, Env) :-
maplist( equality_l(Env), V, VA ),
new_arith(max, VA, NV, Env).
equality(V1+V2, NV, Env) :-
equality(V1, V1A, Env),
equality(V2, V2A, Env),
new_arith( plus, V1A, V2A, NV, Env).
equality(V1-V2, NV, Env) :-
equality(V1, V1A, Env),
equality(V2, V2A, Env),
new_arith( minus, V1A, V2A, NV, Env).
equality(V1*V2, NV, Env) :-
equality(V1, V1A, Env),
equality(V2, V2A, Env),
new_arith( times, V1A, V2A, NV, Env).
equality(V1/V2, NV, Env) :-
equality(V1, V1A, Env),
equality(V2, V2A, Env),
new_arith( div, V1A, V2A, NV, Env).
equality(V1 mod V2, NV, Env) :-
equality(V1, V1A, Env),
equality(V2, V2A, Env),
new_arith( (mod), V1A, V2A, NV, Env).
equality(max( V1 , V2), NV, Env) :-
equality(V1, V1A, Env),
equality(V2, V2A, Env),
new_arith( (max), V1A, V2A, NV, Env).
equality(min( V1 , V2), NV, Env) :-
equality(V1, V1A, Env),
equality(V2, V2A, Env),
new_arith( (min), V1A, V2A, NV, Env).
equality(sum( V ), NV, Env) :-
maplist( equality_l(Env), V, VA ),
new_arith(sum, VA, NV, Env).
equality(sum( C, G ), NV, Env) :-
new_arith(sum, C, G, NV, Env).
equality('/\\'( V1 , V2), NV, Env) :-
equality(V1, V1A, Env),
equality(V2, V2A, Env),
new_arith( (/\), V1A, V2A, NV, Env).
equality('\\/'( V1 , V2), NV, Env) :-
equality(V1, V1A, Env),
equality(V2, V2A, Env),
new_arith( (\/), V1A, V2A, NV, Env).
equality('<=>'( V1 , V2), NV, Env) :-
equality(V1, V1A, Env),
equality(V2, V2A, Env),
new_arith( (<=>), V1A, V2A, NV, Env).
equality('=>'( V1 , V2), NV, Env) :-
equality(V1, V1A, Env),
equality(V2, V2A, Env),
new_arith( (=>), V1A, V2A, NV, Env).
equality('xor'( V1 , V2), NV, Env) :-
equality(V1, V1A, Env),
equality(V2, V2A, Env),
new_arith( (xor), V1A, V2A, NV, Env).
equality_l(Env, V0, V) :-
equality(V0, V, Env).
% abs(X) #= 3
out_c(Name, A1, B, Op, Space-Map, Reify) :-
integer(B), !,
new_arith( Name, A1, NB, Space-Map),
gecode_arith_op( Op, BOP ),
l(NB, IB, Map),
( var(Reify) ->
Space += rel(IB, BOP, B)
;
Space += rel(IB, BOP, B, Reify)
).
% abs(X) #= Cin[..]
out_c(Name, A1, B, (#=), Space-Map, Reify) :-
var(Reify),
l(B, IB, Map), !,
l(A1, IA1, Map),
G =.. [Name, IA1, IB],
Space += G.
% abs(X) #= NEW
out_c(Name, A1, B, (#=), Space-Map, Reify) :-
var(Reify), !,
new_arith( Name, A1, B, Space-Map).
% abs(X) #> NEW
out_c(Name, A1, B, Op, Space-Map, Reify) :-
l(B, IB0, Map), !,
new_arith( Name, A1, NB, Space-Map),
l(NB, IB, Map),
gecode_arith_op( Op, BOP ),
(
nonvar(Reify) ->
Space += rel(IB, BOP, IB0)
;
Space += rel(IB, BOP, IB0, Reify)
).
% X*Y #= 3
out_c(Name, A1, A2, B, Op, Space-Map, Reify) :-
integer(B), !,
new_arith( Name, A1, A2, NB, Space-Map),
l(NB, IB, Map),
gecode_arith_op( Op, BOP ),
( var(Reify) ->
Space += rel(IB, BOP, B)
;
Space += rel(IB, BOP, B, Reify)
).
% X*Y #= Cin[..]
out_c(Name, A1, A2, B, (#=), Space-Map, Reify) :-
var(Reify),
l(B, IB, Map), !,
l(A1, IA1, Map),
l(A2, IA2, Map),
G =.. [Name, IA1, IA2, IB],
Space += G.
% abs(X) #= NEW, cannot be reified
out_c(Name, A1, A2, B, (#=), Space-Map, Reify) :-
var(Reify), !,
new_arith( Name, A1, A2, B, Space-Map).
% min(X,Y) #= Cin[..] <=>
out_c(Name, A1, A2, B, Op, Space-Map, Reify) :-
l(B, IB0, Map), !,
new_arith( Name, A1, A2, NB, Space-Map),
l(NB, IB, Map),
gecode_arith_op( Op, BOP ),
( var(Reify) ->
Space += rel(IB, BOP, IB0)
;
Space += rel(IB, BOP, IB0, Reify)
).
new_arith( 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_arith( min, V, NV, Space-Map) :-
V = [V1|RV],
l(V1, _X1, Min0, Max0, Map),
foldl2( min_l(Map), RV, Max0, Max, Min0, Min),
NX := intvar(Space, Min, Max),
m(NV, NX, Min, Max, Map),
maplist(ll(Map), V, X),
Space += min(X, NX).
new_arith( max, V, NV, Space-Map) :-
V = [V1|RV],
l(V1, _X1, Min0, Max0, Map),
foldl2( max_l(Map), RV, Max0, Max, Min0, Min),
NX := intvar(Space, Min, Max),
m(NV, NX, Min, Max, Map),
maplist(ll(Map), V, X),
Space += min(X, NX).
new_arith( sum, V, NV, Space-Map) :-
foldl2( sum_l(Map), V, 0, Max, 0, Min),
NX := intvar(Space, Min, Max),
m(NV, NX, Min, Max, Map),
maplist(ll(Map), V, X),
Space += linear(X, 'IRT_EQ', NX).
new_arith( 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_arith( 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).
new_arith( min, V1, V2, NV, Space-Map) :-
l(V1, X1, Min1, Max1, Map),
l(V2, X2, Min2, Max2, Map),
Min is min(Min1,Min2),
Max is min(Max1,Max2),
NX := intvar(Space, Min, Max),
m(NV, NX, Min, Max, Map),
Space += min(X1, X2, NX).
new_arith( max, V1, V2, NV, Space-Map) :-
l(V1, X1, Min1, Max1, Map),
l(V2, X2, Min2, Max2, Map),
Min is max(Min1,Min2),
Max is max(Max1,Max2),
NX := intvar(Space, Min, Max),
m(NV, NX, Min, Max, Map),
Space += max(X1, X2, NX).
new_arith( times, V1, V2, NV, Space-Map) :-
l(V1, X1, Min1, Max1, Map),
l(V2, X2, Min2, Max2, Map),
min_times(Min1,Min2,Max1,Max2,Min),
max_times(Min1,Min2,Max1,Max2,Max),
NX := intvar(Space, Min, Max),
m(NV, NX, Min, Max, Map),
Space += times(X1, X2, NX).
new_arith( (div), V1, V2, NV, Space-Map) :-
l(V1, X1, Min1, Max1, Map),
l(V2, X2, Min2, Max2, Map),
min_div(Min1,Min2,Max1,Max2,Min),
max_div(Min1,Min2,Max1,Max2,Max),
NX := intvar(Space, Min, Max),
m(NV, NX, Min, Max, Map),
Space += div(X1, X2, NX).
new_arith( (mod), V1, V2, NV, Space-Map) :-
l(V1, X1, _Min1, Max1, Map),
l(V2, X2, _Min2, Max2, Map),
Min is 0,
Max is min(abs(Max1), Max2-1),
NX := intvar(Space, Min, Max),
m(NV, NX, Min, Max, Map),
Space += mod(X1, X2, NX).
new_arith( sum, Foreach, Cond, NV, Space-Map) :-
cond2list( Foreach, Cond, Cs, V),
foldl2( sum_l(Map), V, 0, Max, 0, Min),
NX := intvar(Space, Min, Max),
m(NV, NX, Min, Max, Map),
maplist(ll(Map), V, X),
Space += linear(Cs, X, 'IRT_EQ', NX).
new_arith( (/\), V1, V2, NV, Space-Map) :-
l(V1, X1, Map),
l(V2, X2, Map),
NX := boolvar(Space),
m(NV, NX, 0, 1, Map),
Space += rel(X1, 'BOT_AND', X2, NX).
new_arith( (\/), V1, V2, NV, Space-Map) :-
l(V1, X1, Map),
l(V2, X2, Map),
NX := boolvar(Space),
m(NV, NX, 0, 1, Map),
Space += rel(X1, 'BOT_OR', X2, NX).
new_arith( (=>), V1, V2, NV, Space-Map) :-
l(V1, X1, Map),
l(V2, X2, Map),
NX := boolvar(Space),
m(NV, NX, 0, 1, Map),
Space += rel(X1, 'BOT_IMP', X2, NX).
new_arith( (<=>), V1, V2, NV, Space-Map) :-
l(V1, X1, Map),
l(V2, X2, Map),
NX := boolvar(Space),
m(NV, NX, 0, 1, Map),
Space += rel(X1, 'BOT_EQV', X2, NX).
new_arith( xor, V1, V2, NV, Space-Map) :-
l(V1, X1, Map),
l(V2, X2, Map),
NX := boolvar(Space),
m(NV, NX, 0, 1, Map),
Space += rel(X1, 'BOT_XOR', X2, NX).
min_times(Min1,Min2,Max1,Max2,Min) :-
Min is min(Min1*Min2, min(Min1*Max2, min(Max1*Min2, Max1*Max2))).
max_times(Min1,Min2,Max1,Max2,Max) :-
Max is max(Min1*Min2, max(Min1*Max2, max(Max1*Min2, Max1*Max2))).
min_div(Min1,Min20,Max1,Max20,Min) :-
( Min20 == 0 -> Min2 = 1 ; Min2 = Min20),
( Max20 == 0 -> Max2 = -1; Max2 = Max20),
Min is min(Min1 div Min2, min(Min1 div Max2, min(Max1 div Min2, Max1 div Max2))).
max_div(Min1,Min20,Max1,Max20,Max) :-
( Min20 == 0 -> Min2 = 1 ; Min2 = Min20),
( Max20 == 0 -> Max2 = -1; Max2 = Max20),
Max is max(Min1 div Min2, max(Min1 div Max2, max(Max1 div Min2, Max1 div Max2))).
min_l(Map, V, Min0, Min, Max0, Max) :-
l(V, _, Min1, Max1, Map),
Min is min(Min0, Min1),
Max is min(Max0, Max1).
max_l(Map, V, Min0, Min, Max0, Max) :-
l(V, _, Min1, Max1, Map),
Min is max(Min0, Min1),
Max is max(Max0, Max1).
sum_l(Map, V, Min0, Min, Max0, Max) :-
l(V, _, Min1, Max1, Map),
Min is Min0 + Min1,
Max is Max0 + Max1.
in_c(A, A, _y) :-
var(A), !.
in_c(C, A, Space-Map) :-
integer(C),
Min is C-1,
NX := intvar(Space, Min, C),
m(A, NX, Min, C, Map),
Space += rel(NX, 'IRT_EQ', C).
in_c_l(Env, V, IV) :-
in_c(V, IV, Env).
user:term_expansion( ( H :- B), (H :- (gecode_clpfd:init_gecode(Space, Me), NB, gecode_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_done, false),
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),
b_setval(gecode_done, true),
CVs := val(SolSpace,IVs).
intvar(Map, V) :-
l(V, _IV, Map).
get_home(Home) :-
b_getval(gecode_space, Home).
cond2list((List where Goal), El, Cs, Vs) :- !,
foreach( List, add_el(Goal, El), ([])-([]), Cs-Vs ).
cond2list(List, El, Cs, Vs) :- !,
foreach( List, add_el(true, El), ([])-([]), Cs-Vs ).
add_el(G0, El, Cs-Vs, [C|Cs]-[V|Vs]) :-
call(G0), !,
E <== El,
( var(E) -> C = 1, E = V ; E = C*V, integer(C), var(V) -> true ; E = V*C, integer(C), var(V) ).
add_el(_G0, _El, Cs-Vs, Cs-Vs).
% An attributed variable with attribute value Domain has been
% assigned the value Y
attr_unify_hook(_, _) :-
b_getval(gecode_done, true), !.
attr_unify_hook(v(IV1,_,_), Y) :-
( get_attr(Y, gecode_clpfd, v(IV2,_,_))
->
nb_getval(gecode_space, Space-_),
( IV1 == IV2 -> true ;
Space += rel(IV1, 'IRT_EQ', IV2) )
; var(Y)
-> true
; integer(Y) ->
nb_getval(gecode_space, Space-_),
Space += rel(IV1, 'IRT_EQ', Y)
).
% Translate attributes from this module to residual goals
attribute_goals(X) -->
{ get_attr(X, gecode_clpfd, v(_,A,B)) },
[X in A..B].
m(X, Y, A, B, _Map) :-
put_attr(X, gecode_clpfd, v(Y, A, B)).
/*
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(V, IV, _) :-
get_attr(V, gecode_clpfd, v(IV, _, _)).
/*
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(V, IV, A, B, _) :-
get_attr(V, gecode_clpfd, v(IV, A, B)).
/*
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).
*/
is_one(1).
/**
@}
*/