101 lines
2.7 KiB
MiniZinc
101 lines
2.7 KiB
MiniZinc
/***
|
|
@groupdef internal Internal Builtins
|
|
|
|
These annotations and functions provide the basic building blocks to implement
|
|
meta-heuristics and governed search with the use of solver internal values and
|
|
functionality.
|
|
*/
|
|
|
|
/*
|
|
A search annotation that supplies a function to be executed on restart
|
|
*/
|
|
ann: on_restart(string: pred);
|
|
|
|
/*
|
|
The 'status' function reports the status of the solver (before restarting).
|
|
*/
|
|
enum STATUS = {UNKNOWN, UNSAT, SAT, OPT};
|
|
function var STATUS: status();
|
|
|
|
function var int: restart_number();
|
|
|
|
/*
|
|
The 'rnd' function provides random values chosen by the solver. The arguments
|
|
to the function limit the values to a certain domain.
|
|
*/
|
|
function var int: uniform_internal(int: i, int: j) ::impure = int_uniform(i, j);
|
|
|
|
function var int: uniform_internal(set of int: S) ::impure =
|
|
if card(S) == max(S) - min(S) + 1 then
|
|
int_uniform(min(S),max(S))
|
|
else
|
|
[ i | i in S ][int_uniform(1,card(S))]
|
|
endif;
|
|
|
|
/*
|
|
'int_rnd' is the random intrinsic that needs to be implemented by the solver.
|
|
*/
|
|
function var int: int_uniform(int: a, int: b) ::impure;
|
|
|
|
/*
|
|
The 'sol' functions provides access to solution values of model variables. The
|
|
sol functions are only safe to use when the solver status is not UNKNOWN.
|
|
*/
|
|
function var bool: sol(var bool: x) =
|
|
if is_fixed(x) then
|
|
fix(x)
|
|
else
|
|
bool_sol(x)
|
|
endif;
|
|
|
|
function var float: sol(var float: x) =
|
|
if is_fixed(x) then
|
|
fix(x)
|
|
else
|
|
float_sol(x)
|
|
endif;
|
|
|
|
function var int: sol(var int: x) =
|
|
if is_fixed(x) then
|
|
fix(x)
|
|
else
|
|
int_sol(x)
|
|
endif;
|
|
|
|
function array[int] of var bool: sol(array[int] of var bool: x) =
|
|
[if is_fixed(x[i]) then fix(x[i]) else bool_sol(x[i]) endif | i in index_set(x)];
|
|
|
|
function array[int] of var float: sol(array[int] of var float: x) =
|
|
[if is_fixed(x[i]) then fix(x[i]) else float_sol(x[i]) endif | i in index_set(x)];
|
|
|
|
function array[int] of var int: sol(array[int] of var int: x) =
|
|
[if is_fixed(x[i]) then fix(x[i]) else int_sol(x[i]) endif | i in index_set(x)];
|
|
|
|
/*
|
|
'bool_rnd', 'float_sol', and 'int_sol' are the solution intrinsics that needs
|
|
to be implemented by the solver.
|
|
*/
|
|
function var bool: bool_sol(var bool: a);
|
|
function var float: float_sol(var float: a);
|
|
function var int: int_sol(var int: a);
|
|
|
|
/*
|
|
'round_robin' provides a metaheuristic for LNS where each neighbourhood is
|
|
chosen sequentially.
|
|
*/
|
|
predicate round_robin(array[int] of var bool: nbhs) =
|
|
let {
|
|
set of int: N = index_set(nbhs);
|
|
% Neighbourhood control variables
|
|
array[N] of var bool: control;
|
|
% Neighbourhood selection
|
|
var N: select;
|
|
} in forall(i in N) (control[i] -> nbhs[i]) /\
|
|
if status() == UNKNOWN then
|
|
control = [false | i in N]
|
|
/\ select = max(N)
|
|
else
|
|
select = (sol(select) + 1) mod card(N)
|
|
/\ control = [i == select | i in N]
|
|
endif;
|