/**
  *
  * de Bruijn sequences in Choco v2
  *
  * 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 http://www.hakank.org/JaCoP/DeBruijn.java
  *
  * Choco model by Hakan Kjellerstrand (hakank@bonetmail.com)
  *
  *
  */
import static choco.Choco.*;
import choco.cp.model.CPModel;
import choco.cp.solver.CPSolver;
import choco.cp.solver.constraints.*;
import choco.cp.solver.*;
import choco.kernel.model.variables.integer.*;
import choco.kernel.*;
import choco.kernel.model.*;
import choco.kernel.model.variables.*;
import choco.kernel.model.constraints.*;
import choco.kernel.model.variables.set.*;
import choco.cp.solver.search.set.*;

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
    int num_solutions; // number of solutions to show, default all

    // The constraint variables
    Model model;
    CPSolver s;
    IntegerVariable[] x;        // the decimal numbers
    IntegerVariable[][] binary; // the representation of numbers in x, in the choosen base
    IntegerVariable[] bin_code; // the de Bruijn sequence (first number in binary)


   // integer power method
    static int pow( int x, int y) {
        int z = x; 
        for( int i = 1; i < y; i++ ) z *= x;
        return z;
    } // end pow


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

        model = new CPModel();

        base = in_base;
        n = in_n;
        int pow_base_n = 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;            
        }
        num_solutions = in_num_solutions;

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

        // decimal representation, ranges from 0..base^n-1
        x = makeIntVarArray("x", m, 0, pow_base_n-1, "cp:bound");

        
        //
        // 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 IntegerVariable[m][n];
        for(int i = 0; i < m; i++) {
            binary[i] = makeIntVarArray("binary" + i, n, 0, base-1, "cp:bound");
            model.addConstraint(eq(x[i], scalar(binary[i], weights)));
        }

        //
        // 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++) {
                model.addConstraint(eq(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++) {
            model.addConstraint(eq(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 IntegerVariable[m];
        for(int i = 0; i < m; i++) {
            bin_code[i] = makeIntVar("bin_code_" + i, 0, base-1, "cp:bound");
            model.addConstraint(eq(bin_code[i], binary[i][0]));
        }

        
        // All values in x should be different
        model.addConstraint(allDifferent(x));

        // Symmetry breaking: the minimum value in x should be the
        // first element.
        model.addConstraint(min(x, x[0]));


    } // end model


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

        s = new CPSolver();
        s.read(model);
        // s.solveAll();
        s.solve();

        // System.out.println(s.pretty());
        if (s.isFeasible()) {

            int num_sols = 0;
            // ChocoUtils.printAllSolutions(model, s);

            do {

                System.out.print("\ndecimal values: ");
                for (int i = 0; i < m; i++) {
                    System.out.print(s.getVar(x[i]).getVal() + " ");
                }

                System.out.print("\nde Bruijn sequence: ");
                for(int i = 0; i < m; i++) {
                    System.out.print(s.getVar(bin_code[i]).getVal() + " ");
                }


                System.out.println("\nbinary:");
                
                for(int i = 0; i < m; i++) {
                    for(int j = 0; j < n; j++) {
                        System.out.print(s.getVar(binary[i][j]).getVal() + " ");
                    }
                    System.out.println(" : " + s.getVar(x[i]).getVal());
                }


                System.out.println("");
                num_sols++;
                if (num_solutions > 0 && num_sols >= num_solutions) {
                    break;
                }

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

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

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

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

            System.out.println("nbSol: " + s.getNbSolutions());

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


    }

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

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

        if (args.length >= 4) {
            num_solutions = Integer.parseInt(args[3]);
        }

        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, num_solutions);
        debruijn.search();

    } // end main

} // end class