Support for Python "infinity" value for MZNJSONEncoder

[raphaelboudreault]

Using Python infinity value in the MiniZinc data is encoded in JSON as "Infinity" instead of "infinity", which makes MiniZinc crash. I believe the best way would be to change MZNJSONEncoder to support that or forbid this conversion to happen.

[Dekker1]

Are you referring to the floating point infinity values in Python? I suppose they would be the way handle infinity in Python.

However, I'm not sure whether MiniZinc's JSON parser is setup to do handle any type of Infinity value. I don't really see any mention of infinity in the JSON spec: https://www.json.org/json-en.html

[raphaelboudreault]

According to Python's json lib, JSONEncoder encodes Python infinity values by default as "Infinity"/"-Infinity":
Ref

If allow_nan is true (the default), then NaN, Infinity, and -Infinity will be encoded as such. This behavior is not JSON specification compliant, but is consistent with most JavaScript based encoders and decoders. Otherwise, it will be a ValueError to encode such floats.

I believe this could be handled in MZNJSONEncoder so that it instead prints "infinity"/"-infinity" and doesn't crash.

[Dekker1]

I'm actually not sure whether this could be handled by the MZNJSONEncoder class. The problem that I've been unable to resolve in #2 is that number classes are handled directly by Python's JSON encoder, and will not call the hook.

Apart from that, you seem to be under the impression that "infinity" is already supported by MiniZinc's JSON parser, but this is not the case.

Using the json {"x": "infinity"} with the MiniZinc file int: x; will give an error:

Error: type error: cannot determine coercion from type string to type int
unknown file:0.0

So maybe the right way to change this is for MiniZinc's json parser to accept what Python will already output. I don't think I particularly mind this, but I am a little wary of the fact that this would mean that you wouldn't be able to tell whether something was an integer or an floating point value

[raphaelboudreault]

I'm actually not sure whether this could be handled by the MZNJSONEncoder class. The problem that I've been unable to resolve in #2 is that number classes are handled directly by Python's JSON encoder, and will not call the hook.

You are right, so it seems there is no way to override Python's JSONEncoder for specific numeric values.

Apart from that, you seem to be under the impression that "infinity" is already supported by MiniZinc's JSON parser, but this is not the case.

You are also right. MiniZinc's JSON parser is not able to handle (yet) the "infinity" string for numerical values, which was a wrong assumption on my side.

So maybe the right way to change this is for MiniZinc's json parser to accept what Python will already output. I don't think I particularly mind this, but I am a little wary of the fact that this would mean that you wouldn't be able to tell whether something was an integer or an floating point value

I think this is it. MiniZinc JSON parser should at least understand an "infinity" string, whether it is with a capital letter or not.

In the meantime, I suggest that you set allow_nan=False in the main function that encodes to JSON (line 519 of file encoder.py) This will make minizinc-python fail on a request of encoding a Python INFINITY numeric value. You could also catch the error from JSONEncoder to return a better error message for users that is specific to minizinc-python (like a "Not implemented" error).