isa-group/IDLReasoner

MiniZinc implementation differs from Designer

Closed this issue · 3 comments

AML14 commented

I realized this while testing the isDeadParameter operation. The following IDL specification:

Or(p1, p2, p3, p4, p5);
OnlyOne(p1, p2);
p4>=p5;
Or(p1==true, p4==1 OR p2);
OnlyOne(p3, p5);
p2!=p3;
OnlyOne(p2 AND p3, p4 AND p5);
NOT Or(p2=='ejemplo', p5==4);

which translates to the following MiniZinc:

var bool: p1;
var 0..1: p1Set;
var 0..10000: p2;
var 0..1: p2Set;
var {1, 2, 3, 4, 5}: p3;
var 0..1: p3Set;
var {1, 2, 3, 4, 5}: p4;
var 0..1: p4Set;
var {1, 2, 3, 4, 5}: p5;
var 0..1: p5Set;

constraint (((p1Set==1)) \/ ((p2Set==1)) \/ ((p3Set==1)) \/ ((p4Set==1)) \/ ((p5Set==1)));
constraint ((((p1Set==1)) -> ((not ((p2Set==1))))) /\ (((p2Set==1)) -> ((not ((p1Set==1))))) /\ (((p1Set==1)) \/ ((p2Set==1))));
constraint ((p4Set==1 /\ p5Set==1) -> (p4>=p5));
constraint (((p1Set==1 /\ p1==true)) \/ ((p4Set==1 /\ p4==1) \/ (p2Set==1)));
constraint ((((p3Set==1)) -> ((not ((p5Set==1))))) /\ (((p5Set==1)) -> ((not ((p3Set==1))))) /\ (((p3Set==1)) \/ ((p5Set==1))));
constraint ((p2Set==1 /\ p3Set==1) -> (p2!=p3));
constraint ((((p2Set==1) /\ (p3Set==1)) -> ((not ((p4Set==1) /\ (p5Set==1))))) /\ (((p4Set==1) /\ (p5Set==1)) -> ((not ((p2Set==1) /\ (p3Set==1))))) /\ (((p2Set==1) /\ (p3Set==1)) \/ ((p4Set==1) /\ (p5Set==1))));
constraint (not (((p2Set==1 /\ (p2==0))) \/ ((p5Set==1 /\ p5==4))));
solve satisfy;

should be solvable. Designer returns a solution for it, but IDLReasoner's MiniZinc implementation does not. Just for the record, I manually checked this issue and it should actually return a solution, therefore Designer is right and IDLReasoner is wrong.

AML14 commented

Also for the record, I tried manually calling the MiniZinc exe from the prompt, and the result is the same. Therefore, the problem has most probably to do with the MiniZinc implementation or version.

AML14 commented

The problem is FOR SURE with this constraint:

NOT Or(p2=='ejemplo', p5==4);

which is mapped to

constraint (not (((p2Set==1 /\ (p2==0))) \/ ((p5Set==1 /\ p5==4))));

If p2 is forced to be present (i.e. p2Set=1), it fails to find a solution, and that shouldn't happen. A possible solution would be p2Set=1, p2=1, p5Set=0.

AML14 commented

This is a confirmed bug in MiniZinc (MiniZinc/libminizinc#359). We have to wait until they release the new version.