/**
  *
  *   Who killed agatha? (The Dreadsbury Mansion Murder Mystery) in Choco.

  *   This is a standard benchmark for theorem proving.  
  *   http://www.lsv.ens-cachan.fr/~goubault/H1.dist/H1.1/Doc/h1003.html
  *   """ 
  *   Someone in Dreadsbury Mansion killed Aunt Agatha. 
  *   Agatha, the butler, and Charles live in Dreadsbury Mansion, and 
  *   are the only ones to live there. A killer always hates, and is no 
  *   richer than his victim. Charles hates noone that Agatha hates. Agatha 
  *   hates everybody except the butler. The butler hates everyone not richer 
  *   than Aunt Agatha. The butler hates everyone whom Agatha hates. 
  *   Noone hates everyone. Who killed Agatha? 
  *   """
  
  *   Originally from 
  *   F. J. Pelletier: Seventy-five problems for testing automatic theorem provers. Journal of Automated Reasoning, 2: 191–216, 1986.
  
  *   Compare with the following models:
  *   - MiniZinc: http://www.hakank.org/minizinc/who_killed_agatha.mzn
  *   - Comet: http://www.hakank.org/comet/who_killed_agatha.mzn
  *   - Gecode: http://www.hakank.org/gecode/who_killed_agatha.cpp

  * 
  * This Choco model was created by Hakan Kjellerstrand (hakank@bonetmail.com)
  * Also, see my Choco page: http://www.hakank.org/choco/ 

  *
  * This JaCoP model was created by Hakan Kjellerstrand (hakank@bonetmail.com)
  * http://www.hakank.org/JaCoP/ .
  *
  *
  */

import JaCoP.constraints.*;
import JaCoP.core.*;
import JaCoP.search.*;

import java.io.*;
import java.util.*;
import java.text.*;

/*
  
  This version use Element by transposing the hates and richer matrices.

 */

public class WhoKilledAgatha_element {


    public void model() {

        int n = 3;
        Store store = new Store();

        IntVar the_killer = new IntVar(store, "the_killer", 0, n-1);
        //IntVar the_victim = new IntVar(store, "the_victim", 0, n-1);

        int agatha  = 0;
        int butler  = 1;
        int charles = 2;

        IntVar[][] hates = new IntVar[n][n];
        IntVar[][] richer = new IntVar[n][n];
        for(int i = 0; i < n; i++) {
            for(int j = 0; j < n; j++) {
                hates[i][j]  = new IntVar(store, "hates:" + i + "->" + j, 0, 1);
                richer[i][j] = new IntVar(store, "richer:" + i + "->" + j, 0, 1);
            }
        }

        IntVar one = new IntVar(store, "one", 1, 1);
        IntVar zero = new IntVar(store, "zero", 0, 0);

        ArrayList<IntVar> allVars; // used by the search 
        allVars = new ArrayList<IntVar>();

        //
        // The comments below contains the corresponding MiniZinc code,
        // for documentation and comparision.
        //
        
        // """
        // Agatha, the butler, and Charles live in Dreadsbury Mansion, and 
        // are the only ones to live there. 
        // """


        // "A killer always hates, and is no richer than his victim."
        // MiniZinc: hates[the_killer, the_victim] = 1
        //           richer[the_killer, the_victim] = 0
        //
        // Note: Element has default start index as 1, so we shift it to
        // start at 0.
        int shift = -1;
        for(int i = 0; i < n; i++) {
            store.impose(new Element(the_killer, hates[agatha], one, shift));
            store.impose(new Element(the_killer, richer[agatha], zero, shift));
        }
        
        
        // define the concept of richer: 
        //   a) no one is richer than him-/herself
        for(int i = 0; i < n; i++) {
            store.impose(new XeqC(richer[i][i], 0));
        }
        
        // (contd...) 
        //   b) if i is richer than j then j is not richer than i
        for(int i = 0; i < n; i++) {
            for(int j = 0; j < n; j++) {
                if (i != j) {
                    // MiniZinc: richer[i,j] == 1 <-> richer[j,i] == 0
                     store.impose(
                                  new Eq(
                                         new XeqC(richer[j][i], 1),
                                         new XeqC(richer[i][j], 0)
                                         )
                                  );

                }
            }
        }

       
        // "Agatha hates everybody except the butler. "
        store.impose(new XeqC(hates[charles][agatha], 1));
        store.impose(new XeqC(hates[agatha][agatha], 1));
        store.impose(new XeqC(hates[butler][agatha], 0));


        // "Charles hates no one that Agatha hates." 
        for(int i = 0; i < n; i++) {
            // MiniZinc: hates[agatha, i] = 1 -> hates[charles, i] = 0
            store.impose(
                         new IfThen(
                                    new XeqC(hates[i][agatha], 1),
                                    new XeqC(hates[i][charles], 0)
                                    )
                         );
        }

        
        // "The butler hates everyone not richer than Aunt Agatha. "
        for(int i = 0; i < n; i++) {
            // MiniZinc: richer[i, agatha] = 0 -> hates[butler, i] = 1
             store.impose(
                          new IfThen(
                                     new XeqC(richer[agatha][i], 0),
                                     new XeqC(hates[i][butler], 1)
                                     )
                          );
        }
        
        // "The butler hates everyone whom Agatha hates." 
        for(int i = 0; i < n; i++) {
            // MiniZinc: hates[agatha, i] = 1 -> hates[butler, i] = 1
             store.impose(
                             new IfThen(
                                        new XeqC(hates[i][agatha], 1),
                                        new XeqC(hates[i][butler], 1)
                                     )
                             );

        }

        allVars.add(the_killer);

        for(int i = 0; i < n; i++) {
            for(int j = 0; j < n; j++) {
                allVars.add(hates[j][i]);
            }
        }

        for(int i = 0; i < n; i++) {
            for(int j = 0; j < n; j++) {
                allVars.add(richer[j][i]);
            }
        }


        // "No one hates everyone. "
        for(int i = 0; i < n; i++) {
            // MiniZinc: sum(j in r) (hates[i,j]) <= 2
            IntVar a[] = new IntVar[n];
            for (int j = 0; j < n; j++) {
                a[j] = new IntVar(store, "a"+j, 0, 1);
                a[j] = hates[j][i];
            }
            IntVar a_sum = new IntVar(store, "a_sum"+i, 0, n);
            store.impose(new Sum(a, a_sum));
            store.impose(new XlteqC(a_sum, 2));
            allVars.add(a_sum);

        }
        

        // "Who killed Agatha?"
        // store.impose(eq(the_victim, agatha));


        SelectChoicePoint select = 
            new SimpleSelect (allVars.toArray(new IntVar[1]),
                              new SmallestDomain(),
                              new IndomainMin ()
                              );

        Search label = new DepthFirstSearch ();
        label.getSolutionListener().searchAll(true);
        label.getSolutionListener().recordSolutions(true);
        boolean result = label.labeling(store, select);

        //
        // output
        //
        if (result) {

            int numSolutions = label.getSolutionListener().solutionsNo();
            for(int s = 1; s <= numSolutions; s++) {
                Domain [] res = label.getSolutionListener().getSolution(s);
                int len = res.length;

                System.out.println("the_killer: " + res[0]);

                // print the result
                for(int i = 0; i < len; i++) {
                    System.out.print(res[i] + " ");
                }
                System.out.println();

            }

            System.out.println("Number of Solutions: " + numSolutions);

        }  else {

            System.out.println("No solution.");
            
        } 

    } // end model

    public static void main(String args[]) {
        WhoKilledAgatha_element t = new WhoKilledAgatha_element();
        t.model();
        
    } // end main

} // end class