diff --git a/gbac/on_restart.mzn b/gbac/on_restart.mzn index 841d2c8..1a98176 100644 --- a/gbac/on_restart.mzn +++ b/gbac/on_restart.mzn @@ -1,5 +1,5 @@ include "gbac.mzn"; -include "../lib.mzn"; +include "restart.mzn"; predicate int_eq_imp(var int: x, var int: y, var bool: b); predicate bool_eq_imp(var bool: x, var bool: y, var bool: b); @@ -18,12 +18,12 @@ predicate free_period(var bool: b) = let { array[1..2] of var bool: nbh; constraint random_allocation(nbh[1]); constraint free_period(nbh[2]); -var 0..10000000: restart = restart_number(); -var 1..2: select = (restart mod 2) + 1; -constraint bool_eq_imp(nbh[1], false, status() == UNKNOWN); -constraint bool_eq_imp(nbh[2], false, status() == UNKNOWN); -constraint bool_eq_imp(nbh[1], select == 1, status() != UNKNOWN); -constraint bool_eq_imp(nbh[2], select == 2, status() != UNKNOWN); +var 1..2: select; +constraint lastval(select) mod 2 + 1 = select; +constraint bool_eq_imp(nbh[1], false, status() == START); +constraint bool_eq_imp(nbh[2], false, status() == START); +constraint bool_eq_imp(nbh[1], select == 1, status() != START); +constraint bool_eq_imp(nbh[2], select == 2, status() != START); annotation main_vars(array[int] of var int: vars); diff --git a/lib.mzn b/lib.mzn deleted file mode 100644 index bc14cdf..0000000 --- a/lib.mzn +++ /dev/null @@ -1,100 +0,0 @@ -/*** - @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; diff --git a/rcpsp-wet/on_restart.mzn b/rcpsp-wet/on_restart.mzn index 38def3e..11f715d 100644 --- a/rcpsp-wet/on_restart.mzn +++ b/rcpsp-wet/on_restart.mzn @@ -1,5 +1,5 @@ include "rcpsp-wet.mzn"; -include "../lib.mzn"; +include "restart.mzn"; predicate int_eq_imp(var int: x, var int: y, var bool: b); predicate bool_eq_imp(var bool: x, var bool: y, var bool: b); @@ -21,12 +21,12 @@ predicate free_timeslot(var bool: b) = array[1..2] of var bool: nbh; constraint randomize(nbh[1]); constraint free_timeslot(nbh[2]); -var 0..10000000: restart = restart_number(); -var 1..2: select = (restart mod 2) + 1; -constraint bool_eq_imp(nbh[1], false, status() == UNKNOWN); -constraint bool_eq_imp(nbh[2], false, status() == UNKNOWN); -constraint bool_eq_imp(nbh[1], select == 1, status() != UNKNOWN); -constraint bool_eq_imp(nbh[2], select == 2, status() != UNKNOWN); +var 1..2: select; +constraint lastval(select) mod 2 + 1 = select; +constraint bool_eq_imp(nbh[1], false, status() == START); +constraint bool_eq_imp(nbh[2], false, status() == START); +constraint bool_eq_imp(nbh[1], select == 1, status() != START); +constraint bool_eq_imp(nbh[2], select == 2, status() != START); annotation main_vars(array[int] of var int: vars); diff --git a/steelmillslab/on_restart.mzn b/steelmillslab/on_restart.mzn index 2009a7d..bb30f17 100644 --- a/steelmillslab/on_restart.mzn +++ b/steelmillslab/on_restart.mzn @@ -1,5 +1,5 @@ include "steelmillslab.mzn"; -include "../lib.mzn"; +include "restart.mzn"; predicate int_eq_imp(var int: x, var int: y, var bool: b); predicate bool_eq_imp(var bool: x, var bool: y, var bool: b); @@ -18,12 +18,12 @@ predicate random_bin(var bool: b) = let { array[1..2] of var bool: nbh; constraint random_assignment(nbh[1]); constraint random_bin(nbh[2]); -var 0..10000000: restart = restart_number(); -var 1..2: select = (restart mod 2) + 1; -constraint bool_eq_imp(nbh[1], false, status() == UNKNOWN); -constraint bool_eq_imp(nbh[2], false, status() == UNKNOWN); -constraint bool_eq_imp(nbh[1], select == 1, status() != UNKNOWN); -constraint bool_eq_imp(nbh[2], select == 2, status() != UNKNOWN); +var 1..2: select; +constraint lastval(select) mod 2 + 1 = select; +constraint bool_eq_imp(nbh[1], false, status() == START); +constraint bool_eq_imp(nbh[2], false, status() == START); +constraint bool_eq_imp(nbh[1], select == 1, status() != START); +constraint bool_eq_imp(nbh[2], select == 2, status() != START); annotation main_vars(array[int] of var int: vars);