#include "Solver.h"
#include "mtl/Sort.h"
using namespace Glucose;



// simplify All
//
CRef Solver::simplePropagate()
{
    CRef    confl = CRef_Undef;
    int     num_props = 0;
    watches.cleanAll();
    watchesBin.cleanAll();
    while (qhead < trail.size()){
        Lit            p = trail[qhead++];     // 'p' is enqueued fact to propagate.
        vec<Watcher>&  ws = watches[p];
        Watcher        *i, *j, *end;
        num_props++;

        // First, Propagate binary clauses
        vec<Watcher>&  wbin = watchesBin[p];

        for (int k = 0; k<wbin.size(); k++){

            Lit imp = wbin[k].blocker;

            if (value(imp) == l_False){
                return wbin[k].cref;
            }

            if (value(imp) == l_Undef){
                simpleUncheckEnqueue(imp, wbin[k].cref);
            }
        }
        for (i = j = (Watcher*)ws, end = i + ws.size(); i != end;){
            // Try to avoid inspecting the clause:
            Lit blocker = i->blocker;
            if (value(blocker) == l_True){
                *j++ = *i++; continue;
            }

            // Make sure the false literal is data[1]:
            CRef     cr = i->cref;
            Clause&  c = ca[cr];
            Lit      false_lit = ~p;
            if (c[0] == false_lit)
                c[0] = c[1], c[1] = false_lit;
            assert(c[1] == false_lit);
            //  i++;

            // If 0th watch is true, then clause is already satisfied.
            // However, 0th watch is not the blocker, make it blocker using a new watcher w
            // why not simply do i->blocker=first in this case?
            Lit     first = c[0];
            //  Watcher w     = Watcher(cr, first);
            if (first != blocker && value(first) == l_True){
                i->blocker = first;
                *j++ = *i++; continue;
            }

            // Look for new watch:
            if (incremental){ // ----------------- INCREMENTAL MODE
                int choosenPos = -1;
                for (int k = 2; k < c.size(); k++){
                    if (value(c[k]) != l_False){
                        if (decisionLevel()>assumptions.size()){
                            choosenPos = k;
                            break;
                        }
                        else{
                            choosenPos = k;

                            if (value(c[k]) == l_True || !isSelector(var(c[k]))) {
                                break;
                            }
                        }

                    }
                }
                if (choosenPos != -1){
                    // watcher i is abandonned using i++, because cr watches now ~c[k] instead of p
                    // the blocker is first in the watcher. However,
                    // the blocker in the corresponding watcher in ~first is not c[1]
                    Watcher w = Watcher(cr, first); i++;
                    c[1] = c[choosenPos]; c[choosenPos] = false_lit;
                    watches[~c[1]].push(w);
                    goto NextClause;
                }
            }
            else{  // ----------------- DEFAULT  MODE (NOT INCREMENTAL)
                for (int k = 2; k < c.size(); k++){

                    if (value(c[k]) != l_False){
                        // watcher i is abandonned using i++, because cr watches now ~c[k] instead of p
                        // the blocker is first in the watcher. However,
                        // the blocker in the corresponding watcher in ~first is not c[1]
                        Watcher w = Watcher(cr, first); i++;
                        c[1] = c[k]; c[k] = false_lit;
                        watches[~c[1]].push(w);
                        goto NextClause;
                    }
                }
            }

            // Did not find watch -- clause is unit under assignment:
            i->blocker = first;
            *j++ = *i++;
            if (value(first) == l_False){
                confl = cr;
                qhead = trail.size();
                // Copy the remaining watches:
                while (i < end)
                    *j++ = *i++;
            }
            else{
                simpleUncheckEnqueue(first, cr);
            }
            NextClause:;
        }
        ws.shrink(i - j);

        // unaryWatches "propagation"
        if(useUnaryWatched && confl == CRef_Undef) {
            confl = simplePropagateUnaryWatches(p);

        }
    }


    return confl;
}

CRef Solver::simplePropagateUnaryWatches(Lit p) {
    CRef confl = CRef_Undef;
    Watcher *i, *j, *end;
    vec <Watcher> &ws = unaryWatches[p];
    for(i = j = (Watcher *) ws, end = i + ws.size(); i != end;) {
        // Try to avoid inspecting the clause:
        Lit blocker = i->blocker;
        if(value(blocker) == l_True) {
            *j++ = *i++;
            continue;
        }

        // Make sure the false literal is data[1]:
        CRef cr = i->cref;
        Clause &c = ca[cr];
        assert(c.getOneWatched());
        Lit false_lit = ~p;
        assert(c[0] == false_lit); // this is unary watch... No other choice if "propagated"
        //if (c[0] == false_lit)
        //c[0] = c[1], c[1] = false_lit;
        //assert(c[1] == false_lit);
        i++;
        Watcher w = Watcher(cr, c[0]);
        for(int k = 1; k < c.size(); k++) {
            if(value(c[k]) != l_False) {
                c[0] = c[k];
                c[k] = false_lit;
                unaryWatches[~c[0]].push(w);
                goto NextClauseUnary;
            }
        }

        // Did not find watch -- clause is empty under assignment:
        *j++ = w;

        confl = cr;
        qhead = trail.size();
        // Copy the remaining watches:
        while(i < end)
            *j++ = *i++;

        NextClauseUnary:;
    }
    ws.shrink(i - j);

    return confl;
}


void Solver::simpleUncheckEnqueue(Lit p, CRef from){
    assert(value(p) == l_Undef);
    assigns[var(p)] = lbool(!sign(p)); // this makes a lbool object whose value is sign(p)
    vardata[var(p)].reason = from;
    trail.push_(p);
}

void Solver::cancelUntilTrailRecord()
{
    for (int c = trail.size() - 1; c >= trailRecord; c--)
    {
        Var x = var(trail[c]);
        assigns[x] = l_Undef;

    }
    qhead = trailRecord;
    trail.shrink(trail.size() - trailRecord);

}

void Solver::litsEnqueue(int cutP, Clause& c)
{
    for (int i = cutP; i < c.size(); i++)
    {
        simpleUncheckEnqueue(~c[i]);
    }
}

bool Solver::removed(CRef cr) {
    return ca[cr].mark() == 1;
}

void Solver::simpleAnalyze(CRef confl, vec<Lit>& out_learnt, vec<CRef>& reason_clause, bool True_confl)
{
    int pathC = 0;
    Lit p = lit_Undef;
    int index = trail.size() - 1;

    do{
        if (confl != CRef_Undef){
            reason_clause.push(confl);
            Clause& c = ca[confl];
            // Special case for binary clauses
            // The first one has to be SAT
            if (p != lit_Undef && c.size() == 2 && value(c[0]) == l_False) {

                assert(value(c[1]) == l_True);
                Lit tmp = c[0];
                c[0] = c[1], c[1] = tmp;
            }
            // if True_confl==true, then choose p begin with the 1th index of c;
            for (int j = (p == lit_Undef && True_confl == false) ? 0 : 1; j < c.size(); j++){
                Lit q = c[j];
                if (!seen[var(q)]){
                    seen[var(q)] = 1;
                    pathC++;
                }
            }
        }
        else if (confl == CRef_Undef){
            out_learnt.push(~p);
        }
        // if not break, while() will come to the index of trail blow 0, and fatal error occur;
        if (pathC == 0) break;
        // Select next clause to look at:
        while (!seen[var(trail[index--])]);
        // if the reason cr from the 0-level assigned var, we must break avoid move forth further;
        // but attention that maybe seen[x]=1 and never be clear. However makes no matter;
        if (trailRecord > index + 1) break;
        p = trail[index + 1];
        confl = reason(var(p));
        seen[var(p)] = 0;
        pathC--;

    } while (pathC >= 0);
}

void Solver::simplifyLearnt(Clause& c)
{
    stats[lcmtested]++;

    trailRecord = trail.size();// record the start pointer

    vec<Lit> falseLit;

    falseLit.clear();

    bool True_confl = false;
    int beforeSize, afterSize;
    beforeSize = c.size();
    int i, j;
    CRef confl;

    for (i = 0, j = 0; i < c.size(); i++){
        if (value(c[i]) == l_Undef){
            //printf("///@@@ uncheckedEnqueue:index = %d. l_Undef\n", i);
            simpleUncheckEnqueue(~c[i]);
            c[j++] = c[i];
            confl = simplePropagate();
            if (confl != CRef_Undef){
                break;
            }
        }
        else{
            if (value(c[i]) == l_True){
                //printf("///@@@ uncheckedEnqueue:index = %d. l_True\n", i);
                c[j++] = c[i];
                True_confl = true;
                confl = reason(var(c[i]));
                break;
            }
            else{
                falseLit.push(c[i]);
                //printf("///@@@ uncheckedEnqueue:index = %d. l_False\n", i);
            }
        }
    }
    c.shrink(c.size() - j);
    if (LCMUpdateLBD && c.lbd() > c.size()) c.setLBD(c.size());
    afterSize = c.size();

    if (confl != CRef_Undef || True_confl == true){
        simp_learnt_clause.clear();
        simp_reason_clause.clear();
        if (True_confl == true){
            simp_learnt_clause.push(c.last());
        }
        simpleAnalyze(confl, simp_learnt_clause, simp_reason_clause, True_confl);

        if (simp_learnt_clause.size() < c.size()){
            for (i = 0; i < simp_learnt_clause.size(); i++){
                c[i] = simp_learnt_clause[i];
            }
            c.shrink(c.size() - i);
            if (LCMUpdateLBD) {
                int nblevels = computeLBD(simp_learnt_clause);
                if (nblevels < c.lbd())
                    c.setLBD(nblevels);
            }
        }
    }

    cancelUntilTrailRecord();

}

bool Solver::simplifyAll()
{
    int nbGoodReduce = 0;
    int beforeSize, afterSize;
    int nbSize1 = 0, nbSize2 = 0;

    if (!ok || propagate() != CRef_Undef)
        return ok = false;

    removeSatisfied(clauses);

    int ci, cj, li, lj;
    bool sat, false_lit;
    unsigned int nblevels;
    vec<Lit> ori_c;

    if (0 && chanseokStrategy && permanentLearnts.size() > 0) {
        for (ci = 0, cj = 0; ci < permanentLearnts.size(); ci++){
            CRef cr = permanentLearnts[ci];
            Clause& c = ca[cr];

            if (!removed(cr)){
                sat = false_lit = false;
                for (int i = 0; i < c.size(); i++){
                    if (value(c[i]) == l_True){
                        sat = true;
                        break;
                    }
                    else if (value(c[i]) == l_False){
                        false_lit = true;
                    }
                }
                if (sat){
                    removeClause(cr);
                }
                else{
                    detachClause(cr, true);

                    if (false_lit){
                        for (li = lj = 0; li < c.size(); li++){
                            if (value(c[li]) != l_False){
                                c[lj++] = c[li];
                            }
                        }
                        c.shrink(li - lj);
                        if(certifiedUNSAT)
                            addToDrat(c, true);
                    }
                    ////
                    if (c.simplified() || c.lbd() > 3) {
                        attachClause(cr);
                        permanentLearntsReduced.push(cr); //[cj++] = permanentLearnts[ci];
                        // permanentLearnts[cj++] = permanentLearnts[ci];
                        continue;
                    }

                    beforeSize = c.size();
                    assert(c.size() > 1);
                    // simplify a learnt clause c
                    simplifyLearnt(c);
                    assert(c.size() > 0);
                    afterSize = c.size();

                    if (beforeSize > afterSize){
                        if (afterSize <= 3) {
                            nbGoodReduce++;
                            if (afterSize > 1) parallelExportClauseDuringSearch(c);
                            if (afterSize == 2){
                                nbSize2++;
                            }
                        }
                        if(certifiedOutput)
                            addToDrat(c, true);
                        stats[lcmreduced]++;
                    }

                    if (c.size() == 1){
                        nbSize1++;
                        // when unit clause occur, enqueue and propagate
                        uncheckedEnqueue(c[0]);
                        parallelExportUnaryClause(c[0]);
                        if (propagate() != CRef_Undef)
                        {
                            ok = false;
                            return false;
                        }
                        // delete the clause memory in logic
                        c.mark(1);
                        ca.free(cr);
                    }
                    else{
                        attachClause(cr);
                        permanentLearntsReduced.push(cr); //[cj++] = permanentLearnts[ci];
                        //permanentLearnts[cj++] = permanentLearnts[ci];
                        // TODO
                        /*nblevels = computeLBD(c);
                          if (nblevels < c.lbd()){
                          c.setLBD(nblevels);
                          }*/

                        c.setSimplified(true);
                    }
                }
            }
        }
        permanentLearnts.shrink(ci - cj);
    }

    if (!chanseokStrategy) {
        sort(learnts, reduceDB_lt(ca));

        for (ci = 0, cj = 0; ci < learnts.size(); ci++){
            CRef cr = learnts[ci];
            Clause& c = ca[cr];

            if (!removed(cr)){
                sat = false_lit = false;
                for (int i = 0; i < c.size(); i++){
                    if (value(c[i]) == l_True){
                        sat = true;
                        break;
                    }
                    else if (value(c[i]) == l_False){
                        false_lit = true;
                    }
                }
                if (sat){
                    removeClause(cr);
                }
                else{
                    detachClause(cr, true);

                    if (false_lit){
                        for (li = lj = 0; li < c.size(); li++){
                            if (value(c[li]) != l_False){
                                c[lj++] = c[li];
                            }
                        }
                        c.shrink(li - lj);
                        if(certifiedUNSAT)
                            addToDrat(c, true);
                    }
                    ////
                    if (ci < learnts.size() / 2 || c.simplified()) {
                        attachClause(cr);
                        learnts[cj++] = learnts[ci];
                        continue;
                    }

                    beforeSize = c.size();
                    assert(c.size() > 1);
                    // simplify a learnt clause c
                    simplifyLearnt(c);
                    assert(c.size() > 0);
                    afterSize = c.size();

                    if (beforeSize > afterSize){
                        if (afterSize <= 3) {
                            nbGoodReduce++;
                            if (afterSize > 1) parallelExportClauseDuringSearch(c);
                            if (afterSize == 2){
                                nbSize2++;
                            }
                        }
                        if(certifiedOutput)
                            addToDrat(c, true);
                        stats[lcmreduced]++;
                    }

                    if (c.size() == 1){
                        nbSize1++;
                        // when unit clause occur, enqueue and propagate
                        uncheckedEnqueue(c[0]);
                        parallelExportUnaryClause(c[0]);
                        if (propagate() != CRef_Undef)
                        {
                            ok = false;
                            return false;
                        }
                        // delete the clause memory in logic
                        c.mark(1);
                        ca.free(cr);
                    }
                    else{
                        attachClause(cr);
                        learnts[cj++] = learnts[ci];
                        // TODO
                        /*nblevels = computeLBD(c);
                          if (nblevels < c.lbd()){
                          c.setLBD(nblevels);
                          }*/

                        c.setSimplified(true);
                    }
                }
            }
        }
        learnts.shrink(ci - cj);
    }

    checkGarbage();

    return true;
}