search

PatrickTrentin88 / fzn2omt

Tools/Scripts to convert MiniZinc/FlatZinc to Optimization Modulo Theories (OMT) for BCLT, OptiMathSAT or Z3 and Satisfiability Modulo Theories (SMT) for CVC4.
8 stars 0 forks source link

Solution recovery for fzn2z3.py #4

Closed JoanEspasa closed 4 years ago

JoanEspasa commented 4 years ago

These days I'm trying to incorporate the fzn2omt scripts in a bigger pipeline to test the encodings thoroughly :)

I'm running some comparisons and I see that the fzn2optimathsat returns the solution in a fzn format, but its not the case with the fzn2z3, as it returns the solution in the Z3 format.

Would it be possible for it to return it also in a fzn format?

Thanks!

PatrickTrentin88 commented 4 years ago

@JoanEspasa This is because OptiMathSAT has a native FlatZinc interface, whereas Z3, Barcelogic and CVC4 do not.

This might take some time to get done.

JoanEspasa commented 4 years ago

Thanks Patrick!

We use that mainly for correctness validation (i.e. the encoding and solver are sound and complete)

PatrickTrentin88 commented 4 years ago

@JoanEspasa This issue is now fixed.

This project now requires OptiMathSAT 1.7.0 or better in order to work. The release will follow in a few days.