#include <gecode/driver.hh>

#include <algorithm>
#include <fstream>
#include <iterator>
#include <iostream>
#include <vector>

#include "ldsb.hh"
#include "siglex.hh"

#include "cputimer.hh"

using namespace Gecode;
using namespace std;

class PartitionGraph {
public:
    int n;
    vector<pair<int, bool> > p;
    vector<pair<int, int> > e;
    PartitionGraph(string filename) {
        ifstream i(filename.c_str());
        i >> n;
        int n_partitions;
        i >> n_partitions;
        for (int j = 0 ; j < n_partitions ; j++) {
            int k;
            bool c;
            i >> k >> c;
            p.push_back(pair<int,bool>(k,c));
        }
        int n_edges;
        i >> n_edges;
        for (int j = 0 ; j < n_edges ; j++) {
            int from, to;
            i >> from >> to;
            e.push_back(pair<int,int>(from, to));
        }
    }
    PartitionGraph() { }

    friend ostream& operator<< (ostream& o, const PartitionGraph& g);
};

// This has to go in namespace std because of C++'s lookup rules.
namespace std {
template <class T, class U>
ostream&
operator<< (ostream& o, const pair<T,U>& p) {
    o << "<" << p.first << "," << p.second << ">";
    return o;
}
}

ostream&
operator<< (ostream& o, const PartitionGraph& g) {
    o << g.n << "\n";
    copy(g.p.begin(), g.p.end(), ostream_iterator<pair<int,bool> >(o, " "));
    o << "\n";
    copy(g.e.begin(), g.e.end(), ostream_iterator<pair<int,int> >(o, " "));
    o << "\n";
    return o;
}

class GraphOptions : public Options {
private:
    int maxColours_;
public:
    PartitionGraph graph;
    GraphOptions(const char *s) : Options(s), maxColours_(-1) {}
    void parse(int& argc, char **argv) {
        Options::parse(argc, argv);
        graph = PartitionGraph(argv[1]);
        if (argc > 2)
            maxColours_ = atoi(argv[2]);
    }
    int maxColours() const { return maxColours_; }
};

int end(IntArgs p, int i, int n) {
    if (i == p.size()-1)
        return n;
    return p[i+1];
}

class GraphColouring : public MinimizeScript {
protected:
    IntVarArray x;
    IntVar m;

    int branchingChoice;
    IntArgs p;

    IntVarArray D, Y, FINP;
public:
    enum {
        SYMMETRY_NONE, 
        SYMMETRY_PRECEDE,
        SYMMETRY_SIGLEX,
        SYMMETRY_SIGLEXDEC,
        SYMMETRY_LDSB,
        SYMMETRY_NAIVE
    };

    enum {
        BRANCH_NONE,
        BRANCH_SIZE_MIN,
        BRANCH_SIZE_CON,
        BRANCH_SIZE_DEGREE_MIN
    };

    enum {
        MODEL_VARVAL,
        MODEL_VAL
    };

    // Sorts by provided array, in decreasing order.
    class DegreeComparator {
    protected:
        const int *degree;
    public:
        DegreeComparator(const int *d) : degree(d) { }
        bool operator() (int i, int j) { return degree[i] > degree[j]; }
    };

    GraphColouring(const GraphOptions& opt)
        : x(*this, opt.graph.n, 1, opt.graph.n),
          m(*this, 0, opt.graph.n) {
        // std::cerr << *(opt.graph);
        rel(*this, x, IRT_LQ, m);
        int n = opt.graph.n;

        branchingChoice = opt.branching();

        // std::cerr << opt.graph << "\n";

        p = IntArgs(opt.graph.p.size());
        int k = 0;
        int nodes = 0;
        int biggest_clique_start = -1;
        int biggest_clique_size = -1;
        for (vector<pair<int,bool> >::const_iterator i = opt.graph.p.begin() ;
             i != opt.graph.p.end() ; i++) {
            pair<int,bool> pa = *i;
            if (pa.second) {
                distinct(*this, x.slice(nodes, 1, pa.first), ICL_DOM);
                if (biggest_clique_start == -1 ||
                    pa.first > biggest_clique_size) {
                    biggest_clique_start = nodes;
                    biggest_clique_size = pa.first;
                }
            }
            p[k] = nodes;
            k++;
            nodes += pa.first;
        }

        for (vector<pair<int,int> >::const_iterator i = opt.graph.e.begin() ;
             i != opt.graph.e.end() ; i++) {
            pair<int,int> edge = *i;
            for (int j = p[edge.first] ; j != end(p,edge.first,n) ; j++)
                for (int k = p[edge.second] ; k != end(p,edge.second,n) ; k++)
                    rel(*this, x[j] != x[k]);
        }

        // Discard variable symmetries?
        if (opt.model() == MODEL_VAL) {
            p = IntArgs(n);
            for (int i = 0 ; i < n ; i++)
                p[i] = i;
        }
        
        if (opt.maxColours() != -1)
            rel(*this, m == opt.maxColours());

        if (opt.symmetry() == SYMMETRY_LDSB) {
            branch(*this, m, INT_VAL_MIN);
            branch(*this, &GraphColouring::post);
        } else {
            if (opt.symmetry() == SYMMETRY_PRECEDE) {
                int minval = 1;
                int maxval = opt.maxColours() == -1 ? x[0].max() : opt.maxColours();
                for (int i = minval ; i < maxval ; i++) {
                    //                    ValuePrecede::valuePrecede(*this,
                    //                    x, i, i+1);
                    precede(*this, x, i, i+1);
                }
                for (int i = 0 ; i < p.size() ; i++) {
                    for (int j = p[i] ; j != end(p,i,n)-1 ; j++)
                        rel(*this, x[j] <= x[j+1]);
                }
            } else if (opt.symmetry() == SYMMETRY_SIGLEX || opt.symmetry() == SYMMETRY_SIGLEXDEC) {
                int minval = 1;
                int maxval = opt.maxColours() == -1 ? x[0].max() : opt.maxColours();
                for (int i = minval ; i < maxval ; i++) {
                    // cerr << "siglex: " << i << " " << p << "\n";
                    // if (i == 4)
                    //     SigLex::siglex(*this, i, p, x, &D, &Y, &FINP);
                    // else
                    if (opt.symmetry() == SYMMETRY_SIGLEX)
                        SigLex::siglex(*this, i, p, x);
                    else if (opt.symmetry() == SYMMETRY_SIGLEXDEC)
                        SigLex::siglexdec(*this, i, p, x);
                    else
                        abort();
                }
            } else if (opt.symmetry() == SYMMETRY_NAIVE) {
                // Order the vertices in each partition.
                for (int i = 0 ; i < p.size() ; i++)
                    for (int j = p[i] ; j != end(p,i,n)-1 ; j++)
                        rel(*this, x[j] <= x[j+1]);
                // Label the biggest clique (if there is one).
                cerr << "clique: " << biggest_clique_start << " " << biggest_clique_size << "\n";
                if (biggest_clique_start != -1)
                    for (int i = 0 ; i < biggest_clique_size ; i++)
                        rel(*this, x[biggest_clique_start+i] == i+1);
            }
            branch(*this, m, INT_VAL_MIN);
            switch (branchingChoice) {
            case BRANCH_NONE: branch(*this, x, INT_VAR_NONE, INT_VAL_MIN); break;
            case BRANCH_SIZE_MIN: branch(*this, x, INT_VAR_SIZE_MIN, INT_VAL_MIN); break;
            case BRANCH_SIZE_DEGREE_MIN: branch(*this, x, INT_VAR_SIZE_DEGREE_MIN, INT_VAL_MIN); break;
            case BRANCH_SIZE_CON: branch(*this, x, tiebreak(INT_VAR_SIZE_MIN, INT_VAR_DEGREE_MAX), INT_VAL_MIN); break;
            default: abort();
            }
        }
    }
    static void post(Space& home) {
        static_cast<GraphColouring&>(home).more();
    }
    void more(void) {
        int n = x.size();
        // Make sure m is assigned, by propagating the space.
        (void) status();
        // Get value of m.
        int ncolours = m.val();
        // Construct symmetries and branch.
        Symmetries<IntView> s(p.size()+1);

        IntArgs a(ncolours);
        for (int i = 0 ; i < ncolours ; i++)
            a[i] = i+1;
        s[0] = ValueSymmetry<IntView>(*this, a);

        for (int i = 0 ; i < p.size() ; i++) {
            int ps = end(p,i,n) - p[i];
            IntArgs indices(ps);
            for (int j = 0 ; j < ps ; j++)
                indices[j] = p[i]+j;
            s[i+1] = VariableSymmetry<IntView>(*this, indices);
        }
        switch (branchingChoice) {
        case BRANCH_NONE: branch(*this, x, INT_VAR_NONE, INT_VAL_MIN, s); break;
        case BRANCH_SIZE_MIN: branch(*this, x, INT_VAR_SIZE_MIN, INT_VAL_MIN, s); break;
        case BRANCH_SIZE_DEGREE_MIN: branch(*this, x, INT_VAR_SIZE_DEGREE_MIN, INT_VAL_MIN, s); break;
        case BRANCH_SIZE_CON: branch(*this, x, tiebreak(INT_VAR_SIZE_MIN, INT_VAR_DEGREE_MAX), INT_VAL_MIN, s); break;
        default: abort();
        }
    }
    virtual Space* copy(bool share) {
        return new GraphColouring(share, *this);
    }
    GraphColouring(bool share, GraphColouring& e)
        : MinimizeScript(share, e),
          branchingChoice(e.branchingChoice), p(e.p) {
        x.update(*this, share, e.x);
        m.update(*this, share, e.m);

        D.update(*this, share, e.D);
        Y.update(*this, share, e.Y);
        FINP.update(*this, share, e.FINP);
        
    }
    IntVar cost(void) const {
        return m;
    }

    virtual void print(std::ostream& o) const {
        o << "colours: " << m << '\n';
        o << x << '\n';

        // o << D << '\n';
        // o << Y << '\n';
        // o << FINP << '\n';
    }
};

int
main(int argc, char **argv) {
    GraphOptions opt("graph colouring");
    opt.solutions(0);
    opt.symmetry(GraphColouring::SYMMETRY_NONE);
    opt.symmetry(GraphColouring::SYMMETRY_NONE, "none", "no symmetry breaking");
    opt.symmetry(GraphColouring::SYMMETRY_PRECEDE, "precede", "use value precedence constraints");
    opt.symmetry(GraphColouring::SYMMETRY_SIGLEX, "siglex", "use SigLex constraints");
    opt.symmetry(GraphColouring::SYMMETRY_SIGLEXDEC, "siglexdec", "use SigLex constraints with decreasing partition ordering");
    opt.symmetry(GraphColouring::SYMMETRY_LDSB, "ldsb", "use LDSB");
    opt.symmetry(GraphColouring::SYMMETRY_NAIVE, "naive", "use naive symmetry breaking");
    opt.branching(GraphColouring::BRANCH_SIZE_MIN);
    opt.branching(GraphColouring::BRANCH_NONE, "none", "naive branching");
    opt.branching(GraphColouring::BRANCH_SIZE_MIN, "size", "smallest domain size");
    opt.branching(GraphColouring::BRANCH_SIZE_CON, "sizecon", "smallest domain, break ties by constrainedness");
    opt.branching(GraphColouring::BRANCH_SIZE_DEGREE_MIN, "sizedegree", "smallest domain size divided by degree");
    opt.model(GraphColouring::MODEL_VARVAL);
    opt.model(GraphColouring::MODEL_VARVAL, "varval", "consider variable and value symmetries");
    opt.model(GraphColouring::MODEL_VAL, "val", "consider only value symmetries");
    opt.parse(argc, argv);
    // std::cerr << *(opt.graph);
    CPUTimer t;
    if (opt.maxColours() == -1)
        MinimizeScript::run<GraphColouring,BAB,GraphOptions>(opt);
    else
        MinimizeScript::run<GraphColouring,DFS,GraphOptions>(opt);
    cout << "\tCPUTimer: ";
    t.stop();
    cout << "\n";
}

