$ Equidistant Frequency Permuation Arrays
$
$ modelled by Ian Gent, Paul McKay, Ian Miguel, Peter Nightingale and Sophie Huczynska
$ for further details see their paper:
$ http://www.cs.ualberta.ca/~nathanst/sara/papers/sara09_submission_8.pdf
$
$
$ ---- Parameters & Constants ----
  given d : int(1..)       $ hamming distance
  given lambda : int(1..)  $ occurrences
  given q : int(1..)       $ alphabet size
  given noCodes : int(1..) $ to generate
  given valuesArray : matrix indexed by [int(1..q)] of int(1..q)
  given occsArray : matrix indexed by [int(1..q)] of int(lambda..lambda)

  letting COLS be domain int(0..q*lambda-1)
  letting ROWS be domain int(0..noCodes-1)

$ ---- Decision Variables ----
  find codes : matrix indexed by[int(0..noCodes-1), COLS] of int(1..q)
  find pete : matrix indexed by[int(0..noCodes-2), int(0..q-1), 
    int(0..q-1)] of int(0..lambda)
$ pete is occurrences of values in blocks 0..q-1 of codeword. pete[code, block, symbol]=occs of symbol
  find cycleconfig : matrix indexed by[int(0..((noCodes*(noCodes-1))/2)-1)] of int(0..1)
  find fred : matrix indexed by[int(0..((noCodes*(noCodes-1))/2)-1), int(0..d-1)] of int(0..q*lambda-1)

  $ fredcodes is the elements of codes indexed by fred. fredcodes[code,0,..] are the ones
  find fredcodes : matrix indexed by[int(0..((noCodes*(noCodes-1))/2)-1), int(0..7)] of int(1..q)

$  find dave : matrix indexed by[int(0..((noCodes*(noCodes-1))/2)-1), int(0..q*lambda-1)] of int(0..1)
$ dave is occurrences of values in fred
$ ---- Constraints ----
such that

$ Symmetry breaking
  forall col : int(0..q*lambda-2) .
    codes[.., col] <=lex codes[..,col+1],    
  forall row : int(0..noCodes-2) .
    codes[row, ..] <=lex codes[row+1, ..],

$ gcc on code words
  forall row : ROWS .
    gcc (codes[row,..], valuesArray, occsArray),
    $forall val : int(1..q) . Get andrea to fix this.
    $   (atmost(codes[row,..], [lambda], [val]) /\ atleast(codes[row,..],[lambda],[val])),


$ Hamming distance -- it should be possible to take these out with fred.

  forall row1 : ROWS .
    forall row2 : int (row1+1..noCodes-1) .
      (sum col : COLS . codes[row1,col] != codes[row2,col]) = d,

$ Implied 
(implied=1)=>
  forall row : int(1..noCodes-1) .
    forall block : int(1 .. q) . 
(
      gcc (codes[row,(block-1)*lambda..(block*lambda-1)], 
           valuesArray, pete[row-1,block-1,..])  /\
      (pete[row-1, block-1, block-1]>=(lambda-(d/2))) /\
     $ sum up the columns in pete
      ( (sum col : int(0..q-1) . pete[row-1, col, block-1]) = lambda)
),

$$ fillin
$forall col : COLS .
  $codes[0, col]=(col/lambda)+1,

$ Now for fred.

$Can we use element as a gac disjunction, by 
$ making a new array of the elements indexe by
$ fred, then making them equal to 
$ places in codeword 2.
((d=4) /\ (usefred=1))=>
forall r1 : int(0..noCodes-2) .
  forall r2 : int(r1+1..noCodes-1) .
    (
    $ pairidx = ((noCodes-r1)*(noCodes-r1-1))/2+r2-r1
(
    $ two pairs
    ((cycleconfig[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1]=0) =>
    (
    $(codes[r1, fred[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1 , 1]] = 
        $codes[r2, fred[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1 , 0]]) /\
    $$ pair 2
    $(codes[r1, fred[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1 , 3]] = 
        $codes[r2, fred[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1 , 2]])  /\
    (fred[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1 , 2] < 
        fred[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1 , 3])
    )
    ) /\ 
    $ or one 4-cycle.
    ((cycleconfig[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1]=1) =>
    (
    $(codes[r1, fred[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1 , 1]] = 
        $codes[r2, fred[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1 , 2]])  /\
    $(codes[r1, fred[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1 , 3]] = 
        $codes[r2, fred[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1 , 0]])  /\
    $post that the two symbols swapped are not the same.in r1 or in r2.
    $(codes[r1, fred[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1 , 1]] != 
        $codes[r1, fred[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1 , 2]])  /\
    $(codes[r1, fred[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1 , 3]] != 
        $codes[r1, fred[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1 , 0]])  /\
    $(codes[r2, fred[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1 , 1]] != 
        $codes[r2, fred[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1 , 2]])  /\
    $(codes[r2, fred[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1 , 3]] != 
        $codes[r2, fred[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1 , 0]])  /\
    $ And Ian Gent's observation that they are alldiff for the 4-cycle. Makes a diff in nodes. 
    $ Otherwise, the four-cycle could be two two-cycles. Is this true? 
    $ fred 1,2,3,4 rotating 1,2,1,3 would give 3,1,2,1
    $ so use fred 1,4,2,3 (pairs) instead.
    $(codes[r1, fred[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1 , 0]] != 
        $codes[r1, fred[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1 , 2]])  /\
    $(codes[r1, fred[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1 , 1]] != 
        $codes[r1, fred[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1 , 3]])  /\
    $(codes[r2, fred[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1 , 0]] != 
        $codes[r2, fred[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1 , 2]])  /\
    $(codes[r2, fred[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1 , 1]] != 
        $codes[r2, fred[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1 , 3]]) 
  alldiff(fredcodes[(((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1), (1,3,5,7)]) 
    ))
) /\
    $Symmetry breaking, first element is least.
    (fred[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1 , 0] < 
        fred[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1 , 1]) /\
    (fred[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1 , 0] < 
        fred[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1 , 2]) /\
    (fred[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1 , 0] < 
        fred[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1 , 3])
    $ Common part of mapping r1 to r2 through fred.
    $(codes[r1, fred[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1 , 0]] = 
        $codes[r2, fred[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1 , 1]])  /\
    $(codes[r1, fred[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1 , 2]] = 
        $codes[r2, fred[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1 , 3]])  /\
    $ fred moves distinct indices around.
    $/\ alldiff(fred[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1 , ..])    $ slightly better time w/out alldiff, 4449
    $ Two symbols swapped are not the same -- common part.
    $/\ (codes[r1, fred[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1 , 0]] != 
        $codes[r1, fred[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1 , 1]])  /\
    $(codes[r1, fred[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1 , 2]] != 
        $codes[r1, fred[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1 , 3]])  /\
    $(codes[r2, fred[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1 , 0]] != 
        $codes[r2, fred[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1 , 1]])  /\
    $(codes[r2, fred[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1 , 2]] != 
        $codes[r2, fred[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1 , 3]])
  /\  (fredcodes[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1, 0]!= fredcodes[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1, 2])
  /\  (fredcodes[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1, 4]!= fredcodes[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1, 6])

$ All other elements stay in the same place.
/\ (
forall i : int(0..q*lambda-1) . 
    ((sum j : int(0..d-1) . fred[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1, j] = i) = 0)
    <=> (codes[r1,i]=codes[r2,i])   $ Potential bug: are we allowed the leftward implication? 
) /\

$ Extra stuff for disjunction based on element.
$ first set up fredcodes from r1  . Even numbers are for cycleconfig=0
(fredcodes[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1, 0]=
    codes[r1, fred[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1 , 1]]) /\
(fredcodes[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1, 2]=
    codes[r1, fred[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1 , 0]]) /\
(fredcodes[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1, 4]=
    codes[r1, fred[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1 , 3]]) /\
(fredcodes[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1, 6]=
    codes[r1, fred[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1 , 2]]) /\
$ odd numbers for cycleconfig=1
(fredcodes[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1, 1]=
    codes[r1, fred[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1 , 3]]) /\
(fredcodes[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1, 3]=
    codes[r1, fred[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1 , 0]]) /\
(fredcodes[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1, 5]=
    codes[r1, fred[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1 , 1]]) /\
(fredcodes[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1, 7]=
    codes[r1, fred[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1 , 2]]) /\
$ now the appropriate value from fredcodes goes into r2
(codes[r2, fred[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1, 0]]=
    fredcodes[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1, 
        cycleconfig[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1]]) /\
(codes[r2, fred[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1, 1]]=
    fredcodes[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1, 
        cycleconfig[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1]+2]) /\
(codes[r2, fred[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1, 2]]=
    fredcodes[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1, 
        cycleconfig[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1]+4]) /\
(codes[r2, fred[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1, 3]]=
    fredcodes[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1, 
        cycleconfig[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1]+6]) 

$ some vars in fredcodes are always equal. Makes no difference to nodes 4-4-4-9
$/\ (fredcodes[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1, 2]=fredcodes[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1, 3])
$/\ (fredcodes[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1, 6]=fredcodes[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1, 7])
)  $ end forall r1 and r2.

$ connect freds together

$ first, populate dave with the occurrences of values in fred.
$,forall fredidx : int(0..((noCodes*(noCodes-1))/2)-1) .
  $gcc(fred[fredidx,..], fredValuesArray, dave[fredidx,..])


$,forall r1 : int(0..noCodes-1).
 $forall r2 : int(r1+1..noCodes-1).
   $forall r3 : int(r2+1..noCodes-1).
     $((r1 != r2) /\ (r1 != r3) /\ (r2 !=r3))=>
     $(
      $$ composing the fred for r1:r2 and r2:r3 should be the fred for r1:r3
      $$ so each index in fred r1:r3 must be in one of the other two.
      $$ Much less than a full composition but may be worthwhile.
      $forall val : int(0..q*lambda-1) .
      $(
        $(((dave[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1, val]=0) /\
        $(dave[((noCodes-r2-1)*(noCodes-r2-2))/2+r3-r2-1, val]=0)) =>
        $(dave[((noCodes-r1-1)*(noCodes-r1-2))/2+r3-r1-1, val]=0) )
        $/\
        $(((dave[((noCodes-r1-1)*(noCodes-r1-2))/2+r3-r1-1, val]=0) /\
        $(dave[((noCodes-r2-1)*(noCodes-r2-2))/2+r3-r2-1, val]=0)) =>
        $(dave[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1, val]=0) )
        $/\ 
        $(((dave[((noCodes-r1-1)*(noCodes-r1-2))/2+r2-r1-1, val]=0) /\
        $(dave[((noCodes-r2-1)*(noCodes-r2-2))/2+r3-r2-1, val]=0)) =>
        $(dave[((noCodes-r1-1)*(noCodes-r1-2))/2+r3-r1-1, val]=0) )
        $$ add another couple of these for other ways 
        $$ of using r1,r2,r3
      $)
     $)

$ first thing: get new translator, or fix this so that it has arrays indexed from 0.
$ next: do proper thing with composing elements of fred together.