output of solvers

[oferst]

The fzn files I am generating with mzn2fzn are full with thousands of declarations such as var bool: X_INTRODUCED48:: output_var; (even if there is no OUTPUT statement in the mzn file, by the way). I assume that this is the reason that the output of e.g. fzn2z3 gives value to all those internal variables. Is there a way to just see the output of the mzn decision variables ? Thanks.

[PatrickTrentin88]

The fzn files I am generating with mzn2fzn are full with thousands of declarations such as var bool: X_INTRODUCED48:: output_var;

These are artificial variables introduced by the mzn2fzn compiler.

(even if there is no OUTPUT statement in the mzn file, by the way).

That's the problem. Since there is no output statement in the MiniZinc model, all variables are promoted to output variables by the mzn2fzn compiler.

I assume that this is the reason that the output of e.g. fzn2z3 gives value to all those internal variables.

Correct.

Is there a way to just see the output of the mzn decision variables ?

Provide an output statement listing all and only the variables you are interested in.

Thanks.

I am closing this issue because it is not caused by fzn2omt but by mzn2fzn.

[oferst]

I rechecked the output issue. Even when the mzn file contains an output statement, the output of fzn2z3 contains all those auxiliary variables, and only a few of the variables that were in the original output statement. The formatted output itself (including labels) is not part of the output. I guess minizinc prints this formatted output based on the result from the solver. I am attaching a sample mzn (please rename the extension .txt to .mzn). See the output statement in lines 611-649.

Ofer

[note: edited because too long]

[PatrickTrentin88]

@oferst Yeah, I guess I was wrong on this. In the future, I ought to test the information I am giving first or properly signal that I haven't.

In any case, fzn2z3.py prints all and only those variables marked as output variables in the FlatZinc file by the mzn2fzn compiler. There is no way for me to fix this issue without violating the FlatZinc Specification.

---

[I haven't personally tested what follows]

What you may want to try to do is to configure the solvers distributed with fzn2omt as MiniZinc backends.

e.g. 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

Since now minizinc is in control, I believe (but I cannot guarantee) that the output should be properly formatted, similarly to what happens with other FlatZinc solvers.

Unfortunately, I haven't got the chance to test setting up the fzn2omt solvers as MiniZinc back-ends by myself. However, I know for a fact that someone else got it working.

---

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).

[oferst]

Thanks for the detailed answer! Regarding the option of adding an smt solver into the pool of minizinc solvers: Is there an option to hook fzn2z3 itself to minizinc ? this will enable solving with z3.

-- Ofer

From: PatrickTrentin88 notifications@github.com Sent: Wednesday, June 10, 2020 1:19 AM To: PatrickTrentin88/fzn2omt fzn2omt@noreply.github.com Cc: Ofer Strichman ofers@technion.ac.il; Mention mention@noreply.github.com Subject: Re: [PatrickTrentin88/fzn2omt] output of solvers (#8)

@ofersthttps://eur01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Foferst&data=02%7C01%7Cofers%40technion.ac.il%7C2bfc41b3c8514b4f31fb08d80cc33829%7Cf1502c4cee2e411c9715c855f6753b84%7C1%7C0%7C637273379883335115&sdata=s%2FBLtUd7RgLIwtBoUBTQRgrcc2rNstGlE0%2FQXMl5zQY%3D&reserved=0 Yeah, I guess I was wrong on this. I should have tested first, before answering. In any case, fzn2z3.py prints all and only those variables marked as output variables in the FlatZinc file by the mzn2fzn compiler, as requested by the standard. There is no way for me to fix this issue because the original MiniZinc model is not available.

---

What you may want to try to do is to configure the solvers distributed with fzn2omt as a MiniZinc backendshttps://eur01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwww.minizinc.org%2Fdoc-2.4.3%2Fen%2Fsolvers.html&data=02%7C01%7Cofers%40technion.ac.il%7C2bfc41b3c8514b4f31fb08d80cc33829%7Cf1502c4cee2e411c9715c855f6753b84%7C1%7C0%7C637273379883345111&sdata=jKKqib%2BzLIf6u%2BzCbpSouXDHnGSkqN%2F6oDh%2FaZJjGzA%3D&reserved=0.

e.g. 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

Since now minizinc is in control, I believe that the output should be properly formatted.

Unfortunately, I haven't got the chance to test this myself, but I know for a fact that someone else got it working.

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHubhttps://eur01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2FPatrickTrentin88%2Ffzn2omt%2Fissues%2F8%23issuecomment-641611472&data=02%7C01%7Cofers%40technion.ac.il%7C2bfc41b3c8514b4f31fb08d80cc33829%7Cf1502c4cee2e411c9715c855f6753b84%7C1%7C0%7C637273379883345111&sdata=I4G9pJh1i6jDxdil7gR5tku5UxQ69hpypB7yN3xqcuc%3D&reserved=0, or unsubscribehttps://eur01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fnotifications%2Funsubscribe-auth%2FACLFDDCQQ5QV6CBBWBNQY6DRV2YOZANCNFSM4NS6WC2A&data=02%7C01%7Cofers%40technion.ac.il%7C2bfc41b3c8514b4f31fb08d80cc33829%7Cf1502c4cee2e411c9715c855f6753b84%7C1%7C0%7C637273379883355104&sdata=jsPDeH8LbulRAaoMrXxJrf54b5KiKFenuukEi1t%2FzW0%3D&reserved=0.

This email is from an external mail server, be judicious when opening attachments or links

[PatrickTrentin88]

Thanks for the detailed answer! Regarding the option of adding an smt solver into the pool of minizinc solvers: Is there an option to hook fzn2z3 itself to minizinc ? this will enable solving with z3.

Perhaps I was not clear in my previous message, but the idea is exactly that: add one configuration file for each fzn2<whatever>.py solver (or solver configuration), including fzn2z3.py.