1%---------------------------------------------------------------------- 2% BEGIN LICENSE BLOCK 3% Version: CMPL 1.1 4% 5% The contents of this file are subject to the Cisco-style Mozilla Public 6% License Version 1.1 (the "License"); you may not use this file except 7% in compliance with the License. You may obtain a copy of the License 8% at www.eclipse-clp.org/license. 9% 10% Software distributed under the License is distributed on an "AS IS" 11% basis, WITHOUT WARRANTY OF ANY KIND, either express or implied. See 12% the License for the specific language governing rights and limitations 13% under the License. 14% 15% The Original Code is The Zinc Modelling Interface for ECLiPSe 16% The Initial Developer of the Original Code is Joachim Schimpf 17% Portions created by the Initial Developer are 18% Copyright (C) 2007 Cisco Systems, Inc. All Rights Reserved. 19% 20% Contributor(s): Joachim Schimpf 21% 22% END LICENSE BLOCK 23%---------------------------------------------------------------------- 24 25:- module(fzn_fd). 26 27:- comment(categories, ["Interfacing","Constraints"]). 28:- comment(summary, "Mapping from FlatZinc to lib(fd) and lib(fd_sets)"). 29:- comment(author, "Joachim Schimpf, supported by Cisco Systems and NICTA Victoria"). 30:- comment(copyright, "Cisco Systems Inc, licensed under CMPL"). 31:- comment(date, "$Date: 2015/01/14 01:31:09 $"). 32:- comment(see_also, [library(flatzinc), 33 library(fd),library(fd_sets),library(fd_global), 34 library(propia),library(branch_and_bound)]). 35:- comment(desc, html(" 36This module defines a mapping from FlatZinc operations to lib(fd), 37lib(fd_sets) and lib(fd_global), and is intended to be used in 38conjunction with lib(flatzinc). It uses lib(propia) to implement 39variants of the element constraint that are not supported by lib(fd). 40Moreover, lib(branch_and_bound) is used to provide optimization. 41</P><P> 42This mapping supports bool, integer and set variables. 43It does currently not support all constraints in reified form, 44in particular set constraints, according to the limitations of 45the underlying solvers. 46</P><P> 47The following extra annotations are supported by this mapping: 48<DL> 49<DT>annotation strategy(string:s)</DT> 50 <DD>the branch-and-bound strategy (default: \"continue\"). Valid names 51 are \"continue\", \"restart\", \"dichotomic\", See bb_min/3.</DD> 52<DT>annotation delta(float:f)</DT> 53 <DD>minimal absolute improvement for branch-and-bound steps (default 1.0). 54 See bb_min/3.</DD> 55<DT>annotation factor(float:f)</DT> 56 <DD>minimal improvement ratio (with respect to the lower cost bound) 57 for strategies 'continue' and 'restart' (default 1.0), or split factor 58 for strategy 'dichotomic' (default 0.5). See bb_min/3.</DD> 59<DT>annotation timeout(float:f)</DT> 60 <DD>timeout for branch-and-bound in seconds (default: unlimited). 61 See bb_min/3.</DD> 62</DL> 63You must include \"eclipse.mzn\" in your MiniZinc model to use these 64annotations. 65<P> 66")). 67 68 69% Lazy person's way of exporting (almost) all locally defined predicates: 70:- local initialization( 71 ( 72 current_module_predicate(local, Pred), 73 get_flag(Pred, auxiliary, off), 74 nonmember(Pred, [ 75 arg_nd/3, 76 array_any_element/3, 77 vector_sum/3, 78 search_ann/1, 79 set_choice/3, 80 termify/2 81 ]), 82 export(Pred), 83 fail 84 ; 85 true 86 )). 87 88:- lib(fd). % the actual solver libraries 89:- lib(fd_search). 90:- lib(fd_sets). 91:- lib(propia). 92:- lib(branch_and_bound). 93 94:- import % resolve ambiguous imports 95 (::)/2, 96 intersection/3, 97 subset/2, 98 union/3 99 from fd_sets. 100 101:- import 102 fzn_write/2, 103 fzn_error/2 104 from flatzinc. 105 106 107% Declarations ----------------------------------------------- 108 109% Single variable declarations 110bool_declare(X) :- X #:: 0..1. 111int_declare(X) :- integers([X]). 112int_declare(X, Min, Max) :- X #:: Min..Max. 113int_declare(X, Elems) :- X #:: Elems. 114set_declare(X, Min, Max) :- intset(X, Min, Max). 115set_declare(X, Elems) :- X :: Elems. 116 117% Variable array declarations 118% Unfortunately not all primitives can handle arrays 119bool_declare_array(Xs) :- 120 ( foreacharg(X,Xs) do X #:: 0..1 ). 121int_declare_array(Xs) :- 122 ( foreacharg(X,Xs) do integers([X]) ). 123int_declare_array(Xs, Min, Max) :- 124 ( foreacharg(X,Xs), param(Min,Max) do X #:: Min..Max ). 125int_declare_array(Xs, Elems) :- 126 ( foreacharg(X,Xs), param(Elems) do X #:: Elems ). 127set_declare_array(Xs, Min, Max) :- 128 ( foreacharg(X,Xs), param(Min,Max) do intset(X, Min, Max) ). 129set_declare_array(Xs, Elems) :- 130 ( foreacharg(X,Xs), param(Elems) do X :: Elems ). 131 132 133% Comparisons ----------------------------------------------- 134 135% int_??(var int, var int) 136int_eq(X, Y) :- X = Y. 137int_ne(X, Y) :- X #\= Y. 138int_le(X, Y) :- X #=< Y. 139int_ge(X, Y) :- X #>= Y. 140int_lt(X, Y) :- X #< Y. 141int_gt(X, Y) :- X #> Y. 142 143% float_??(var float, var float) 144 145% bool_??(var bool, var bool) 146bool_eq(X, Y) :- X = Y. 147bool_ne(X, Y) :- X #\= Y. 148bool_le(X, Y) :- X #=< Y. 149bool_ge(X, Y) :- X #>= Y. 150bool_lt(X, Y) :- X #< Y. 151bool_gt(X, Y) :- X #> Y. 152 153% set_??(var set, var set) 154set_eq(X, Y) :- X = Y. 155%bool_ne(X, Y) :- 156%bool_le(X, Y) :- 157%bool_ge(X, Y) :- 158%bool_lt(X, Y) :- 159%bool_gt(X, Y) :- 160 161% int_lin_??(array[int] of int, array[int] of var int, int) 162int_lin_eq(Cs, Xs, Rhs) :- vector_sum(Cs, Xs, CXs), sum(CXs) #= Rhs. 163int_lin_ne(Cs, Xs, Rhs) :- vector_sum(Cs, Xs, CXs), sum(CXs) #\= Rhs. 164int_lin_le(Cs, Xs, Rhs) :- vector_sum(Cs, Xs, CXs), sum(CXs) #=< Rhs. 165int_lin_ge(Cs, Xs, Rhs) :- vector_sum(Cs, Xs, CXs), sum(CXs) #>= Rhs. 166int_lin_lt(Cs, Xs, Rhs) :- vector_sum(Cs, Xs, CXs), sum(CXs) #< Rhs. 167int_lin_gt(Cs, Xs, Rhs) :- vector_sum(Cs, Xs, CXs), sum(CXs) #> Rhs. 168 169% float_lin_??(array[int] of float, array[int] of var float, float) 170 171% int_??(var int, var int, var bool) 172int_eq_reif(X, Y, B) :- #=(X, Y, B). 173int_ne_reif(X, Y, B) :- #\=(X, Y, B). 174int_le_reif(X, Y, B) :- #=<(X, Y, B). 175int_ge_reif(X, Y, B) :- #>=(X, Y, B). 176int_lt_reif(X, Y, B) :- #<(X, Y, B). 177int_gt_reif(X, Y, B) :- #>(X, Y, B). 178 179% float_??(var float, var float, B) 180 181% bool_??(var bool, var bool) 182bool_eq_reif(X, Y, B) :- #=(X, Y, B). 183bool_ne_reif(X, Y, B) :- #\=(X, Y, B). 184bool_le_reif(X, Y, B) :- #=<(X, Y, B). 185bool_ge_reif(X, Y, B) :- #>=(X, Y, B). 186bool_lt_reif(X, Y, B) :- #<(X, Y, B). 187bool_gt_reif(X, Y, B) :- #>(X, Y, B). 188 189% set_??(var set, var set, B) 190%set_eq_reif(X, Y, B) :- 191%bool_ne_reif(X, Y, B) :- 192%bool_le_reif(X, Y, B) :- 193%bool_ge_reif(X, Y, B) :- 194%bool_lt_reif(X, Y, B) :- 195%bool_gt_reif(X, Y, B) :- 196 197% int_lin_??(array[int] of int, array[int] of var int, int, var bool) 198int_lin_eq_reif(Cs, Xs, Rhs, B) :- vector_sum(Cs, Xs, CXs), #=(sum(CXs), Rhs, B). 199int_lin_ne_reif(Cs, Xs, Rhs, B) :- vector_sum(Cs, Xs, CXs), #\=(sum(CXs), Rhs, B). 200int_lin_le_reif(Cs, Xs, Rhs, B) :- vector_sum(Cs, Xs, CXs), #=<(sum(CXs), Rhs, B). 201int_lin_ge_reif(Cs, Xs, Rhs, B) :- vector_sum(Cs, Xs, CXs), #>=(sum(CXs), Rhs, B). 202int_lin_lt_reif(Cs, Xs, Rhs, B) :- vector_sum(Cs, Xs, CXs), #<(sum(CXs), Rhs, B). 203int_lin_gt_reif(Cs, Xs, Rhs, B) :- vector_sum(Cs, Xs, CXs), #>(sum(CXs), Rhs, B). 204 205% float_lin_??(array[int] of float, array[int] of var float, float, B) 206 207 vector_sum(Cs, Xs, CXs) :- 208 arity(Cs, N), 209 ( arity(Xs, N) -> 210 ( for(I,1,N), foreach(C*X,CXs), param(Cs,Xs) do 211 arg(I, Cs, C), arg(I, Xs, X) 212 ) 213 ; 214 fzn_error("Mismatched vector product %w %w", [Cs, Xs]) 215 ). 216 217 218% Arithmetic operations ----------------------------------------------- 219 220% int_???(var int, var int, var int) 221int_negate(X, Z) :- Z #= -X. 222int_plus(X, Y, Z) :- Z #= X+Y. 223int_minus(X, Y, Z) :- Z #= X-Y. 224int_times(X, Y, Z) :- Z #= X*Y. 225int_div(Dividend, Divisor, Quotient) :- 226 Remainder #>=0, Remainder #< abs(Divisor), 227 Dividend #= Quotient*Divisor + Remainder. 228int_mod(Dividend, Divisor, Remainder) :- 229 Remainder #>=0, Remainder #< abs(Divisor), 230 Dividend #= _Quotient*Divisor + Remainder. 231int_min(X, Y, Z) :- Z #= min(X,Y). 232int_max(X, Y, Z) :- Z #= max(X,Y). 233int_abs(X, Z) :- Z #= abs(X). 234 235% float_???(var float, var float, var float) 236 237 238% Logical operations ----------------------------------------------- 239 240% bool_???(var bool, var bool, var bool) 241bool_and(X, Y, Z) :- #/\(X, Y, Z). 242bool_or(X, Y, Z) :- #\/(X, Y, Z). 243bool_left_imp(X, Y, Z) :- #=>(Y, X, Z). 244bool_right_imp(X, Y, Z) :- #=>(X, Y, Z). 245bool_xor(X, Y, Z) :- #\=(X, Y, Z). 246bool_not(X, Z) :- #\+(X, Z). 247 248% array_bool_???(array[int] of var bool, var bool) 249array_bool_and(Xs, B) :- fd_global:minlist(Xs, B). 250array_bool_or(Xs, B) :- fd_global:maxlist(Xs, B). 251 252% bool_clause(array[int] of var bool, array[int] of var bool) 253bool_clause(Ps, Ns) :- 254 bool_clause_reif(Ps, Ns, 1). 255bool_clause_reif(Ps, Ns, B) :- 256 ic_global:maxlist(Ps, B1), 257 ic_global:minlist(Ns, B2), 258 #>=(B1,B2,B). 259 260 261% Set operations ----------------------------------------------- 262 263% set_???(... var set of int ...) 264set_in(I, S) :- I in S. 265set_subset(Sub, Super) :- subset(Sub, Super). 266set_intersect(X, Y, Z) :- intersection(X, Y, Z). 267set_union(X, Y, Z) :- union(X, Y, Z). 268set_diff(X, Y, Z) :- difference(X, Y, Z). 269set_symdiff(X, Y, Z) :- symdiff(X, Y, Z). 270set_card(S, I) :- #(S, I). 271 272set_in_reif(I, S, B) :- in(I, S, B). 273 274 275% Array operations ----------------------------------------------- 276 277% array_xx_yy_element(var int, array[int] of xx yy, var yy) 278array_bool_element(I, Array, E) :- Array =.. [_|List], element(I, List, E). 279array_int_element(I, Array, E) :- Array =.. [_|List], element(I, List, E). 280%array_set_element(I, Array, E) :- array_any_element(I, Array, E). 281array_var_bool_element(I, Array, E) :- array_any_element(I, Array, E). 282array_var_int_element(I, Array, E) :- array_any_element(I, Array, E). 283%array_var_set_element(I, Array, E) :- array_any_element(I, Array, E). 284 285 array_any_element(I, Array, E) :- 286 arity(Array, N), 287 I #:: 1..N, 288 arg_nd(I, Array, E) infers fd. 289 290 arg_nd(I, Array, E) :- 291 indomain(I), 292 arg(I, Array, E). 293 294 295% Coercion operations ----------------------------------------------- 296 297% This is only useful for float-typed annotations, 298% as lib(fd) cannot handle floats elsewhere. 299int2float(I, F) :- ( var(I) -> F=I ; F is float(I) ). 300 301bool2int(X, X). 302 303 304% FZN data <-> ECLiPSe data ----------------------------------------------- 305 306bool_fzn_to_solver(false, 0). 307bool_fzn_to_solver(true, 1). 308 309bool_solver_to_fzn(0, false). 310bool_solver_to_fzn(1, true). 311 312% This is only useful for float-typed annotations, 313% as lib(fd) cannot handle floats elsewhere. 314float_fzn_to_solver(X, F) :- F is float(X). 315 316% should never be needed 317float_solver_to_fzn(X, X) :- real(X). 318 319 320% Set constants are ordered lists in fd_sets 321set_fzn_to_solver(List, Set) :- eclipse_language:sort(List, Set). 322 323set_solver_to_fzn(List, List) :- is_list(List). 324 325% Set constants are ordered lists in fd_sets 326range_fzn_to_solver(Min, Max, Set) :- 327 ( for(I,Min,Max), foreach(I,Set) do true ). 328 329 330% Search ----------------------------------------------- 331 332satisfy(Anns) :- 333 ( foreach(Ann,Anns) do 334 termify(Ann, Ann1), % for Flatzinc<1.0 compatibility 335 search_ann(Ann1) 336 ). 337 338:- export minimize/3. % silence warning 339minimize(Expr, Anns, Cost) :- 340 extract_bb_anns(Anns, Anns1, BbOptions), 341 Cost #= Expr, 342 bb_min(satisfy(Anns1), Cost, BbOptions). 343 344maximize(Expr, Anns, ObjVal) :- 345 extract_bb_anns(Anns, Anns1, BbOptions), 346 Cost #= -Expr, 347 bb_min(satisfy(Anns1), Cost, BbOptions), 348 ObjVal is -Cost. 349 350 termify(In, Out) :- 351 functor(In, F, N), functor(Out, F, N), 352 ( for(I,1,N),param(In,Out) do 353 arg(I,In,InI), arg(I,Out,OutI), 354 ( string(InI) -> term_string(OutI,InI) ; OutI=InI ) 355 ). 356 357 358 search_ann(seq_search(Searches)) :- !, 359 ( foreacharg(Search,Searches) do search_ann(Search) ). 360 search_ann(bool_search(Vars, Select, Choice, Explore)) :- !, 361 search(Vars, 0, Select, Choice, Explore, []). 362 search_ann(int_search(Vars, Select, Choice, Explore)) :- !, 363 search(Vars, 0, Select, Choice, Explore, []). 364 search_ann(float_search([], _Prec, _, _, _)) :- !. 365 search_ann(set_search(Sets, input_order, Choice, complete)) :- 366 set_choice(Choice, ElemSel, Order), !, 367 ( functor(Sets, [], _) -> 368 ( foreacharg(Set,Sets), param(ElemSel,Order) do 369 insetdomain(Set, any, ElemSel, Order) 370 ) 371 ; 372 ( foreach(Set,Sets), param(ElemSel,Order) do 373 insetdomain(Set, any, ElemSel, Order) 374 ) 375 ). 376 search_ann(Ann) :- 377 fzn_error("Unsupported search annotation: %w", [Ann]). 378 379 380 :- mode set_choice(+,-,-). 381 set_choice(indomain_min, small_first, in_notin). 382 set_choice(indomain_max, big_first, in_notin). 383 set_choice(outdomain_min, small_first, notin_in). 384 set_choice(outdomain_max, big_first, notin_in). 385 386 387 extract_bb_anns(Anns, RestAnns, BbOptions) :- 388 ( 389 foreach(Ann,Anns), 390 fromto(RestAnns,Anns2,Anns1,[]), 391 param(BbOptions) 392 do 393 ( bb_ann(Ann, BbOptions) -> Anns2 = Anns1 ; Anns2 = [Ann|Anns1] ) 394 ). 395 396 % Corresponding annotation-declarations are in eclipse.mzn 397 bb_ann(delta(R), bb_options{delta:F}) :- float(R, F). 398 bb_ann(factor(R), bb_options{factor:F}) :- float(R, F). 399 bb_ann(timeout(R), bb_options{timeout:F}) :- float(R, F). 400 bb_ann(strategy(S), bb_options{strategy:A}) :- atom_string(A, S). 401 402 403% Global Constraints (see fzn_fd/globals.mzn) ------------------- 404 405all_different_int(Xs) :- fd_global:alldifferent(Xs). 406 407at_most_int(N,Xs,V) :- fd_global:atmost(N, Xs, V). 408%at_most(N,Xs,V) :- Count #=< N, fd_global:occurrences(V, Xs, Count). 409 410at_least_int(N,Xs,V) :- Count #>= N, fd_global:occurrences(V, Xs, Count). 411 412exactly_int(N,Xs,V) :- fd_global:occurrences(V, Xs, N). 413 414count_avint_int_int(Xs,V,N) :- fd_global:occurrences(V, Xs, N). 415 416%cumulative_avint_aint_aint_vint(Ss,Ds,Rs,B) :- cumulative:cumulative(Ss,Ds,Rs,B). 417cumulative_avint_aint_aint_vint(Ss,Ds,Rs,B) :- edge_finder:cumulative(Ss,Ds,Rs,B). 418%cumulative_avint_aint_aint_vint(Ss,Ds,Rs,B) :- edge_finder3:cumulative(Ss,Ds,Rs,B). 419 420:- export sort/2. % to resolve ambiguity with sort/2 builtin 421sort(Xs,Ss) :- fd_global:sorted(Xs, _Ps, Ss). 422 423 424:- reexport disjoint/2 from fd_sets. 425 426:- export all_disjoint/1. 427all_disjoint(Array) :- Array =.. [[]|List], fd_sets:all_disjoint(List). 428 429link_set_to_booleans(Set, Bools) :- fd_sets:membership_booleans(Set, Bools). 430 431