[gecode-users] BoolExpr example

[Malcolm Ryan]

So... some clarifying questions:

1) What's the difference between BoolVarArgs and BoolVarArray?

2) Could you explain in more detail what ~ does?

3) Likewise, what does tt() do?

4) Under exactly what conditions does post() create a BoolVar?

5) How's the documentation coming along?

Malcolm

On 20/11/2008, at 6:30 PM, Mikael Zayenz Lagerkvist wrote:

> On Thu, Nov 20, 2008 at 7:52 AM, Malcolm Ryan <malcolmr at cse.unsw.edu.au 
> > wrote:
>> I'm not sure I understand that code. Would you mind explaining in  
>> more
>> detail?
>
> First of all, the loops in the code looping through layers can be
> ignored for exposition, since they are there to handle the cases when
> cards are in the bottom, middle, or top of a pile of three cards.
> Assume that we have two piles of card (X1, X2, X3) and (Y1, Y2, Y3)
> where Xv and Xv are integer variables, and where X2 and Y2 have the
> same function for purposes of the game. The values of the cards
> represent when they are played (note that I mistranslated the
> condition in my earlier post, X1 and Y1 should be exchanged, as should
> X3 and Y3). Now the code can be simplified to
>  // cond is the condition for the symmetry
>   BoolVarArgs ba(4);
>   // Both cards played after the ones on top of them
>   ba[0] = post(this, ~(X2 < Y3));
>   ba[1] = post(this, ~(Y2 < X3));
>   // Both cards played before the ones under them
>   ba[2] = post(this, ~(Y1 < X2));
>   ba[3] = post(this, ~(X1 < Y2));
>   // Cond holds when all the above holds
>   BoolVar cond(this, 0, 1);
>   rel(this, BOT_AND, ba, cond);
>
>   // If cond is fulfilled, then we can order the cards
>   // cond -> (X2 < Y2)
>   post(this, tt(!cond || ~(X2 < Y2)));
>
> The ba-array holds a set Boolean variables for reified relations, and
> the rel-function takes the conjunction of these. The final post just
> uses the standard unfolding of an implication since there is no
> implication-operator. You can also use the implication-function
> together with post to get it:
>   post(this, tt(imp(cond, ~(X2 < Y2))));
>
>
>> How do you do reified constraints in Gecode?
>
> By using the reified post-functions, such as
>   rel(this, x, IRT_LE, y, b);
> with x and y integer variables and b a Boolean control variable. In
> MiniModel expressions, you can use the unary tilde-operator to reify
> an expression:
>   BoolVar b = post(this, ~(x < y));
>
> Cheers,
> Mikael
>
> -- 
> Mikael Zayenz Lagerkvist, http://www.ict.kth.se/~zayenz/