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

elements in fzn that are not supported #6

Closed oferst closed 4 years ago

oferst commented 4 years ago

Hi there, Getting the following messages:

c:\temp\fzn2omt-master>bin\fzn2optimathsat.py c:\temp\3zSx3MTpfJEQFcAJW-full.fzn
c:\temp\3zSx3MTpfJEQFcAJW-full.fzn:68590:
        error: constraint 'int_eq_imp' is not supported.
c:\temp\3zSx3MTpfJEQFcAJW-full.fzn:68590:
        error: constraint 'int_eq_imp' is not supported.
c:\temp\3zSx3MTpfJEQFcAJW-full.fzn:1:
        error: syntax error, unexpected ',', expecting ..
c:\temp\3zSx3MTpfJEQFcAJW-full.fzn:1:
        error: syntax error, unexpected ',', expecting ..

The first line in the fzn is

predicate int_eq_imp(var int: a,var int: b,var bool: r);

Is it really not supported ?

PatrickTrentin88 commented 4 years ago

@oferst OptiMathSAT 1.7.0.1 supports version 1.6 of the FlatZinc format, which does not include half-reified predicates. I can extend OptiMathSAT to support these predicates, but it might take a few days. How urgent is this?

oferst commented 4 years ago

I wouldn’t want to impose my needs on your schedule .... Whenever it is ready – it will be great if you let me know. Also – do you know if there is a way to restrict mzn2fzn to the fzn version that you support ?

Thank you, Patrick,

Ofer

PatrickTrentin88 commented 4 years ago

@oferst could you please help me reproduce your error?

I am looking at the files distributed with MiniZinc version 2.4.3, and only nosets.mzn appears to be using some half-reified predicates, such as:

set_eq_imp(...)
set_ne_imp(...)
set_le_imp(...)
set_lt_imp(...)
set_subset_imp(...)
set_superset_imp(...)
set_in_imp(...)

In particular,

predicate int_eq_imp(var int: a,var int: b,var bool: r);

does not appear to be defined anywhere. Are you using some non-standard redefinition? (e.g. linear)

oferst commented 4 years ago

here is an example,

var y ::output_var;
var bool: X_INTRODUCED_1 ::output_var;
var bool: X_INTRODUCED_2 ::output_var;
constraint int_eq_imp(y,0,X_INTRODUCED_1);
constraint int_eq_imp(y,1,X_INTRODUCED_2);
solve minimize y;

Thanks, Ofer

PatrickTrentin88 commented 4 years ago

@oferst I have released a new version of OptiMathSAT that includes half-reified predicates for all of the mandatory FlatZinc predicates. This should fix your issue.

Since you appear to be using a quite recent version of mzn2fzn, other issues may appear. Please do not hesitate to open a new ticket in such a case.

oferst commented 4 years ago

I redownloaded both but still apparently getting the half-reified issues (you can see below that it finds the new optimathsat). Could it be that the repository does not include the updated binaries ?

c:\temp\fzn2omt-master>bin\fzn2optimathsat.py c:\temp\Hakbatzot.fzn c:\temp\Hakbatzot.fzn:1: error: syntax error, unexpected int_eq_imp c:\temp\Hakbatzot.fzn:1: error: syntax error, unexpected int_eq_imp c:\temp\Hakbatzot.fzn:1: error: syntax error, unexpected ',', expecting .. c:\temp\Hakbatzot.fzn:1: error: syntax error, unexpected ',', expecting .. c:\temp\Hakbatzot.fzn:1: error: syntax error, unexpected int_eq_imp c:\temp\Hakbatzot.fzn:1: error: syntax error, unexpected int_eq_imp c:\temp\Hakbatzot.fzn:1: error: syntax error, unexpected ',', expecting .. c:\temp\Hakbatzot.fzn:1: error: syntax error, unexpected ',', expecting ..

c:\temp\fzn2omt-master>where optimathsat C:\temp\optimathsat-1.7.1-windows-64-bit-mingw\bin\optimathsat.exe

PatrickTrentin88 commented 4 years ago

@oferst I downloaded OptiMathSAT from the website, so I would exclude that. Could you please send me the file c:\temp\Hakbatzot.fzn?

oferst commented 4 years ago

it is the same file that I sent you this morning. Ofer

PatrickTrentin88 commented 4 years ago

@oferst I don't know whether this is due to the fact that you are replying to the messages via email instead of using the github page, but I haven't seen any file.

PatrickTrentin88 commented 4 years ago

NOTE: there has been a mixup and some messages related to this issue ended up in issue #7 . This issue is now solved.