TypeError in checker models where data partially fixes variable arrays

[95A31]

Hello, I would like to know if it is possible to adjust the variables' domain from the data file. In detail I would like do something like this:

MODEL

var int: a;
array[1..3] of var bool: bs;

solve satisfy;

DATA

a = 1..5;
bs[2] = true; `

[Dekker1]

This is possible by naming the domain that you would like to set. In you model:

set of int: dom_a;
var dom_a: a;
solve satisfy;

In you data you can then add the line: dom_a = 1..5;

Assigning a single variable using array indexing is also not supported in data files, instead, you can assign one by using the following syntax:

bs = [_, true, _];

[95A31]

Thank you. Now I have a problem with the solution checker, do you know if there is a workaround?

MODEL

set of int: dom_a;
var dom_a: a;

array[1..3] of var bool: bs;

solve satisfy;

DATA

dom_a = 1..5;
bs = [_, true, _];

CHECKER

set of int: dom_a;
int: a;
array[1..3] of bool: bs;

output
[
  if a > 0 /\ bs[2] == true
  then 
    "Ok\n"
  else 
    "Fail\n"
  endif
];

[Dekker1]

It seems that the model checkers are currently unable to handle the partial assignments of variables in data files. The statement bs = [_, true, _]; will be combined to the checker model, but the types do not yet match:

MiniZinc: type error: initialisation value for `bs' has invalid type-inst: expected `array[int] of bool', actual `array[int] of var bool'

A full assignment (bs = [true,true,true];) does not have the same problem.

[95A31]

In my case is possible this workaround:

DATA (Test-D.mzn)

var 0..5: a;

array[int] of var bool: bs = [_,true,_];

MODEL (Test-M.mzn)

constraint a > 0;

solve satisfy;

CHECKER (Tests-C.mzc.mzn)

int: a;
array[int] of bool: bs;

output
[
  if a > 0 /\ bs[2] == true
  then 
    "Ok\n"
  else 
    "Fail\n"
  endif
];

The command I used is:

minizinc Test-D.mzn Test-M.mzn Test-C.mzc.mzn

[guidotack]

The problem is that, strictly speaking, assignments to variables shouldn't really be part of data files at all. The MiniZinc type checker has always been quite lenient about what it accepts in a .dzn file, mainly to remain compatible to older versions. Ideally, you would e.g. use an array of optional values to specify input (with <> to denote unspecified parts), which is compatible with checker models. In your example, the following would work:

test.dzn:

dom_a = 0..5;
bs_input = [<>, true, <>];

test.mzn:

set of int: dom_a;
var dom_a: a ;
array[int] of opt bool: bs_input;
array[int] of var bool: bs = [ if absent(bs_input[i]) then _ else deopt(bs_input[i]) endif | i in index_set(bs_input) ];

test.mzc.mzn:

set of int: dom_a;
array[int] of opt bool: bs_input;
int: a;
array[int] of bool: bs;

output
[
  if a > 0 /\ bs[2] == true
  then 
    "Ok\n"
  else 
    "Fail\n"
  endif
];