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

compiler: constant folding can be improved #149

Closed
matsc-at-sics-se opened this Issue Mar 14, 2017 · 3 comments

Comments

Projects
None yet
2 participants
@matsc-at-sics-se

matsc-at-sics-se commented Mar 14, 2017

I'm working on a project where it's evident from the FlatZinc that the compiler's constant folding is far from optimal, which makes the flattened model bigger than necesssary. I can work around most of it, at the cost of obfuscating the MiniZinc model. Is this something that you plan to improve?

Here is a small artificial sample illustrating some problems:

array[1..2] of var bool: sel;
var 1..3: omatch;
var {1,33,113,116}: loc;

constraint
  let {var bool: b} in
  omatch in 3..3 /\
  (omatch=3 <-> sel[1]) /\
  loc in {1,33} /\
  loc in {1,116} /\
  (loc in 1..32 <-> b) /\
  (sel[1] -> b);

solve satisfy;

becomes:

var bool: X_INTRODUCED_0:: is_defined_var;
var bool: X_INTRODUCED_1;
var 3..3: omatch:: output_var;
var 1..1: loc:: output_var;
var bool: X_INTRODUCED_2 ::var_is_introduced :: is_defined_var;
array [1..2] of var bool: sel:: output_array([1..2]) = [X_INTRODUCED_0,X_INTRODUCED_1];
constraint bool_clause([X_INTRODUCED_2],[X_INTRODUCED_0]);
constraint int_eq_reif(omatch,3,X_INTRODUCED_0):: defines_var(X_INTRODUCED_0);
constraint set_in_reif(1,1..32,X_INTRODUCED_2):: defines_var(X_INTRODUCED_2);
solve  satisfy;
@guidotack

This comment has been minimized.

Member

guidotack commented Mar 14, 2017

Thanks for the example, I had seen this before but hadn't had time yet to track it down. I've just pushed a fix that should solve it at least for this type of constant folding.

guidotack added a commit that referenced this issue Mar 14, 2017

For operator x in a..b, check if a=b and set right and side of x acco…
…rdingly. Enables some additional constant folding. Partially fixes #149.

guidotack added a commit that referenced this issue Mar 14, 2017

Keep track of unification during optimisation. Fixes #149.
A VarDecl could be in the queue for optimisation while it is being unified with another VarDecl. In that case, we need to check if it was re-written and removed and optimise the target of the rewriting instead.
@matsc-at-sics-se

This comment has been minimized.

matsc-at-sics-se commented Mar 15, 2017

guidotack added a commit that referenced this issue Mar 16, 2017

Keep track of unification during optimisation. Fixes #149.
A VarDecl could be in the queue for optimisation while it is being unified with another VarDecl. In that case, we need to check if it was re-written and removed and optimise the target of the rewriting instead.

@guidotack guidotack closed this in 032d72b Mar 16, 2017

@guidotack

This comment has been minimized.

Member

guidotack commented Mar 19, 2017

It's part of 2.1.4.

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