[gecode-users] Linear expressions in 'post'

[Andrea Rendl]

Dear Gecoders,

I've noticed that Gecode is very effective with solving linear
expressions (Gecode::MiniModel::LinExpr)  given in the 'post'
constraint. I was wondering how you deal with them internally. I guess
you build some kind of expression tree from the linear expression and
then map the tree to an adequate 'linear' constraint? How do you deal
with more 'complex' linear expressions that you cannot directly map to
linear, such as

x + c1 != y + c2                   (where x,y are IntVars and c1,c2
are constants)

In this case, do you internally re-write the expression to 'x + c1 - y
!= c2' (or similar) to match with linear? If yes, are there any
particular rules you apply for re-writing? I assume there is no case
where you flatten any expressions (and introduce auxiliary variables
internally)? If there exists some published work on it, I'd be happy
if you could point it out to me.

Thank you,
Andrea