Compiler should accept sets (especially ranges) as valid output values

[ridgeworks]

I'm interested in experimenting with a solver over a continuous domain (extended set of reals). Values in such a domain can be modelled by a range of floats to represent the set of all reals between the two float values. On the input side this works fine, but it's also necessary to output a float range value (the range can't be enumerated as for finite sets).

The Reference manual https://www.minizinc.org/doc-2.7.6/en/fzn-spec.html suggests this should be allowed:

Output must take the following form: <var-par-identifier> = <basic-literal-expr>;

and from the FlatZinc grammar:

<basic-literal-expr> ::= <bool-literal>
                       | <int-literal>
                       | <float-literal>
                       | <set-literal>

% Set literals
<set-literal> ::= "{" [ <int-literal> "," ... ] "}"
                | <int-literal> ".." <int-literal>
                | "{" [ <float-literal> "," ... ] "}"
                | <float-literal> ".." <float-literal>

but when I try this in the IDE with the following program:

var 1.1..1.3:X;

and my experimental solver, I get the following message:

[solution received from solver:1.5-42:](err:solution received from solver?line=1&column=5)
MiniZinc: type error: assignment value for `X' has invalid type-inst: expected `float', actual `set of float'
Process finished with non-zero exit code 1

If I temporarily work around this by outputting the midpoint of the ranges as a float, I get the expected result, so I'm fairly confident the rest of the machinery is functioning as intended.

I think this capability would also be useful for under constrained problems in finite domains so ranges could be compactly represented rather than enumerated. (Try the above one-liner with Gecode.)

I think this is a bug (fails to meet documented specification) but if it's a feature, a workaround would be appreciated.

[Dekker1]

Although you are right that the solver output can contain something like X = 1.1..3.3 according to the syntax spec, this does not guarantee that using a range as a solution assignment to X is valid. The solver has to make sure that the type is correct. For example, X = true would also not be accepted.

The underlying issue in this case seems come from the fact that we ask solvers to output a stream of solution. In MiniZinc a solution is defined as the assignment of parameter values for each (output) decision variable in the instance, such that all constraint are (or can be) satisfied. Working from such a definition, X must be defined to a single float value. However, your idea is that it should be possible for solvers to also output sets/collections of solutions as a single item within that stream, and that the set syntax can be used to represent these.

Again, note that the syntax is already supported, but it is used for solvers that support var set of int as input.

[ridgeworks]

In MiniZinc a solution is defined as the assignment of parameter values for each (output) decision variable in the instance, such that all constraint are (or can be) satisfied.

Not sure why assigning a set of values to a decision variable doesn't meet this criteria, i.e., the constraints are satisfied for all members of the set. This would actually allow a compact representation of a set of solutions, rather than having to enumerate all the individual solutions. (Various CLP dialects, e.g., CLP(FD), support this functionality.)

Working from such a definition, X must be defined to a single float value.

That seems to me to be rather restrictive. To expand on that, MiniZinc dictates that a solution cannot be a set; it must be either an int or a float. Therefore I cannot model sets of reals as a float range. (Well it works for input but not output.)

Float ranges (also known as intervals) are used to represent sets of reals and mathematically correct functions over intervals can be implemented (unlike floating point arithmetic with inherent rounding errors). (Google "interval arithmetic libraries").

Again, note that the syntax is already supported, but it is used for solvers that support var set of int as input.

And I have a solver that would like to support float (and int) ranges as input and output. The syntax is supported but the restriction on output is a showstopper.

[guidotack]

The output is required to be type correct with respect to the variable definitions. If your MiniZinc model has a variable var float: x; then an assignment item like x = 1.0 .. 3.0; will be rejected by the compiler because you are assigning a set to a variable that does not have set type. It is irrelevant that this is a syntactically correct assignment item, it’s simply a type error. Output from solvers has to be a sequence of type correct assignment items. If that’s not clear enough in the spec we may have to add an explanation there.

To support what you are suggesting would require significant changes in the output processing. It’s possible but not high on our todo list given the limited development resources. You’re welcome to make those changes and to contribute them back.

[ridgeworks]

The output is required to be type correct with respect to the variable definitions. If your MiniZinc model has a variable var float: x; then an assignment item like x = 1.0 .. 3.0; will be rejected by the compiler because you are assigning a set to a variable that does not have set type.

Would it be accepted if the variable was a set type, e.g.,

var 1.0..10.0:x;

followed by

x = 1.0..3.0

i.e., the assignment value is a subset of the original? I suspect not.

I guess the bottom line is that sets are not values, they're really just types. The only values are bools, ints and floats, and arrays. But if that's the case <set-literal> ought to be excluded from the output syntax.

As my skillset doesn't include cpp and I also have limited resources, I won't pursue this further.

[Dekker1]

It should be allowed if the variable was actually a set type:

var set of 1.0..10.0: x;

In this case assigning x = 1.0..3.0 would be type correct. However, since we current don't have any solvers that support these types of variables, our infrastructure lacks an internal representation of decision variables of set of float types, and a type error would still be raised.

Note that using sets as decision variables is rather different from what I thought the point of this issue was. As I understand it, the idea was to be able to provide collections/sets/ranges of solutions from the solver. We had an interesting conversation about this internally, and we believe it could be supported. To make it type correct you would provide your result as, for example, x in 1.0..3.0 (given var float: x). We then would need to think about the additional processing needed in our output processing to make it work, and what other parts of the ecosystem it affects. As I understand it, however, it seems quite interesting for the support of interval solvers.

[ridgeworks]

I'm a novice when it comes to MiniZinc, in particular what happens to solver output, but I have a "solver" for the domain of reals based on relational interval arithmetic (https://github.com/ridgeworks/clpBNR). When I came across MiniZinc I was curious as to whether the MiniZinc could be used as as a front end to this IA solver rather than Prolog (the current implementation is an SWI-Prolog module and the solver would still run in a SWIP environment).

To accomplish this, one main issue is how to map MiniZinc types and values to/from intervals. Fortunately, MiniZInc has float (and int) ranges so these can pretty much represent intervals for all practical purposes. Certainly no problem on input, and since intervals can only narrow during a solve operation, conceptually there should be no problem on output other than the one that triggered this issue.

On input (from the FlatZinc source), the following are currently mapped to intervals:

• unfixed ints and bools to integer intervals
• unfixed floats to real intervals
• int ranges to integer intervals
• float ranges to real intervals
• float literals to real intervals (because a literals like '0.1' are interpreted as a real value, not a floating point value closest to 0.1)

On output, intervals which haven't been narrowed to a point by the solve operation:

• integer intervals output as int ranges
• real intervals output as float ranges

I should note that real intervals rarely narrow to a point value due to the "fuzzy" nature of floating point arithmetic. OTOH, integer intervals are usually narrowed to a single value due to the enumeration process of any solve operation. Also note that the general 'set of float' ( { ....} ) isn't needed, just ranges.

Perhaps there's a better way, but this is the current state of play. Any help/advice appreciated.