search

conjure-cp / conjure

Conjure: The Automated Constraint Modelling Tool
Other
96 stars 24 forks source link

letting domains #64

Closed ozgurakgun closed 8 years ago

ozgurakgun commented 11 years ago

Originally reported by: Bilal Hussain (Bitbucket: Bilalh, GitHub: Bilalh)

Using the following essence 

language ESSENCE 2.0

letting V be domain int(1..3)

find x : set (minSize 1) of V
$ find x : set (minSize 1) of int(1..3)  $ works

such that
    3 in x

produces many eprimes the first: 

language ESSENCE' 1.0

find x_ExplicitVarSize_tuple1: matrix indexed by [int(1..3)] of bool
find x_ExplicitVarSize_tuple2: matrix indexed by [int(1..3)] of V
letting V be domain int(1..3)
such that
    exists v__6 : int(1..3)
        . x_ExplicitVarSize_tuple1[v__6] /\ x_ExplicitVarSize_tuple2[v__6] = 3,
    forAll v__1 : int(1..3)
        . (forAll v__2 : int(1..3)
               . v__1 < v__2 /\ x_ExplicitVarSize_tuple1[v__1]
                 /\
                 x_ExplicitVarSize_tuple1[v__2]
                 ->
                 x_ExplicitVarSize_tuple2[v__1] < x_ExplicitVarSize_tuple2[v__2]),
    forAll v__1 : int(1..2)
        . x_ExplicitVarSize_tuple1[v__1] <= x_ExplicitVarSize_tuple1[v__1 + 1],
    (sum v__3 : int(1..3) . x_ExplicitVarSize_tuple1[v__3]) >= 1

Should't V be refined and inlined to int(1..3)?

Running it in savilerow anyway produces the following error.

ERROR: In statement : find x_ExplicitVarSize_tuple2
ERROR: Right-hand side contains an identifier that is not a constant or parameter.
ozgurakgun commented 11 years ago

Original comment by Özgür Akgün (Bitbucket: ozgurakgun, GitHub: ozgurakgun):

on a second thought, inlining more stuff shouldn't be the solution, unless we do it for a good reason.

refix #63 without inlining letting-domain statements.

ozgurakgun commented 11 years ago

Original comment by Özgür Akgün (Bitbucket: ozgurakgun, GitHub: ozgurakgun):

fixes #63

ozgurakgun commented 11 years ago

Original comment by Özgür Akgün (Bitbucket: ozgurakgun, GitHub: ozgurakgun):

letting-domains statements do not necessarily need to be inlined, but here the problem is: we are creating new variables whose domain refer to these lettings but are inserted before them for some reason. a easy solution is to inline them. will do so.