New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Issue with optimized compilation for partially defined mydiv function #54

Alexander-Schiendorfer opened this Issue Sep 29, 2015 · 1 comment


None yet
2 participants

Alexander-Schiendorfer commented Sep 29, 2015

When trying the user-defined partial function example mydiv from the Coursera class, I noticed some problems with compiler optimizations (also here Gist) :

function var int:mydiv(var int: x, var int: y) = 
  assert(lb(x) >= 0 /\ lb(y) >= 0,
         "Mydiv got wrong arguments",
         let {constraint y != 0 } in 
         safediv(x, y)

function var int: safediv(var int: x, var int: y)   :: promise_total = 
  let {
    var 0..ub(x): q;
    var 0..ub(y)-1: r;
    constraint q*y + r = x;
    constraint r < y;
  }  in q;

var int: x;
var int: y; 
var int: z;

constraint x = 7;
constraint y = 1;
constraint z = mydiv(x,y);

% should return z = 7
solve satisfy;

which returns { (7,1,i) | i in 0..7} as solution set when producing optimized FlatZinc.

*. When declaring var 0..ub(y)-1: r; as var int: r;' with optimized FlatZinc, the correct (only) solution(7,1,7)` is returned. Then, the constraints

array [1..3] of int: X_INTRODUCED_5 = [1,-1,-1];
array [1..2] of int: X_INTRODUCED_6 = [1,-1];

are present, whereas they weren't in the original version. The original FlatZinc is obscurely small:

var 0..7: z:: output_var;
solve  satisfy;
  • When compiling the model without the flag for optimized FlatZinc, I get the correct solution set.

I'm using the bundled MiniZinc IDE, Version 0.9.9.


This comment has been minimized.


guidotack commented Sep 30, 2015

Thanks a lot, that was a bug in the optimisation phase of the compiler (completely unrelated to partial functions, but triggered by this example). It will be fixed in the next release (which should have happened today, but there were a few showstoppers like this one).

@guidotack guidotack closed this in aa8347e Oct 5, 2015

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment