/**
  *
  * Who killed agatha? (The Dreadsbury Mansion Murder Mystery) in Choco3.
  *
  * 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.
  *
  * This Choco3 model was created by Hakan Kjellerstrand (hakank@gmail.com)
  * Also, see http://www.hakank.org/choco3/ 
  *
  */
import org.kohsuke.args4j.Option;
import org.slf4j.LoggerFactory;
import samples.AbstractProblem;
import solver.ResolutionPolicy;
import solver.Solver;
import solver.constraints.Constraint;
import solver.constraints.IntConstraintFactory;
import solver.constraints.nary.cnf.Literal;
import solver.constraints.nary.cnf.Node;
import solver.constraints.nary.cnf.Node.*;
import solver.constraints.nary.cnf.ALogicTree;
import solver.search.limits.FailLimit;
import solver.search.strategy.IntStrategyFactory;
import solver.search.loop.monitors.SearchMonitorFactory;
import solver.variables.IntVar;
import solver.variables.BoolVar;
import solver.variables.VariableFactory;
import solver.search.strategy.strategy.AbstractStrategy;
import util.ESat;
import util.tools.ArrayUtils;

public class WhoKilledAgatha extends AbstractProblem {

  int n = 3;

  @Override
  public void buildModel() {

    IntVar the_killer = makeIntVar("the_killer", 0, n-1);

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

    // constants for nth
    // IntVar zero = makeIntVar("zero", 0, 0); 
    // IntVar one = makeIntVar("one", 1, 1); 

    IntVar[][] hates = VariableFactory.boolMatrix("hates", n, n, solver);
    IntVar[][] richer = VariableFactory.boolMatrix("hates", n, n, solver);

    //
    // 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: I cannot get nth to work here...
    for(int i = 0; i < n; i++) {
      /*
      m.addConstraint(implies(
                              eq(the_killer,i),
                              eq(hates[i][agatha], 1)
                              )
                      );
      */
      // This don't work!
      solver.post(IntConstraintFactory.implies(
                                               IntConstraintFactory.arithm(hates[i][agatha],"=",1),
                                               IntConstraintFactory.arithm(the_killer,"=", i)));

      m.addConstraint(implies(
                              eq(the_killer, i),
                              eq(richer[i][agatha], 0)
                              )
                      );

    }
        
        
    // define the concept of richer: 
    //   a) no one is richer than him-/herself
    for(int i = 0; i < n; i++) {
      solver.post(IntConstraintFactory.arithm(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
          m.addConstraint(
                          ifOnlyIf(
                                   eq(richer[i][j], 1),
                                   eq(richer[j][i], 0)
                                   )
                          );
        }
      }
    }
  
    // "Charles hates no one that Agatha hates." 
    for(int i = 0; i < n; i++) {
      // MiniZinc: hates[agatha, i] = 1 -> hates[charles, i] = 0
      m.addConstraint(
                      implies(
                              eq(hates[agatha][i], 1),
                              eq(hates[charles][i], 0)
                              )
                      );
    }
        
    // "Agatha hates everybody except the butler. "
    solver.post(eq(hates[agatha][charles], 1));
    solver.post(eq(hates[agatha][agatha], 1));
    solver.post(eq(hates[agatha][butler], 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
      m.addConstraint(
                      implies(
                              eq(richer[i][agatha], 0),
                              eq(hates[butler][i], 1)
                              )
                      );
    }
        
    // "The butler hates everyone whom Agatha hates." 
    for(int i = 0; i < n; i++) {
      // MiniZinc: hates[agatha, i] = 1 -> hates[butler, i] = 1
      m.addConstraint(
                      implies(
                              eq(hates[agatha][i], 1),
                              eq(hates[butler][i], 1)
                              )
                      );

    }

    // "No one hates everyone. "
    for(int i = 0; i < n; i++) {
      // MiniZinc: sum(j in r) (hates[i,j]) <= 2
      IntVar a[] = makeIntVarArray("a", n, 0,1);
      for (int j = 0; j < n; j++) {
        a[j] = hates[i][j];
      }
      m.addConstraint(leq(sum(a), 2));

    }
        
    // "Who killed Agatha?"
    // m.addConstraint(eq(the_victim, agatha));


  }

  @Override
  public void createSolver() {
    solver = new Solver("MineSweeper");
  }

  @Override
  public void configureSearch() {
    solver.set(IntStrategyFactory.firstFail_InDomainMin(ArrayUtils.flatten(mines)));
  }

  @Override
  public void solve() {
    // System.out.println(solver); // Solver/model before solve.
    solver.findSolution();
  }

  @Override
  public void prettyOut() {
        
    if(solver.isFeasible() == ESat.TRUE) {
            
      int num_solutions = 0;
      do {

        System.out.print("the_killer: " + the_killer.getValue() + " ");
        // System.out.print("the_victim: " + S.getVar(the_victim).getVal() + " ");
        /*
          System.out.println("\n" + "hates:" );
          for(int i = 0; i < n; i++) {
          for(int j = 0; j < n; j++) {
          System.out.print(S.getVar(hates[i][j]).getVal() + " ");
          }
          System.out.println();                
          }

          System.out.println("\n" + "richer:" );
          for(int i = 0; i < n; i++) {
          for(int j = 0; j < n; j++) {
          System.out.print(S.getVar(richer[i][j]).getVal() + " ");
          }
          System.out.println();                
          }
        */

        System.out.println();                
        num_solutions++;

      } while (solver.nextSolution() == Boolean.TRUE);

      System.out.println("Number of solutions: " + num_solutions);

    } else {

      System.out.println("Problem is not feasible.");

    }

  } // end model

  public static void main(String args[]) {
    new WhoKilledAgatha().execute(args);
        
  }

}