/**
 * 
 * Global constraint alldifferent_except_0 (decomposition) in Choco.
 *
 *
 * From Global Constraint Catalog
 * http://www.emn.fr/x-info/sdemasse/gccat/Calldifferent_except_0.html
 * """
 * Enforce all variables of the collection VARIABLES to take distinct values, 
 * except those variables that are assigned to 0.
 * """
 * 
 * JaCoP model 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.*;

public class AllDifferentExcept0_test {

    Store store;
    IntVar[] x;

    int n; // length of x


    //
    // decomposition of alldifferent except 0
    //
    public void allDifferentExcept0(Store m, IntVar[] v) {

        allDifferentExceptC(m, v, 0);

    } // end allDifferentExcept0


    //
    // slightly more general: alldifferent except c
    //
    public void allDifferentExceptC(Store m, IntVar[] v, int c) {
        int len = v.length;

        for(int i = 0; i < v.length; i++) {
            for(int j = i+1; j < v.length; j++) {
                // if v[i] > c && v[j] > c -> v[i] != v[j]
                m.impose(new IfThen(
                                           new And(
                                               new XneqC(v[i], c), 
                                               new XneqC(v[j], c)
                                               ), 
                                           new XneqY(v[i], v[j])
                                           )
                                );
            }
        }
        
    } // end allDifferentExceptC

    //
    // increasing
    //
    public void increasing(Store m, IntVar[] v) {
        for(int j = 1; j < v.length; j++) {
            m.impose(new XgteqY(v[j], v[j-1]));
        }
    } // end increasing

    //
    // Model
    //
    public void model() {

        store = new Store();

        n = 10; // length of array

        x = new IntVar[n];
        for(int i = 0; i < n; i++) {
            x[i] = new IntVar(store, "x_" + i, 0, n);
        }

        allDifferentExceptC(store, x, 0);
        increasing(store, x);


    } // end model


    //
    // Search and output
    // 
    public void search() {
        System.out.print("search....");

        SelectChoicePoint select = 
            new SimpleSelect (x,
                              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;

                // 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 search
        
    //
    // main
    //
    public static void main(String args[]) {

      AllDifferentExcept0_test m = new AllDifferentExcept0_test();
      m.model();
      m.search();

    } // end main

} // end class AllDifferentExcept0_test