Configuration files for MiniZinc IDE integration

[PatrickTrentin88]

The project might benefit from including the necessary configuration files (for Linux, Windows and MacOS) to setup the fzn2omt solvers as MiniZinc backends.

e.g. [not tested]

On Linux, one would need to create the a configuration file similar to this and place it in .minizinc/solvers:

{
  "id": "optimathsat_int",
  "name": "OptiMathSAT (NIRA)",
  "description": "OptiMathSAT + OMT(NIRA)",
  "version": "1.7.0",
  "mznlib": "",
  "executable": "/opt/fzn2omt/bin/fzn2optimathsat.sh",
  "tags": ["cp","int"],
  "stdFlags": ["-a","-n","-p","-r","-f"],
  "supportsMzn": false,
  "supportsFzn": true,
  "needsSolns2Out": true,
  "needsMznExecutable": false,
  "needsStdlibDir": false,
  "isGUIApplication": false
 }

where fzn2optimathsat.sh is a new bash script that runs fzn2optimathsat.py with the correct options for the given configuration:

#!/bin/bash
python3 /.../fzn2omt/bin/fzn2optimathsat.py --finite-precision 20 --int-enc

Then it should be possible to run

minizinc --solver optimathsat_int model.mzn data.dzn

IMPORTANT NOTE: it appears to be necessary to create a new script fzn2optimathsat.sh to act as an intermediary for fzn2optimathsat.py because the MiniZinc solver does not appear to like solver options to be appended to the executable entry. (It doesn't have to be a bash script, it can be any executable without arguments).

[GustavBjordal]

The configuration works fine for me on Linux, it would be nice if it was part of the source.

I have a few questions though: 1) shouldn't the tags be "tags": ["smt","int"] ? 2) what do the --finite-precision 20 --int-enc flags do and are there any other flags I might want to use? You should also be able to move those flags into the configuration (so that MiniZinc provides them to the solver), but I don't recall the exact syntax for that. 3) Are there really no mznlib files?

Great work overall by the way, I look forward to using this solver!

[PatrickTrentin88]

@GustavBjordal

The configuration works fine for me on Linux, it would be nice if it was part of the source.

I have a few questions though:

1. shouldn't the tags be "tags": ["smt","int"] ?

Possibly, I'm not sure how these tags are used. I'd include these files as part of the project once we get working configurations for all platforms from some generous contributor.

2. what do the --finite-precision 20 --int-enc flags do and are there any other flags I might want to use?

You may want to look at the code of fzn2optimathsat.py, or at the output of fzn2optimathsat.py --help.

• --finite-precision N: number of decimals to be used when printing infinite-precision rational numbers as finite precision decimals; (Most MiniZinc solvers expect finite precision decimal numbers as an output; OptiMathSAT reasons with infinite precision).

• --int-enc: encode MiniZinc ints with the SMT-LIB Int type.

You should also be able to move those flags into the configuration (so that MiniZinc provides them to the solver), but I don't recall the exact syntax for that.

I have not found a way to do that. Adding these arguments to the contents of the "executable" field value does not work.

3. Are there really no mznlib files?

There are (see optimathsat docs). However, currently there is no performance improvement expectation so I'd recommend not using them.

Great work overall by the way, I look forward to using this solver!

You may also try to use dockers to play with the tool

• optimathsat_bv_mznc2020
• optimathsat_int_mznc2020

[GustavBjordal]

Possibly, I'm not sure how these tags are used. I'd include these files as part of the project once we get working configurations for all platforms from some generous contributor.

As far as I can tell, the tags are not really used for anything at this point, but can help users understand the capabilities of solvers. Specifically, we will be using optimathsat as part of a MiniZinc course (where we emphasize different solving technologies), so it in our case the tags can be beneficial to students.

I have not found a way to do that. Adding these arguments to the contents of the "executable" field value does not work.

I looked a bit more at it and this should do the trick:

{
  "id": "optimathsat_int",
  "name": "OptiMathSAT (NIRA)",
  "description": "OptiMathSAT + OMT(NIRA)",
  "version": "1.7.0",
  "mznlib": "",
  "executable": "/opt/fzn2omt/bin/fzn2optimathsat.sh",
  "tags": ["SMT","int"],
  "stdFlags": ["-a","-n","-p","-r","-f"],
  "supportsMzn": false,
  "extraFlags": [
    ["--bv-enc", "Encode ints with the SMT-LIB Bit-Vector type.", "bool", "false"],
    ["--int-enc", "Encode ints with the SMT-LIB Int type.", "bool", "true"],
    ["--cardinality-networks", "Enable cardinality networks (when applicable).", "bool", "false"],
    ["--finite-precision", "Print infinite-precision rational numbers as finite precision decimals using the specified precision level.", "int:2:32", "20"]
  ],
  "supportsFzn": true,
  "needsSolns2Out": true,
  "needsMznExecutable": false,
  "needsStdlibDir": false,
  "isGUIApplication": false
 }

However, I had not had time to actually test it completely yet. I'll have another look later.

Also, except for the "executable" line, the configurations should already be platform independent.

However, currently there is no performance improvement expectation so I'd recommend not using them.

That's actually very interesting, I guess this might be a trend for clause learning solvers then!

Thanks for all the answers!

[hakank]

Regarding the tags, they can be used to select a solver. E.g.

$ minizinc model.mzn --solver cp

will select a solver with the "cp" tag, but I'm not sure the exact way it selects this solver.

So, defining "smt" as a tag makes it possible to run optimathsat as $ minizinc model.mzn --solver smt

And I'm not sure how useful this is...

/Hakan

On Wed, Aug 26, 2020 at 11:44 AM GustavBjordal notifications@github.com wrote:

Possibly, I'm not sure how these tags are used. I'd include these files as part of the project once we get working configurations for all platforms from some generous contributor.

As far as I can tell, the tags are not really used for anything at this point, but can help users understand the capabilities of solvers. Specifically, we will be using optimathsat as part of a MiniZinc course (where we emphasize different solving technologies), so it in our case the tags can be beneficial to students.

I have not found a way to do that. Adding these arguments to the contents of the "executable" field value does not work.

I looked a bit more at it and this should do the trick:

{ "id": "optimathsat_int", "name": "OptiMathSAT (NIRA)", "description": "OptiMathSAT + OMT(NIRA)", "version": "1.7.0", "mznlib": "", "executable": "/opt/fzn2omt/bin/fzn2optimathsat.sh", "tags": ["SMT","int"], "stdFlags": ["-a","-n","-p","-r","-f"], "supportsMzn": false, "extraFlags": [ ["--bv-enc", "Encode ints with the SMT-LIB Bit-Vector type.", "bool", "false"], ["--int-enc", "Encode ints with the SMT-LIB Int type.", "bool", "true"], ["--cardinality-networks", "Enable cardinality networks (when applicable).", "bool", "false"], ["--finite-precision", "Print infinite-precision rational numbers as finite precision decimals using the specified precision level.", "int:2:32", "20"] ], "supportsFzn": true, "needsSolns2Out": true, "needsMznExecutable": false, "needsStdlibDir": false, "isGUIApplication": false }

However, I had not had time to actually test it completely yet. I'll have another look later.

However, currently there is no performance improvement expectation so I'd recommend not using them.

That's actually very interesting, I guess this might be a trend for clause learning solvers then!

Thanks for all the answers!

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/PatrickTrentin88/fzn2omt/issues/9#issuecomment-680776243, or unsubscribe https://github.com/notifications/unsubscribe-auth/AADH5HKQFCH4VRXEI3MZ6XTSCTKPHANCNFSM4NZ2OVIQ .

-- Hakan Kjellerstrand http://www.hakank.org/ http://www.hakank.org/webblogg/ http://www.hakank.org/constraint_programming_blog/ http://twitter.com/hakankj https://www.facebook.com/hakankj

[GustavBjordal]

Update on the flags:

It seems that "extraFlags" doesn't exactly do what I though it did. It only allows a user to pass these flags via MiniZinc, but MiniZinc will not pass them with their default values unless the user explicitly requests them.

As far as I can tell, the only way to currently tell MiniZinc to always call a solver with special flags is via User Configuration Files and the solverDefaults member. However, the user config file is not something that you can bundle with a solver, so this does not solve the issue.

However, I notice now that you actually have default values for these flags in fzn2optimathsat.py which means that it is not necessary for the user to provide them, right? In that case, the "extraFlags" solution is probably what you want.

[PatrickTrentin88]

Thanks for your suggestions. I have not yet made up my mind about this.

The best approach might be to have a default configuration file for OptiMathSAT and place there its configuration. I have to check whether this approach would work smoothly for the other solvers too.