% 
% Enigma problem 843 (How many are whole?) in MiniZinc.
% 
% Problem formulation from 
% http://magma.maths.usyd.edu.au/magma/Examples/node4.html
% """
% The problem `How many are whole?', by Susan Denham, was taken from 
% New Scientist No. 1998 (7 Oct 1995), in the Enigma problem section 
% on p. 63. 
%
% [...]
%
% The Problem:
% 
% In what follows, digits have been consistently replaced by letters, 
% with different letters being used for different digits:
% 
% In the list ONE TWO THREE FOUR just the first and one other are perfect squares.
% In the list ONE+1 TWO+1 THREE+1 FOUR+1 just one is a perfect square.
% In the list ONE+2 TWO+2 THREE+2 FOUR+2 just one is a perfect square.
% 
% If you want to win the prize send in your FORTUNE. 
% 
% ...
%
% The answer published a few weeks later was FORTUNE = 3701284. 
%
% """

% Note: In this model I have some problem using the following type of 
%       reifications:
%    square(ONE) /\ ( square(TWO) \/ square(THREE) \/ square(FOUR)) /\ ...
%  or
%    (square(ONE) /\ ( bool2int(square(TWO)) + bool2int(square(THREE)) + bool2int(square(FOUR)) = 1) /\ ...
%
% Hence the rather contrieved variant using a bool matrix here. It may have 
% to do with how I define the square predicate...
%

% 
% This MiniZinc model was created by Hakan Kjellerstrand, hakank@bonetmail.com
% See also my MiniZinc page: http://www.hakank.org/minizinc
%
include "globals.mzn"; 

int: n = 9;
set of int: Digits = 0..9;

var Digits: O :: is_output;
var Digits: N :: is_output;
var Digits: E :: is_output;
var Digits: T :: is_output;
var Digits: W :: is_output;
var Digits: H :: is_output;
var Digits: R :: is_output;
var Digits: F :: is_output;
var Digits: U :: is_output;

array[1..n] of var Digits: x = [O,N,E,T,W,H,R,F,U] :: is_output;

var 100..999:     ONE   :: is_output;
var 100..999:     TWO   :: is_output;
var 10000..99999: THREE :: is_output;
var 1000..9999:   FOUR  :: is_output;
var 1000000..9999999: FORTUNE :: is_output;

array[1..3,1..4] of var bool: bools :: is_output;

predicate square(var int: y) =
  let {
     var 1..ceil(sqrt(int2float(ub(y)))): z
  } in
  z*z = y
;

predicate toNum(array[int] of var 0..9: a, var int: n) =
          let { int: len = length(a) } in
          n = sum(i in 1..len) (
            ceil(pow(10.0, int2float(len-i))) * a[i]
          )
;

predicate cp1d(array[int] of var bool: x, array[int] of var bool: y) =
  assert(index_set(x) = index_set(y),
           "cp1d: x and y have different sizes",
     forall(i in index_set(x)) ( x[i] = y[i] ))
; 


% solve satisfy;
solve :: seq_search([
   bool_search([bools[i,j] | i in 1..3, j in 1..4], first_fail, indomain_min, complete),
   int_search(x ++ [ONE,TWO,THREE, FOUR, FORTUNE], first_fail, indomain_min, complete)
  ])
  satisfy;

constraint
  all_different(x) /\

  toNum([O,N,E], ONE)             /\
  toNum([T,W,O], TWO)             /\
  toNum([T,H,R,E,E], THREE)       /\
  toNum([F,O,U,R], FOUR)          /\
  toNum([F,O,R,T,U,N,E], FORTUNE) /\

  % In the list ONE TWO THREE FOUR just the first and one other are perfect squares.
  square(ONE) /\ 
  cp1d([bools[1,j] | j in 1..4], [square(ONE),square(TWO),square(THREE),square(FOUR)]) /\
  sum([bool2int(bools[1,j]) | j in 1..4]) = 2 /\

  % In the list ONE+1 TWO+1 THREE+1 FOUR+1 just one is a perfect square.   
  cp1d([bools[2,j] | j in 1..4], [square(ONE+1),square(TWO+1),square(THREE+1),square(FOUR+1)]) /\

  % In the list ONE+2 TWO+2 THREE+2 FOUR+2 just one is a perfect square.
  cp1d([bools[3,j] | j in 1..4], [square(ONE+2),square(TWO+2),square(THREE+2),square(FOUR+2)]) /\
  
  forall(i in 2..3) (
    sum([bool2int(bools[i,j]) | j in 1..4]) = 1
  )
;