search

conjure-cp / conjure

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

Set of lettings #66

Closed ozgurakgun closed 7 years ago

ozgurakgun commented 11 years ago

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

Using this essence

language Essence 2.0

letting V be domain int(1..n)
letting SS be domain set of V
letting n be 3
letting CC be domain set of tuple (V, SS)

find x : set of tuple (V,int(1..n),int(1..4))
find y : CC

such that
    (2,3,4) in x,
    (1,{3}) in y

produces 


language ESSENCE' 1.0

letting V be domain int(1..3)
letting SS be domain set of V
letting CC be domain set of (V, SS)
find x_ExplicitVarSize_tuple1: matrix indexed by [int(1..36)] of bool
find x_ExplicitVarSize_tuple2_tuple1: matrix indexed by [int(1..36)] of V
find x_ExplicitVarSize_tuple2_tuple2:
        matrix indexed by [int(1..36)] of int(1..3)
find x_ExplicitVarSize_tuple2_tuple3:
        matrix indexed by [int(1..36)] of int(1..4)
find y: CC
such that
    exists v__4 : int(1..36)
        . x_ExplicitVarSize_tuple1[v__4]
          /\
          (x_ExplicitVarSize_tuple2_tuple1[v__4] = 2
           /\
           (x_ExplicitVarSize_tuple2_tuple2[v__4] = 3
            /\
            x_ExplicitVarSize_tuple2_tuple3[v__4] = 4)),
    exists v__5 in y
        . v__5[1] = 1
          /\
          ((forAll v__6 in v__5[2] . 3 = v__6) /\ (exists v__9 in v__5[2] . v__9 = 3)),
    forAll v__1 : int(1..36)
        . (forAll v__2 : int(1..36)
               . v__1 < v__2 /\ x_ExplicitVarSize_tuple1[v__1]
                 /\
                 x_ExplicitVarSize_tuple1[v__2]
                 ->
                 x_ExplicitVarSize_tuple2_tuple1[v__1] != x_ExplicitVarSize_tuple2_tuple1[v__2]
                 \/
                 (x_ExplicitVarSize_tuple2_tuple2[v__1] != x_ExplicitVarSize_tuple2_tuple2[v__2]
                  \/
                  x_ExplicitVarSize_tuple2_tuple3[v__1]
                  !=
                  x_ExplicitVarSize_tuple2_tuple3[v__2])),
    forAll v__1 : int(1..35)
        . x_ExplicitVarSize_tuple1[v__1] <= x_ExplicitVarSize_tuple1[v__1 + 1]

Not sure if it conjure bug for not refining enough or a savilerow bug

ozgurakgun commented 11 years ago

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

fixes #65 -- generated files in the repo.