Discussion about the Alice programming system

Guido Tack | 21 Sep 2007 10:43

Re: 2 questions on constraints (x=a or b, FD.gcc arguments)

gabriele renzi wrote:

> 1) is it possible to express a constraint so that an FD.intvar is  
> bound to
> be one of two choices which are themselves FD.intvar's ?
> I believe this should be done with FD.gcc4 but I'm not sure if this  
> is the
> right thing.

Do you mean a constraint like (x = y) or (x = z)?  That's not what  
gcc is used for, but you can use reified constraints to achieve this:

val b1 = FD.boolvar space
val b2 = FD.boolvar space
val b3 = FD.intvar2boolvar(space, FD.intvar(space, #[(1,1)]))   (* b3  
= true *)
val _ = FD.disj(space, b1, b2, b3)   (* b1 or b2 = b3 *)
val _ = FD.Reified.rel(space, x, FD.eq, y, b1)    (* x == y    <=>   
b1 *)
val _ = FD.Reified.rel(space, x, FD.eq, z, b2)    (* x == z    <=>   
b2 *)

> 2) about gcc*: what is the meaning of all the paramaters in the
> various FD.gcc ?
> [s,x,min,max,level] are clear from the description, but
> [v,c,m,ulow,uup,all] are not so obvious, in my humble opinion.

You're right, they are not obvious at all, and the documentation for  
gcc practically doesn't exist.  In fact, we realized that this  
interface doesn't work as expected for some cases, and -

(Continue reading)

headers

gabriele renzi | 21 Sep 2007 23:14

Re: 2 questions on constraints (x=a or b, FD.gcc arguments)

On Fri, 21 Sep 2007 10:43:15 +0200, Guido Tack wrote:

> Do you mean a constraint like (x = y) or (x = z)?  That's not what  
> gcc is used for, but you can use reified constraints to achieve this:
> 
> val b1 = FD.boolvar space
> val b2 = FD.boolvar space
> val b3 = FD.intvar2boolvar(space, FD.intvar(space, #[(1,1)]))   (* b3  
> = true *)
> val _ = FD.disj(space, b1, b2, b3)   (* b1 or b2 = b3 *)
> val _ = FD.Reified.rel(space, x, FD.eq, y, b1)    (* x == y    <=>   
> b1 *)
> val _ = FD.Reified.rel(space, x, FD.eq, z, b2)    (* x == z    <=>   
> b2 *)

one more thing:
I think that reifying with FD.Reified is equivalent to using
Modeling.HOLDS, is this true?
If true, am I right in thinking that the above is somewhat the
same as 

 Modeling.postTrue(space, Modeling.HOLDS(x`=y) `| Modeling.HOLDS(x`=z) ) 

where x,y and z are terms instead of intvars (types seem correct) ?

headers

gabriele renzi | 21 Sep 2007 11:37

Re: 2 questions on constraints (x=a or b, FD.gcc arguments)

On Fri, 21 Sep 2007 10:43:15 +0200, Guido Tack wrote:

> Do you mean a constraint like (x = y) or (x = z)?  That's not what  
> gcc is used for, but you can use reified constraints to achieve this:

yes. I thought I could express this via a cardinality constraint on the
triple [x,y,z] imposing that there are exactly two different values, and 
that I could do this via gcc.

Actually I also gave some thought to the idea of using FD.count, but it
seems that there is a mismatch between the signatures:
    countII : space * intvar vector *  int * relation * int -> unit
    countVI : space * intvar vector *  intvar * relation * int -> unit
    countIV : space * intvar vector *  int * relation * intvar -> unit
    countVV : space * intvar vector *  intvar * relation * intvar -> unit

and the documentation

    countII (s, v, rel1, n, rel2, m level)
    countVI (s, v, rel1, x, rel2, m level)
    countIV (s, v, rel1, n, rel2, y level)
    countVV (s, v, rel1, x, rel2, y level)

(the rel1 in the latters doesn't seem to be there in the formers) 
so I gave up on it. 

<snip code>
I see this makes sense. And I didn't know I could express a domain
directly through its representation :)

(Continue reading)