#ifndef _DECI_H_
#define _DECI_H_

#include "basis_pms.h"

using namespace std;

class Decimation
{
  public:
    Decimation(lit **ls_var_lit, int *ls_var_lit_count, lit **ls_clause_lit, long long *ls_org_clause_weight, long long ls_top_clause_weight);

    void make_space(int max_c, int max_v);
    void free_memory();
    void init(int *ls_local_opt, int *ls_global_opt, lit *ls_unit_clause, int ls_unit_clause_count, int *ls_clause_lit_count);
    void push_unit_clause_to_queue(lit tem_l);
    void assign(int v, int sense);
    void remove_unassigned_var(int v);
    void hunit_propagation();
    void sunit_propagation();
    void random_propagation();
    void unit_prosess();
    bool choose_sense(int v);

    vector<int> fix;

    int num_vars;
    int num_clauses;

    long long *h_true_score;
    long long *h_false_score;
    long long *hscore;
    long long *s_true_score;
    long long *s_false_score;
    long long *sscore;

    lit **clause_lit;
    lit **var_lit;
    int *var_lit_count;

    int *local_opt;
    int *global_opt;
    long long *org_clause_weight;
    long long top_clause_weight;

    lit *hunit_clause_queue;
    int *sense_in_hunit_clause_queue;
    int hunit_beg_pointer;
    int hunit_end_pointer;

    lit *sunit_clause_queue;
    int *sense_in_sunit_clause_queue;
    int sunit_beg_pointer;
    int sunit_end_pointer;

    int *unassigned_var;
    int *index_in_unassigned_var;
    int unassigned_var_count;

    int *clause_delete;
    int *clause_lit_count;
};

Decimation::Decimation(lit **ls_var_lit, int *ls_var_lit_count, lit **ls_clause_lit, long long *ls_org_clause_weight, long long ls_top_clause_weight)
{
    var_lit = ls_var_lit;
    var_lit_count = ls_var_lit_count;
    clause_lit = ls_clause_lit;
    org_clause_weight = ls_org_clause_weight;
    top_clause_weight = ls_top_clause_weight;
}

void Decimation::make_space(int max_c, int max_v)
{
    num_vars = max_v;
    num_clauses = max_c;

    max_c += 10;
    max_v += 10;

    h_true_score = new long long[max_v];
    h_false_score = new long long[max_v];
    hscore = new long long[max_v];
    s_true_score = new long long[max_v];
    s_false_score = new long long[max_v];
    sscore = new long long[max_v];

    fix.resize(max_v);
    fix.reserve(max_v);

    hunit_clause_queue = new lit[max_v];
    sense_in_hunit_clause_queue = new int[max_v];

    sunit_clause_queue = new lit[max_v];
    sense_in_sunit_clause_queue = new int[max_v];

    unassigned_var = new int[max_v];
    index_in_unassigned_var = new int[max_v];

    clause_delete = new int[max_c];
    clause_lit_count = new int[max_c];
}

void Decimation::free_memory()
{
    fix.clear();
    delete[] h_true_score;
    delete[] h_false_score;
    delete[] hscore;
    delete[] s_true_score;
    delete[] s_false_score;
    delete[] sscore;

    delete[] hunit_clause_queue;
    delete[] sense_in_hunit_clause_queue;

    delete[] sunit_clause_queue;
    delete[] sense_in_sunit_clause_queue;

    delete[] unassigned_var;
    delete[] index_in_unassigned_var;

    delete[] clause_delete;
    delete[] clause_lit_count;
}

void Decimation::init(int *ls_local_opt, int *ls_global_opt, lit *ls_unit_clause, int ls_unit_clause_count, int *ls_clause_lit_count)
{
    int v;
    int c;
    //parameters used in decimation
    hunit_beg_pointer = 0;
    hunit_end_pointer = 0;

    sunit_beg_pointer = 0;
    sunit_end_pointer = 0;

    unassigned_var_count = num_vars;

    //data structure of the instance
    local_opt = ls_local_opt;
    global_opt = ls_global_opt;

    for (int i = 0; i < num_vars; ++i)
    {
        v = i + 1;
        unassigned_var[i] = v;
        index_in_unassigned_var[v] = i;

        fix[v] = -1;
        sense_in_hunit_clause_queue[v] = -1; // not in hunit queue
        sense_in_sunit_clause_queue[v] = -1; // not in sunit queue
    }

    for (int i = 0; i < num_clauses; ++i)
    {
        clause_lit_count[i] = ls_clause_lit_count[i];
        clause_delete[i] = 0;
    }

    for (int i = 0; i < ls_unit_clause_count; ++i)
    {
        push_unit_clause_to_queue(ls_unit_clause[i]);
    }

    //figout score
    for (v = 1; v <= num_vars; ++v)
    {
        h_false_score[v] = 0;
        h_true_score[v] = 0;
        s_false_score[v] = 0;
        s_true_score[v] = 0;
        for (int i = 0; i < var_lit_count[v]; ++i)
        {
            c = var_lit[v][i].clause_num;
            if (org_clause_weight[c] == top_clause_weight)
            {
                if (var_lit[v][i].sense == 1)
                    ++h_true_score[v];
                else
                    ++h_false_score[v];
            }
            else
            {
                if (var_lit[v][i].sense == 1)
                    s_true_score[v] += org_clause_weight[c];
                else
                    s_false_score[v] += org_clause_weight[c];
            }
        }
        hscore[v] = max(h_false_score[v], h_true_score[v]);
        sscore[v] = max(s_false_score[v], s_true_score[v]);
    }
}

void Decimation::push_unit_clause_to_queue(lit tem_l)
{
    int v = tem_l.var_num;
    int c = tem_l.clause_num;
    if (org_clause_weight[c] == top_clause_weight)
    {
        if (sense_in_hunit_clause_queue[v] == -1)
        {
            sense_in_hunit_clause_queue[v] = tem_l.sense;
            hunit_clause_queue[hunit_end_pointer++] = tem_l;
        }
        else
        {
            if (sense_in_hunit_clause_queue[v] != tem_l.sense) //conflict var in hard unit queue
            {
                sense_in_hunit_clause_queue[v] = -2; //means this variable is conflict in hard unit queue
            }
        }
    }
    else
    {
        if (sense_in_hunit_clause_queue[v] != -1)
            return; //be defined by hard unit queue

        if (sense_in_sunit_clause_queue[v] == -1)
        {
            sense_in_sunit_clause_queue[v] = tem_l.sense;
            sunit_clause_queue[sunit_end_pointer++] = tem_l;
        }
        else
        {
            if (sense_in_sunit_clause_queue[v] != tem_l.sense) //conflict var in hard unit queue
            {
                sense_in_sunit_clause_queue[v] = -3; //means this variable is conflict in hard unit queue
            }
        }
    }
}

void Decimation::remove_unassigned_var(int v)
{
    int index = index_in_unassigned_var[v];
    int last_var = unassigned_var[--unassigned_var_count];
    unassigned_var[index] = last_var;
    index_in_unassigned_var[last_var] = index;
}

void Decimation::assign(int v, int sense)
{
    int c, l;
    lit tem_lit;
    fix[v] = sense;
    remove_unassigned_var(v);

    for (int i = 0; i < var_lit_count[v]; ++i)
    {
        c = var_lit[v][i].clause_num;
        if (clause_delete[c] == 1)
            continue;

        if (sense == var_lit[v][i].sense)
        {
            clause_delete[c] = 1;
            if (org_clause_weight[c] == top_clause_weight)
            {
                for (int j = 0; j < clause_lit_count[c]; j++)
                {
                    tem_lit = clause_lit[c][j];
                    if (tem_lit.sense == 1)
                    {
                        h_true_score[tem_lit.var_num]--;
                    }
                    else
                        h_false_score[tem_lit.var_num]--;
                    hscore[tem_lit.var_num] = max(h_true_score[tem_lit.var_num], h_false_score[tem_lit.var_num]);
                }
            }
            else
            {
                for (int j = 0; j < clause_lit_count[c]; j++)
                {
                    tem_lit = clause_lit[c][j];
                    if (tem_lit.sense == 1)
                    {
                        s_true_score[tem_lit.var_num] -= org_clause_weight[c];
                    }
                    else
                        s_false_score[tem_lit.var_num] -= org_clause_weight[c];
                    sscore[tem_lit.var_num] = max(s_true_score[tem_lit.var_num], s_false_score[tem_lit.var_num]);
                }
            }
            continue;
        }

        for (int j = 0; j < clause_lit_count[c]; j++)
        {
            if (clause_lit[c][j].var_num == v)
            {
                swap(clause_lit[c][j], clause_lit[c][--clause_lit_count[c]]);
                break;
            }
        }
        if (clause_lit_count[c] == 1)
        {
            push_unit_clause_to_queue(clause_lit[c][0]);
        }
    }
}

bool Decimation::choose_sense(int v)
{
    return rand() % 2;
}

void Decimation::hunit_propagation()
{
    int v, c, sense, rd;

    v = hunit_clause_queue[hunit_beg_pointer].var_num;
    sense = hunit_clause_queue[hunit_beg_pointer].sense;
    hunit_beg_pointer++;

    if (sense_in_hunit_clause_queue[v] == -2)
    {
        if (sscore[v] > 0)
        {
            if (sscore[v] == s_true_score[v])
                sense = 1;
            else
                sense = 0;
        }
        else
        {
            sense = choose_sense(v);
        }
    }
    assign(v, sense);
}

void Decimation::sunit_propagation()
{
    int v, c, sense, rd;

    int ht;
    ht = 15;

    int best_v = sunit_clause_queue[sunit_beg_pointer].var_num;
    int best_score = sscore[best_v];
    int index = sunit_beg_pointer;
    int count = sunit_end_pointer - sunit_beg_pointer;
    if (count > 15)
    {
        for (int i = 0; i < 15; ++i)
        {
            rd = rand() % count;

            v = sunit_clause_queue[sunit_beg_pointer + rd].var_num;
            if (sscore[v] > best_score)
            {
                best_v = v;
                index = sunit_beg_pointer + rd;
            }
        }
    }
    else
    {
        for (int i = sunit_beg_pointer; i < sunit_end_pointer; ++i)
        {
            v = sunit_clause_queue[i].var_num;
            if (sscore[v] > best_score)
            {
                best_v = v;
                index = i;
            }
        }
    }
    swap(sunit_clause_queue[sunit_beg_pointer], sunit_clause_queue[index]);
    v = sunit_clause_queue[sunit_beg_pointer].var_num;
    sense = sunit_clause_queue[sunit_beg_pointer].sense;
    sunit_beg_pointer++;

    if (fix[v] != -1)
        return;

    if (sense_in_sunit_clause_queue[v] == -3)
    {
        sense = choose_sense(v);
    }
    assign(v, sense);
}

void Decimation::random_propagation()
{
    int v, sense;
    v = unassigned_var[rand() % unassigned_var_count];
    sense = rand() % 2;
    assign(v, sense);
}

void Decimation::unit_prosess()
{

    while (unassigned_var_count > 0)
    {
        if (hunit_beg_pointer != hunit_end_pointer)
        {
            hunit_propagation();
        }
        else if (sunit_beg_pointer != sunit_end_pointer)
        {
            sunit_propagation();
        }
        else
        {
            random_propagation();
        }
    }
}

#endif