/**
  *
  * de Bruijn sequences in JaCoP
  *
  * both "normal" and "arbitrary" de Bruijn sequences.
  * 
  * This is a port from my MiniZinc model
  *    http://www.hakank.org/minizinc/debruijn_binary.mzn
  *
  * and is explained somewhat in the swedish blog post
  * "Constraint Programming: Minizinc, Gecode/flatzinc och ECLiPSe/minizinc"
  * http://www.hakank.org/webblogg/archives/001209.html
  *
  * Related programs:
  * - "Normal" de Bruijn sequences
  *  CGI program for calculating the sequences
  *  http://www.hakank.org/comb/debruijn.cgi
  *  http://www.hakank.org/comb/deBruijnApplet.html (as Java applet)
  *
  * 
  * - "Arbitrary" de Bruijn sequences
  *   Program "de Bruijn arbitrary sequences"
  *   http://www.hakank.org/comb/debruijn_arb.cgi
  *
  *   This (swedish) blog post explaines the program:
  *   "de Bruijn-sekvenser av godtycklig längd"
  *   http://www.hakank.org/webblogg/archives/001114.html
  *
  *
  * JaCoP Model by Hakan Kjellerstrand (hakank@bonetmail.com)
  * Also see 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 DeBruijn {

    //
    // Note: The names is the same as the MiniZinc model for
    // easy comparison.
    //

    // These parameters may be set by the user:
    //  - base 
    //  - n 
    //  - m
    int base;  // the base to use. Also known as k. 
    int n;     // number of bits representing the numbers 
    int m;     // length of the sequence, defaults to m = base^n

    // The constraint variables
    Store store;
    IntVar[] x;        // the decimal numbers
    IntVar[][] binary; // the representation of numbers in x, in the choosen base
    IntVar[] bin_code; // the de Bruijn sequence (first number in binary)


    //
    // the model
    //
    public void model(int in_base, int in_n, int in_m) {

        store = new Store();

        base = in_base;
        n = in_n;
        int pow_base_n = HakankUtil.pow(base,n); // base^n, the range of integers
        m = pow_base_n;
        if (in_m > 0) {
            if (in_m > m) {
                System.out.println("m must be <= base^n (" + m + ")");
                System.exit(1);
            }
            m = in_m;            
        }

        System.out.println("Using base: " + base + " n: " + n + " m: " + m);

        // decimal representation, ranges from 0..base^n-1
        x = new IntVar[m];
        for(int i = 0; i < m; i++) {
            x[i] = new IntVar(store, "x_" + i, 0, pow_base_n-1);
        }

        
        //
        // convert between decimal number in x[i] and "base-ary" numbers 
        // in binary[i][0..n-1].
        //
        // (This corresponds to the predicate toNum in the MiniZinc model)
        //

        // calculate the weights array
        int[] weights = new int[n];
        int w = 1;
        for(int i = 0; i < n; i++) {
            weights[n-i-1] = w;
            w *= base;            
        }

        // connect binary <-> x
        binary = new IntVar[m][n];
        for(int i = 0; i < m; i++) {
            for(int j = 0; j < n; j++) {
                binary[i][j] = new IntVar(store, "binary_" + i + "_" + j, 0, base-1);
            }
            store.impose(new SumWeight (binary[i], weights, x[i]));
        }

        //
        // assert the the deBruijn property:  element i in binary starts
        // with the end of element i-1
        //
        for(int i = 1; i < m; i++) {
            for(int j = 1; j < n; j++) {
                store.impose(new XeqY(binary[i-1][j], binary[i][j-1]));
            }
        }

        // ... "around the corner": last element is connected to the first
        for(int j = 1; j < n; j++) {
            store.impose(new XeqY(binary[m-1][j], binary[0][j-1]));
        }



        //
        // This is the de Bruijn sequence, i.e.
        // the first element of of each row in binary[i]
        //
        bin_code = new IntVar[m];
        for(int i = 0; i < m; i++) {
            bin_code[i] = new IntVar(store, "bin_code_" + i, 0, base-1);
            store.impose(new XeqY(bin_code[i], binary[i][0]));
        }

        
        // All values in x should be different
        store.impose(new Alldifferent(x));

        // Symmetry breaking: the minimum value in x should be the
        // first element.
        store.impose(new Min(x, x[0]));


    } // end model


    //
    // Search
    //
    public void search() {

        SelectChoicePoint select = 
            new SimpleSelect (bin_code,
                              new SmallestDomain(),
                              new IndomainMin ()
                              );


        Search label = new DepthFirstSearch ();
        label.getSolutionListener().searchAll(false);
        label.getSolutionListener().recordSolutions(true);

        /*
        // From ExamplesJaCoP/MagicSquares.java
        // Using Credit search:
        // This may give fast results. However, it may result in no
        // result at all.
        CreditCalculator credit = new CreditCalculator(m*m, 5000, 10);        
        if (label.getConsistencyListener() == null)
            label.setConsistencyListener(credit);
        else
            label.getConsistencyListener().setChildrenListeners(credit);
        
        label.setExitChildListener(credit);
        label.setTimeOutListener(credit);
        */

        // The actual search
        boolean result = label.labeling(store, select);
        
        int numSolutions = label.getSolutionListener().solutionsNo();
        System.out.println("numSolutions: " + numSolutions);

        if (result) {

            // prints then de Bruijn sequences
            System.out.print("de Bruijn sequence(s):");            
            HakankUtil.printAllSolutions(label);

            System.out.print("decimal values: ");
            for(int i = 0; i < m; i++) {
                System.out.print(x[i].value() + " ");
            }
            System.out.println();

            /*
            System.out.println("\nbinary:");

            for(int i = 0; i < m; i++) {
                for(int j = 0; j < n; j++) {
                    System.out.print(binary[i][j].value() + " ");
                }
                System.out.println(" : " + x[i].value());
            }
            */
            System.out.println("numSolutions: " + numSolutions);

        } else {
            System.out.println("No solutions.");
        }// end if result


    }

    //
    // Running the program
    //  * java DeBruijn base n
    //  * java DeBruijn base n m
    //
    public static void main(String args[]) {

        int base = 2;
        int n = 3;        
        int m = 0;

        if (args.length == 3) {
            m = Integer.parseInt(args[2]);
        }
        if (args.length >= 2) {
            base = Integer.parseInt(args[0]);
            n = Integer.parseInt(args[1]);
        }

        DeBruijn debruijn = new DeBruijn();
        debruijn.model(base, n, m);
        debruijn.search();

    } // end main

} // end class