/* 

  Swedish Personal Number (Social number) in Picat.

  A study in Swedish personal identity numbers (pnos).

  A pno is a 10 digit number, YYMMDD-NNNC:
   YY: Year
   MM: Month
   DD: Day
   NNN: Birth number
   C: Check digit (check sum)

  http://en.wikipedia.org/wiki/Personal_identity_number_%28Sweden%29
  """
  To calculate the checksum, multiply the individual digits in the identity number 
  and 212121-212. The resulting products (a two digit product, such as 16, would be 
  converted to 1 + 6) are added together. The checksum is the last digit of 10 minus 
  the last digit in this sum (note that if the last digit of the sum is zero, 
  the checksum is 0).
  
  Example:
  
    811228-987x gives
  [
    8*2 + 1*1 + 1*2 + 2*1 + 2*2 + 8*1 + 9*2 + 8*1 + 7*2
    1+6 + 1   + 2   + 2   + 4   + 8   + 1+8 + 8   + 1+4 =  46
  ]
  
  The sum 46 has the last digit of 6. That is then subtracted from ten to give the value: 
  x = 10 - 6 = 4; the checksum is the last digit (in this example, the only digit) of this: 4
  
  If the sum had been 50, then subtraction of the last digit 0 from 10 would give the 
  value x = 10 - 0 = 10. The last digit of this is 0 which would be the resulting checksum.
  """


  Some explorations:

  * There are - in theory - max 99*12*(29+4*30+7*31)*999 = 434 373 192 different pnos.
    This model generates exactly 32 543 100 numbers.

  * 39 binary pnos:
  0101101111
  0101111011
  0110011111
  0110101011
  0110110111
  0110111101
  0111011011
  0111100111
  0111101101
  0111110011
  0111111001
  1001011111
  1001101011
  1001110111
  1001111101
  1010011011
  1010100111
  1010101101
  1010110011
  1010111001
  1011010111
  1011011101
  1011100011
  1011101001
  1011110101
  1101011011
  1101100111
  1101101101
  1101110011
  1101111001
  1110010111
  1110011101
  1110100011
  1110101001
  1110110101
  1111010011
  1111011001
  1111100101
  1111110001

  * 295 palindromic pnos, e.g.
  6611221166
  6612112166
  6701221076
  6702112076
  6705115076
  6710220176
  6711111176
  6801111086
  6810110186
  7004224007
  7007227007
  7008118007
  7103223017
  7104114017
  7106226017
  7107117017
  7112222117
  7202222027
  7203113027
  7205225027
  7206116027
  7211221127
  7212112127

  * 573 increasing pnos, e.g.
  0112237888
  0112259999
  0112278999
  0112288899
  1111222228
  1111222236
  1111222244
  1111222269

  * 5 decreasing pnos
  3211111111
  6511111111
  7311111111
  8111111111
  9911111111

  * no binary and palindromic pnos
  * no increasing and palindromic pnos

  * 180 double digits pnos, e.g.
  1111111199
  3311111144
  3311111177
  3311112233
  6611223311
  6611225522
  6611225555
  6611226611
  7711110044
  7711110077
  7711111133
  7711111166
  7711112222
%

  * 43488 pnos with just even digits
  * 7875 pnos with just odd digits

  * min and max pno are 0101010007 and 9912319994
  
  * 345 "twin" pnos (YYMMDYYMMD), e.g.
  6705167051
  6710267102
  6711167111
  6801168011
  6810168101
  7004270042
  7007270072
  9110291102
  9111191111
  9201192011

  * no single digit pnos

  * 229 two digits pnos, e.g. binary pnos (see above) and
  0202020202
  0404040404
  0505050005
  0606060606
  0808080808
  1212121212
  7707070707
  8111111111
  8111118181
  9111111119
  9911111111
  
  * 24486 three digit pnos

  * no pnos with just prime numbers as digits (2,3,5,7}

  


  This Picat model was created by Hakan Kjellerstrand, hakank@gmail.com
  See also my Picat page: http://www.hakank.org/picat/

*/

import util.
import cp.

main => go.

go ?=>
  % test (the example above: 8112289874)
  Year = 81,
  Month = 12,
  Day = 28,
  BirthNo = 987,
  check_pno(_PNO,Year,Month,Day,BirthNo,_Checksum),
  fail,
  nl.
go => true.

% There are 3 pnos that have the form 8112DD-9874,
% i.e. with an unknown day:
%   8112029874
%   8112109874
%   8112289874
% i.e the days 2,10, and 28
%
go2 ?=>
  Year = 81,
  Month = 12,
  BirthNo = 987,
  Checksum = 4,
  check_pno(_PNO,Year,Month,_Day,BirthNo,Checksum),
  fail,
  nl.
go2 => true.


% Max PNO
go3 ?=>
  Year = 99,
  Month = 12,
  Day = 31,
  BirthNo = 999,
  check_pno(_PNO,Year,Month,Day,BirthNo,_Checksum),
  fail,
  nl.
go3 => true.

% Min PNO
go4 ?=>
  Year = 1,
  Month = 1,
  Day = 1,
  BirthNo = 0,
  check_pno(_PNO,Year,Month,Day,BirthNo,_Checksum),
  fail,
  nl.
go4 => true.

% Binary PNOs 
go5 ?=>
  N = 10,
  PNO = new_list(N),
  foreach(I in 1..N)
    PNO[I] #<= 1
  end,
  check_pno(PNO,_Year,_Month,_Day,_BirthNo,_Checksum),
  fail,
  nl.
go5 => true.

% Palindromic pnos
go6 ?=>
  N = 10,
  PNO = new_list(N),
  foreach(I in 1..N div 2)
    PNO[I] #= PNO[N-I+1]
  end,
  check_pno(PNO,_Year,_Month,_Day,_BirthNo,_Checksum),
  fail, 
  nl.
go6 => true.

% Sorted pnos: increasing
go7 ?=>
  N = 10,
  PNO = new_list(N),
  increasing(PNO),
  check_pno(PNO,_Year,_Month,_Day,_BirthNo,_Checksum),
  fail, 
  nl.
go7 => true.

% Sorted pnos: decreasing
go8 ?=>
  N = 10,
  PNO = new_list(N),
  decreasing(PNO),
  check_pno(PNO,_Year,_Month,_Day,_BirthNo,_Checksum),
  fail, 
  nl.
go8 => true.

% Only odd digits
go9 ?=>
  N = 10,
  PNO = new_list(N),
  foreach(I in 1..N)
     PNO[I] mod 2 #= 1
  end,
  check_pno(PNO,_Year,_Month,_Day,_BirthNo,_Checksum),
  fail, 
  nl.
go9 => true.

% Only even digits
go10 ?=>
  N = 10,
  PNO = new_list(N),
  foreach(I in 1..N)
     PNO[I] mod 2 #= 0
  end,
  check_pno(PNO,_Year,_Month,_Day,_BirthNo,_Checksum),
  fail, 
  nl.
go10 => true.


% Double digits
go11 ?=>
  N = 10,
  PNO = new_list(N),
  foreach(I in 1..N div 2)
     PNO[2*I-1] = PNO[2*I]
  end,
  check_pno(PNO,_Year,_Month,_Day,_BirthNo,_Checksum),
  fail, 
  nl.
go11 => true.


% "Twin" pno: YYMMDDYYMMDD
go12 ?=>
  N = 10,
  PNO = new_list(N),
  foreach(I in 1..N div 2)
     PNO[I] #= PNO[(N div 2)+I]
  end,
  check_pno(PNO,_Year,_Month,_Day,_BirthNo,_Checksum),
  fail, 
  nl.
go12 => true.

% Single digit numbers
go13 ?=>
  N = 10,
  PNO = new_list(N),
  foreach(I in 1..N-1)
     PNO[I] #= PNO[I+1]
  end,
  check_pno(PNO,_Year,_Month,_Day,_BirthNo,_Checksum),
  fail, 
  nl.
go13 => true.

% Just two digits
go14 ?=>
  N = 10,
  PNO = new_list(N),
  GCC = new_list(10),
  GCC :: 0..10,
  global_cardinality(PNO,$[I-GCC[I+1]: I in 0..9]),
  sum([GCC[I] #> 0 : I in 1..N]) #= 2,
  check_pno(PNO,_Year,_Month,_Day,_BirthNo,_Checksum),
  fail, 
  nl.
go14 => true.


% Just three digits
go15 ?=>
  N = 10,
  PNO = new_list(N),
  GCC = new_list(10),
  GCC :: 0..10,
  global_cardinality(PNO,$[I-GCC[I+1]: I in 0..9]),
  sum([GCC[I] #> 0 : I in 1..N]) #= 3,
  check_pno(PNO,_Year,_Month,_Day,_BirthNo,_Checksum),
  fail, 
  nl.
go15 => true.


% Only prime digits
go16 ?=>
  N = 10,
  PNO = new_list(N),
  PNO :: [2,3,5,7],
  check_pno(PNO,_Year,_Month,_Day,_BirthNo,_Checksum),
  fail, 
  nl.
go16 => true.



%
% Calculate pno and print.
%
check_pno(PNO,Year,Month,Day,BirthNo,Checksum) =>
  pno(PNO,Year,Month,Day,BirthNo,Checksum),
  println(PNO).
  % println(map(to_string,PNO).join('')).
  % println([year=Year,month=Month,day=Day,birthNo=BirthNo,checkSum=Checksum]),
  % nl.
  

%
% Calculate the personal no and its parts.
% 
pno(PNO,Year,Month,Day,BirthNo,Checksum) => 
  N = 10,

  % decision variables
  PNO = new_list(N),
  PNO :: 0..9,

  Year :: 1..99,
  Year  #= 10*PNO[1] + PNO[2],
  Month :: 1..12,
  Month #= 10*PNO[3] + PNO[4],
  Day :: 1..31,
  Day   #= 10*PNO[5] + PNO[6],

  BirthNo :: 0..999,
  BirthNo #= 100*PNO[7] + 10*PNO[8] + PNO[9],

  % Array for the checksum (digital root)
  CA = new_list(9*2),
  CA :: 0..9,
  % The checksum
  Checksum :: 0..9,
  Checksum #= PNO[10],

  %
  % Rules for the date.
  %
  leap_year(Year,IsLeapYear),
  max_month_days(IsLeapYear,Month,MaxDays),
  Day #<= MaxDays,

  %
  % Checksum:
  % This is the magic:
  %  - for odd positions : multiply with 2
  %  - for even positions: multiply with 1
  %
  foreach(I in 1..N-1)
     I mod 2 #= 1 #=> PNO[I]*2 #= 10*CA[2*I-1] + CA[2*I],
     I mod 2 #= 0 #=> PNO[I]*1 #= 10*CA[2*I-1] + CA[2*I]
  end,
  Checksum #= 10 - (sum(CA) mod 10),

  Vars = PNO ++ CA ++ [Checksum],
  solve($[],Vars).

%
% Is Year a Leap year?
% See http://en.wikipedia.org/wiki/Leap_year
%
leap_year(Year, B) =>
  B :: 0..1,
  B #= 1 #<=> ((Year mod 4 #= 0 #/\ Year mod 100 #!= 0)
                #\/
               Year mod 400 #= 0).

%
% Max number of days of the month.
%
max_month_days(IsLeapYear, Month, MaxDays) =>
  % February
  (Month #= 2 #/\ IsLeapYear #= 1) #=> MaxDays #= 29,
  (Month #= 2 #/\ IsLeapYear #= 0) #=> MaxDays #= 28,

  % The rest
  Ds = [31,28,31,30,31,30,31,31,30,31,30,31],
  element(Month,Ds,MaxDays2),
  Month #!= 2 #=> MaxDays #= MaxDays2.
  
  %% Some variations on this:
  % table_in({Month,MaxDays},
  %         [
  %          {1,31},
  %          {3,31},
  %          {4,30},
  %          {5,31},
  %          {6,30},
  %          {7,31},
  %          {8,31},
  %          {9,30},
  %          {10,31},
  %          {11,30},
  %          {12,31}
  %         ]).
  %% or 
  % foreach(I in 1..12, I != 2)
  %   Month #= I #=> MaxDays #= Ds[I]
  % end.
  %% or 
  % (Month #= 4 #\/ Month #= 6 #\/ Month #= 9 #\/ Month #= 11) #= MaxDays #= 30,  
  % (Month #= 1 #\/ Month #= 3 #\/ Month #= 5 #\/ Month #= 7 #\/ Month #= 8 #\/
  %  Month #= 10 #\/ Month #= 12) #= MaxDays #= 31.