minesweeper_basic4.fzn 2.18 KB
Newer Older
Valentin Platzgummer's avatar
Valentin Platzgummer committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31
array [1..8] of int: game = [-1, -1, -1, -1, 1, 1, 1, 1];
var bool: BOOL____00001 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00002 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00003 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00004 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00005 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00006 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00007 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00008 :: is_defined_var :: var_is_introduced;
array [1..8] of var 0..1: mines :: output_array([1..2, 1..4]);
constraint int_eq_reif(mines[1], 0, BOOL____00001) :: defines_var(BOOL____00001);
constraint int_eq_reif(mines[1], 1, BOOL____00002) :: defines_var(BOOL____00002);
constraint int_eq_reif(mines[2], 0, BOOL____00003) :: defines_var(BOOL____00003);
constraint int_eq_reif(mines[2], 1, BOOL____00004) :: defines_var(BOOL____00004);
constraint int_eq_reif(mines[3], 0, BOOL____00005) :: defines_var(BOOL____00005);
constraint int_eq_reif(mines[3], 1, BOOL____00006) :: defines_var(BOOL____00006);
constraint int_eq_reif(mines[4], 0, BOOL____00007) :: defines_var(BOOL____00007);
constraint int_eq_reif(mines[4], 1, BOOL____00008) :: defines_var(BOOL____00008);
constraint int_eq_reif(mines[5], 0, true);
constraint int_eq_reif(mines[5], 1, false);
constraint int_eq_reif(mines[6], 0, true);
constraint int_eq_reif(mines[6], 1, false);
constraint int_eq_reif(mines[7], 0, true);
constraint int_eq_reif(mines[7], 1, false);
constraint int_eq_reif(mines[8], 0, true);
constraint int_eq_reif(mines[8], 1, false);
constraint int_lin_eq_reif([-1, -1, -1, -1], [mines[1], mines[2], mines[5], mines[6]], -1, true);
constraint int_lin_eq_reif([-1, -1, -1, -1], [mines[3], mines[4], mines[7], mines[8]], -1, true);
constraint int_lin_eq_reif([-1, -1, -1, -1, -1, -1], [mines[1], mines[2], mines[3], mines[5], mines[6], mines[7]], -1, true);
constraint int_lin_eq_reif([-1, -1, -1, -1, -1, -1], [mines[2], mines[3], mines[4], mines[6], mines[7], mines[8]], -1, true);
solve  :: int_search([mines[1], mines[2], mines[3], mines[4], mines[5], mines[6], mines[7], mines[8]], first_fail, indomain, complete) satisfy;