search

MiniZinc / libminizinc

The MiniZinc compiler
http://www.minizinc.org
Other
499 stars 78 forks source link

any support for Z3 solver? #161

Closed yogeshVU closed 6 years ago

yogeshVU commented 7 years ago

feature request: would be nice to have support for the Z3 solver

guidotack commented 7 years ago

There's a converter from FlatZinc to SMT-LIB format at http://ima.udg.edu/Recerca/lap/fzn2smt/ I haven't tried it myself but I've heard that it still works with current versions of MiniZinc.

Dekker1 commented 6 years ago

This issue is being closed in a cleanup of our GitHub repository. It seems it has been fully discussed to not be an (compiler) issue, already solved, or no longer relevant.

If this not be the case, feel free to comment below and we'll reconsider the issue again.

jarble commented 7 months ago

@Dekker1 and @guidotack: Are there no plans to support Z3 as a solver for MiniZinc? A FlatZinc-to-SMT-LIB converter is still available here.

Dekker1 commented 7 months ago

Although an SMT interface from MiniZinc would certainly be valuable, we currently don't have any plans to create such an interface due to time constraints of the MiniZinc team.

If, however, someone wants to get their hands dirty, then I would urge them to contact us. I certainly have some ideas of how such an interface would work, and I would be very happy to mentor someone in writing the solver backend.