diogo/yap-6.3
Archived
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

booleans and more fixes

Browse Source
This commit is contained in:
Vítor Santos Costa 2013-09-30 00:20:00 +01:00
parent 1ee58c5922
commit 937077d51b
3 changed files with 334 additions and 72 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

82
docs/yap.tex
View File

@ -9407,6 +9407,19 @@ in a more CLP like style. It requires
@end example @end example
Several example programs are available with the distribution. Several example programs are available with the distribution.
Integer variables are declared as:
@table @node
@var{V} in @var{A}..@var{B}
declares an integer variable @var{V} with range @var{A} to @var{B}.
@var{Vs} ins @var{A}..@var{B}
declares a set of integer variabless @var{Vs} with range @var{A} to @var{B}.
@boolvar{@var{V}}
declares a boolean variable.
@boolvars{@var{Vs}}
declares a set of boolean variable.
@end table
Constraints supported are: Constraints supported are:
@table @code @table @code
@item @var{X} #= @var{Y} @item @var{X} #= @var{Y}
@ -9423,8 +9436,10 @@ smaller
smaller or equal smaller or equal
Arguments to this constraint may be an arithmetic expression with @t{+}, Arguments to this constraint may be an arithmetic expression with @t{+},
@t{-}, @t{*}, integer division @t{/}, @t{min}, @t{max}, @t{sum}, and @t{-}, @t{*}, integer division @t{/}, @t{min}, @t{max}, @t{sum},
@t{abs}. The @t{sum} constraint allows a two argument version using the @t{count}, and
@t{abs}. Boolean variables support conjunction (/\), disjunction (\/),
implication (=>), equivalence (<=>), and xor. The @t{sum} constraint allows a two argument version using the
@code{where} conditional, in Zinc style. @code{where} conditional, in Zinc style.
The send more money equation may be written as: The send more money equation may be written as:
@ -9439,7 +9454,11 @@ column @var{I} the elements that have value under @var{M}:
@example @example
OutFlow[I] #= sum(J in 1..N where D[J,I]<M, X[J,I]) OutFlow[I] #= sum(J in 1..N where D[J,I]<M, X[J,I])
@end example @end example
@item all_different(@var{Vs})
The @t{count} constraint counts the number of elements that match a
certain constant or variable (integer sets are not available).
@item all_different(@var{Vs} )
@item all_distinct(@var{Vs}) @item all_distinct(@var{Vs})
@item all_different(@var{Cs}, @var{Vs}) @item all_different(@var{Cs}, @var{Vs})
@item all_distinct(@var{Cs}, @var{Vs}) @item all_distinct(@var{Cs}, @var{Vs})
@ -9474,6 +9493,25 @@ sudoku have a different value:
all_different(M[I*3+(0..2),J*3+(0..2)]) ), all_different(M[I*3+(0..2),J*3+(0..2)]) ),
@end example @end example
@item scalar_product(+@var{Cs}, +@var{Vs}, +@var{Rel}, ?@var{V} )
The product of constant @var{Cs} by @var{Vs} must be in relation
@var{Rel} with @var{V} .
@item @var{X} #=
all elements of @var{X} must take the same value
@item @var{X} #\=
not all elements of @var{X} take the same value
@item @var{X} #>
elements of @var{X} must be increasing
@item @var{X} #>=
elements of @var{X} must be increasinga or equal
@item @var{X} #=<
elements of @var{X} must be decreasing
@item @var{X} #<
elements of @var{X} must be decreasing or equal
@item @var{X} #<==> @var{B} @item @var{X} #<==> @var{B}
reified equivalence reified equivalence
@item @var{X} #==> @var{B} @item @var{X} #==> @var{B}
@ -9489,6 +9527,14 @@ preference_satisfied(X-Y, B) :-
@end example @end example
Note that not all constraints may be reifiable. Note that not all constraints may be reifiable.
@item element(@var{X}, @var{Vs} )
@var{X} is an element of list @var{Vs}
@item clause(@var{Type}, @var{Ps} , @var{Ns}, , @var{V} )
If @var{Type} is @code{and} it is the conjunction of boolen variables
@var{Ps} and the negation of boolean variables @var{Ns} and must have
result @var{V}. If @var{Type} is @code{or} it is a disjunction.
@item DFA @item DFA
the interface allows creating and manipulation deterministic finite the interface allows creating and manipulation deterministic finite
automata. A DFA has a set of states, represented as integers automata. A DFA has a set of states, represented as integers
@ -9530,7 +9576,35 @@ All elements must be ordered.
The following predicates control search: The following predicates control search:
@table @code @table @code
@item labeling(@var{Opts}, @var{Xs}) @item labeling(@var{Opts}, @var{Xs})
performs labeling, currently options are not supported. performs labeling, several variable and value selection options are
available. The defaults are @code{min} and @code{min_step}.
Variable selection options are as follows:
@table @code
@item leftmost
choose the first variable
@item min
choose one of the variables with smallest minimum value
@item max
choose one of the variables with greatest maximum value
@item ff
choose one of the most constrained variables, that is, with the smallest
domain.
@end table
Given that we selected a variable, the values chosen for branching may
be:
@table @code
@item min_step
smallest value
@item max_step
largest value
@item bisect
median
@item enum
all value starting from the minimum.
@end table
@item maximize(@var{V}) @item maximize(@var{V})
maximise variable @var{V} maximise variable @var{V}

BIN
library/gecode/clp_examples/test.yap
View File

Binary file not shown.

324
library/gecode/clpfd.yap
View File

@ -14,8 +14,16 @@
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(700, xfx, in), op(700, xfx, in),
op(700, xfx, ins), op(700, xfx, ins),
op(500, yfx, '<=>'),
op(500, yfx, '=>'),
op(450, xfx, ..), % should bind more tightly than \/ op(450, xfx, ..), % should bind more tightly than \/
(#>)/2, (#>)/2,
(#<)/2, (#<)/2,
@ -23,6 +31,12 @@
(#=<)/2, (#=<)/2,
(#=)/2, (#=)/2,
(#\=)/2, (#\=)/2,
(#>)/1,
(#<)/1,
(#>=)/1,
(#=<)/1,
(#=)/1,
(#\=)/1,
(#<==>)/2, (#<==>)/2,
(#==>)/2, (#==>)/2,
(#<==)/2, (#<==)/2,
@ -31,6 +45,8 @@
(#/\)/2, (#/\)/2,
in/2 , in/2 ,
ins/2, ins/2,
boolvar/1,
boolvars/1,
all_different/1, all_different/1,
all_distinct/1, all_distinct/1,
all_distinct/2, all_distinct/2,
@ -43,8 +59,10 @@
maximum/2, maximum/2,
max/2, max/2,
scalar_product/4, scalar_product/4,
element/2,
extensional_constraint/2, extensional_constraint/2,
in_relation/2, in_relation/2,
clause/4,
dfa/4, dfa/4,
in_dfa/2, in_dfa/2,
in_dfa/4, /* in_dfa/4, /*
@ -124,11 +142,13 @@ constraint( automaton(_, _, _, _, _, _, _, _) ). %8,
constraint( transpose(_, _) ). %2, constraint( transpose(_, _) ). %2,
constraint( zcompare(_, _, _) ). %3, constraint( zcompare(_, _, _) ). %3,
constraint( chain(_, _) ). %2, constraint( chain(_, _) ). %2,
constraint( element(_, _) ). %2,
constraint( fd_var(_) ). %1, constraint( fd_var(_) ). %1,
constraint( fd_inf(_, _) ). %2, constraint( fd_inf(_, _) ). %2,
constraint( fd_sup(_, _) ). %2, constraint( fd_sup(_, _) ). %2,
constraint( fd_size(_, _) ). %2, constraint( fd_size(_, _) ). %2,
constraint( fd_dom(_, _) ). %2 constraint( fd_dom(_, _) ). %2
constraint( clause(_, _, _, _) ). %2
process_constraints((B0,B1), (NB0, NB1), Env) :- process_constraints((B0,B1), (NB0, NB1), Env) :-
@ -169,6 +189,30 @@ process_constraints(B, B, _Env).
check(A, NA), check(A, NA),
check(B, NB), check(B, NB),
post( rel(NA, (#>=), NB), Env, _). post( rel(NA, (#>=), NB), Env, _).
( A #= ) :-
get_home(Env),
check(A, NA),
post( rel(NA, (#=)), Env, _).
( A #\= ) :-
get_home(Env),
check(A, NA),
post( rel(NA, (#\=)), Env, _).
( A #< ) :-
get_home(Env),
check(A, NA),
post( rel(NA, (#<)), Env, _).
( A #> ) :-
get_home(Env),
check(A, NA),
post( rel(NA, (#>)), Env, _).
( A #=< ) :-
get_home(Env),
check(A, NA),
post( rel(NA, (#=<) ), Env, _).
( A #>= ) :-
get_home(Env),
check(A, NA),
post( rel(NA, (#>=)), Env, _).
sum( L, Op, V) :- sum( L, Op, V) :-
get_home( Env ), get_home( Env ),
check(L, NL), check(L, NL),
@ -240,6 +284,15 @@ sum( L, Op, V) :-
maplist(lm(NA, NB, Map), Xs, NXs), maplist(lm(NA, NB, Map), Xs, NXs),
length(Xs, N), length(Xs, N),
NXs := intvars(Space, N, NA, NB). 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 ).
all_different( Xs ) :- all_different( Xs ) :-
get_home(Env), get_home(Env),
check(Xs, NXs), check(Xs, NXs),
@ -280,6 +333,11 @@ max( Xs, V ) :-
check(Xs, NXs), check(Xs, NXs),
check(V, NV), check(V, NV),
post( rel( max(NXs), (#=), NV ), Env, _ ). 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 ) :- in_relation( Xs, Rel ) :-
get_home(Env), get_home(Env),
check(Xs, NXs), check(Xs, NXs),
@ -290,16 +348,39 @@ in_dfa( Xs, Rel ) :-
post(in_dfa(NXs, Rel), Env, _ ). post(in_dfa(NXs, Rel), Env, _ ).
in_dfa( Xs, S0, Ts, Fs ) :- in_dfa( Xs, S0, Ts, Fs ) :-
get_home(Env), get_home(Env),
check(NXs, NXs), check(Xs, NXs),
post(in_dfa(Xs, S0, Ts, Fs), Env, _ ). 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) :- labeling(Opts, Xs) :-
get_home(Space-Map), get_home(Space-Map),
foldl2( processs_lab_opt, Opts, 'INT_VAR_SIZE_MIN', BranchVar, 'INT_VAL_MIN', BranchVal),
term_variables(Xs, Vs), term_variables(Xs, Vs),
check( Vs, X1s ), check( Vs, X1s ),
( X1s == [] -> true ; ( X1s == [] -> true ;
maplist(ll(Map), X1s, NXs), maplist(ll(Map), X1s, NXs),
Space += branch(NXs, 'INT_VAR_SIZE_MIN', 'INT_VAL_MIN') ). 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) :- maximize(V) :-
get_home(Space-Map), get_home(Space-Map),
@ -348,6 +429,7 @@ post( rel( A, Op), Space-Map, Reify):-
gecode_arith_op( Op, GOP ), gecode_arith_op( Op, GOP ),
(var(Reify) -> Space += rel(IA, GOP) ; (var(Reify) -> Space += rel(IA, GOP) ;
Space += rel(IA, GOP, Reify) ). Space += rel(IA, GOP, Reify) ).
% X #< Y % X #< Y
% X #< 2 % X #< 2
post( rel( A, Op, B), Space-Map, Reify):- post( rel( A, Op, B), Space-Map, Reify):-
@ -358,44 +440,49 @@ post( rel( A, Op, B), Space-Map, Reify):-
(var(Reify) -> Space += rel(IA, GOP, IB) ; (var(Reify) -> Space += rel(IA, GOP, IB) ;
Space += rel(IA, GOP, IB, Reify) ). Space += rel(IA, GOP, IB, Reify) ).
% 2 #\= B % 2 #\= B -> reverse
post( rel( A, Op, B), Space-Map, Reify):- post( rel( A, Op, B), Space-Map, Reify) :-
var(B), integer(A), !, ( var(A) ; integer(A) ), !,
l(B, IB, Map), 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 ), gecode_arith_op( Op, GOP ),
(var(Reify) -> Space += rel(A, GOP, IB) ; (var(Reify) -> Space += rel(IL, GOP) ;
Space += rel(A, GOP, IB, Reify) ). Space += rel(IL, GOP, IB) ).
% sum([A,B,C]) #= X % sum([A,B,C]) #= X
post( rel( C, Op, Out), Space-Map, Reify):- post( rel( sum(L), Op, Out), Space-Map, Reify):- !,
nonvar(C), C = sum(L), checklist( var, L ), !,
checklist( var, L ), maplist(ll(Map), L, IL ),
( var(Out) -> l(Out, IOut, Map) ; integer(Out) -> IOut = Out ), !, ( var(Out) -> l(Out, IOut, Map) ; integer(Out) -> IOut = Out ; equality(Out, NOut, Space-Map), l(NOut, IOut, Map) ),
var(Out), !,
maplist(ll(Map), [Out|L], [IOut|IL] ),
gecode_arith_op( Op, GOP ), gecode_arith_op( Op, GOP ),
(var(Reify) -> (var(Reify) ->
Space += linear(IL, GOP, IOut); Space += linear(IL, GOP, IOut);
Space += linear(IL, GOP, IOut, Reify) Space += linear(IL, GOP, IOut, Reify)
). ).
% X #= sum([A,B,C])
post( rel( Out, Op, C), Space-Map, Reify):- % count([A,B,C], 3) #= X
nonvar(C), C = sum(L), post( rel( count(X, Y), Op, Out), Space-Map, Reify):- !,
checklist( var, L ), ( checklist( var, X ) -> maplist(ll(Map), X, IX ) ),
( var(Out) -> l(Out, IOut, Map) ; integer(Out) -> IOut = Out ), !, ( var(Y) -> l(Y, IY, Map) ; integer(Y) -> IY = Y ; equality(Y, NY, Space-Map), l(NY, IY, Map) ),
var(Out), !, ( var(Out) -> l(Out, IOut, Map) ; integer(Out) -> IOut = Out ; equality(Out, NOut, Space-Map), l(NOut, IOut, Map) ), !,
maplist(ll(Map), [Out|L], [IOut|IL] ),
gecode_arith_op( Op, GOP ), gecode_arith_op( Op, GOP ),
(var(Reify) -> (var(Reify) ->
Space += linear(IL, GOP, IOut); Space += count(IX, IY, GOP, IOut);
Space += linear(IL, GOP, IOut, Reify) Space += count(IX, IY, GOP, IOut, Reify)
). ).
% sum([I in 0..N-1, M[I]]) #= X % sum([I in 0..N-1, M[I]]) #= X
post( rel( C, Op, Out), Space-Map, Reify):- post( rel( sum(Foreach, Cond), Op, Out), Space-Map, Reify):- !,
nonvar(C), C = sum(Foreach, Cond), ( var(Out) -> l(Out, IOut, Map) ; integer(Out) -> IOut = Out ; equality(Out, NOut, Space-Map), l(NOut, IOut, Map) ),
( var(Out) -> l(Out, IOut, Map) ; integer(Out) -> IOut = Out ), !,
cond2list( Foreach, Cond, Cs, L), cond2list( Foreach, Cond, Cs, L),
maplist(ll(Map), [Out|L], [IOut|IL] ), maplist(ll(Map), [Out|L], [IOut|IL] ),
gecode_arith_op( Op, GOP ), gecode_arith_op( Op, GOP ),
@ -404,43 +491,10 @@ post( rel( C, Op, Out), Space-Map, Reify):-
Space += linear(Cs, IL, GOP, IOut); Space += linear(Cs, IL, GOP, IOut);
Space += linear(Cs, IL, GOP, IOut, Reify) Space += linear(Cs, IL, GOP, IOut, Reify)
). ).
post( rel( Out, Op, C), Space-Map, Reify):-
nonvar(C), C = sum(Foreach, Cond), post( rel(A1+A2, Op, B), Space-Map, Reify):-
( var(Out) -> l(Out, IOut, Map) ; integer(Out) -> IOut = Out ), !, ( nonvar(B) ; B = _ + _ ; B = _-_), !,
cond2list( Foreach, Cond, Cs, L), linearize(A1+A2, 1, As, Bs, CAs, CBs, 0, A0, Space-Map),
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)
).
% [A,B,C,D] #< 3
post( rel( A, Op, B ), Space-Map, Reify):-
checklist( var, A ), !,
( var(B) -> l(B, IB, Map) ; integer(B) -> IB = B ), !,
maplist(ll(Map), A, IL ),
gecode_arith_op( Op, GOP ),
(var(Reify) -> Space += rel(IL, GOP) ;
Space += rel(IL, GOP, IB) ).
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) ).
post( rel( A, Op, B), Space-Map, Reify):-
checklist( var, A ),
( var(B) -> l(B, IB, Map) ; integer(B) -> IB = B ), !,
maplist(ll(Map), A, IL ),
gecode_arith_op( Op, GOP ),
(var(Reify) -> Space += rel(IL, GOP, IB) ;
Space += rel(IL, GOP, IB, Reify) ).
post( rel(A, Op, B), Space-Map, Reify):-
( nonvar(A), ( A = _+_ ; A = _-_ ) ;
nonvar(B), ( B = _ + _ ; B = _-_) ), !,
linearize(A, 1, As, Bs, CAs, CBs, 0, A0, Space-Map),
linearize(B, -1, Bs, [], CBs, [], A0, B0, Space-Map), linearize(B, -1, Bs, [], CBs, [], A0, B0, Space-Map),
gecode_arith_op( Op, GOP ), gecode_arith_op( Op, GOP ),
(var(Reify) -> (var(Reify) ->
@ -454,8 +508,25 @@ post( rel(A, Op, B), Space-Map, Reify):-
Space += linear(CAs, 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):- post( rel(A, Op, B), Space-Map, Reify):-
nonvar(A),
arith(A, Name), arith(A, Name),
A =.. [_Op,A1], A =.. [_Op,A1],
is_list(A1), !, is_list(A1), !,
@ -464,16 +535,16 @@ post( rel(A, Op, B), Space-Map, Reify):-
maplist(in_c_l( Space-Map), NA1, VA1), maplist(in_c_l( Space-Map), NA1, VA1),
equality(B, B1, Space-Map), equality(B, B1, Space-Map),
out_c(Name, VA1, B1, Op, Space-Map, Reify). out_c(Name, VA1, B1, Op, Space-Map, Reify).
post( rel(A, Op, B), Space-Map, Reify):- post( rel(A, Op, B), Space-Map, Reify):-
nonvar(A),
arith(A, Name), arith(A, Name),
A =.. [_Op,A1], !, A =.. [_Op,A1], !,
equality(A1, NA1, Space-Map), equality(A1, NA1, Space-Map),
in_c(NA1, VA1, Space-Map), !, in_c(NA1, VA1, Space-Map), !,
equality(B, B1, Space-Map), equality(B, B1, Space-Map),
out_c(Name, VA1, B1, Op, Space-Map, Reify). out_c(Name, VA1, B1, Op, Space-Map, Reify).
post( rel(A, Op, B), Space-Map, Reify):- post( rel(A, Op, B), Space-Map, Reify):-
nonvar(A),
arith(A, Name), arith(A, Name),
A =.. [_Op,A1,A2], !, A =.. [_Op,A1,A2], !,
equality(A1, NA1, Space-Map), equality(A1, NA1, Space-Map),
@ -482,6 +553,7 @@ post( rel(A, Op, B), Space-Map, Reify):-
in_c(NA2, VA2, Space-Map), in_c(NA2, VA2, Space-Map),
equality(B, B1, Space-Map), equality(B, B1, Space-Map),
out_c(Name, VA1, VA2, B1, Op, Space-Map, Reify). out_c(Name, VA1, VA2, B1, Op, Space-Map, Reify).
post( scalar_product(Cs, L, Op, Out), Space-Map, Reify):- post( scalar_product(Cs, L, Op, Out), Space-Map, Reify):-
var(Out), !, var(Out), !,
maplist(ll(Map), [Out|L], [IOut|IL] ), maplist(ll(Map), [Out|L], [IOut|IL] ),
@ -551,6 +623,25 @@ post(in_dfa(Xs, TS), Space-Map, Reify) :-
throw(error(domain(not_reifiable),in_dfa(Xs, 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_EQ' ).
gecode_arith_op( (#\=) , 'IRT_NQ' ). gecode_arith_op( (#\=) , 'IRT_NQ' ).
gecode_arith_op( (#>) , 'IRT_GR' ). gecode_arith_op( (#>) , 'IRT_GR' ).
@ -558,6 +649,13 @@ gecode_arith_op( (#>=) , 'IRT_GQ' ).
gecode_arith_op( (#<) , 'IRT_LE' ). gecode_arith_op( (#<) , 'IRT_LE' ).
gecode_arith_op( (#=<) , 'IRT_LQ' ). 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) :- linearize(V, C, [A|As], As, [C|CAs], CAs, I, I, _-Map) :-
var(V), !, var(V), !,
l(V, A, Map). l(V, A, Map).
@ -589,6 +687,11 @@ linearize(AC, C, [A|Bs], Bs, [C|CBs], CBs, I, I, Env) :-
Env = _-Map, Env = _-Map,
l(V, A, Map). l(V, A, Map).
arith('/\\'(_,_), (/\)).
arith('\\/'(_,_), (\/)).
arith('=>'(_,_), (=>)).
arith('<=>'(_,_), (<=>)).
arith(xor(_,_), xor).
arith(abs(_), abs). arith(abs(_), abs).
arith(min(_), min). arith(min(_), min).
arith(max(_), max). arith(max(_), max).
@ -597,6 +700,8 @@ arith(max(_,_), max).
arith((_ * _), times). arith((_ * _), times).
arith((_ / _), div). arith((_ / _), div).
arith(sum(_), sum). arith(sum(_), sum).
arith(sum(_,_), sum).
arith(count(_,_), count).
% replace abs(min(A,B)-max(A,B)) by % 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) % min(A,B,A1), max(A,B,A2), linear([1,-1],[A1,B1],=,A3), abs(A3,AN)
@ -641,6 +746,31 @@ equality(min( V1 , V2), NV, Env) :-
equality(V1, V1A, Env), equality(V1, V1A, Env),
equality(V2, V2A, Env), equality(V2, V2A, Env),
new_arith( (min), V1A, V2A, NV, 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_l(Env, V0, V) :-
equality(V0, V, Env). equality(V0, V, Env).
@ -745,6 +875,13 @@ new_arith( max, V, NV, Space-Map) :-
maplist(ll(Map), V, X), maplist(ll(Map), V, X),
Space += min(X, NX). 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) :- new_arith( minus, V1, V2, NV, Space-Map) :-
l(V1, X1, Min1, Max1, Map), l(V1, X1, Min1, Max1, Map),
l(V2, X2, Min2, Max2, Map), l(V2, X2, Min2, Max2, Map),
@ -808,6 +945,51 @@ new_arith( (mod), V1, V2, NV, Space-Map) :-
m(NV, NX, Min, Max, Map), m(NV, NX, Min, Max, Map),
Space += mod(X1, X2, NX). 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_times(Min1,Min2,Max1,Max2,Min) :-
Min is min(Min1*Min2, min(Min1*Max2, min(Max1*Min2, Max1*Max2))). Min is min(Min1*Min2, min(Min1*Max2, min(Max1*Min2, Max1*Max2))).
@ -835,6 +1017,12 @@ max_l(Map, V, Min0, Min, Max0, Max) :-
Min is max(Min0, Min1), Min is max(Min0, Min1),
Max is max(Max0, Max1). 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) :- in_c(A, A, _y) :-
var(A), !. var(A), !.
in_c(C, A, Space-Map) :- in_c(C, A, Space-Map) :-