/***************************************************************************************[Solver.cc]
Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
Copyright (c) 2007-2009, Niklas Sorensson
Copyright (c) 2009-2012, Mate Soos

Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
associated documentation files (the "Software"), to deal in the Software without restriction,
including without limitation the rights to use, copy, modify, merge, publish, distribute,
sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:

The above copyright notice and this permission notice shall be included in all copies or
substantial portions of the Software.

THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
**************************************************************************************************/

#include "cmsat/ClauseVivifier.h"
#include "cmsat/ClauseCleaner.h"
#include "cmsat/time_mem.h"
#include <iomanip>

//#define ASSYM_DEBUG

using namespace CMSat;

ClauseVivifier::ClauseVivifier(Solver& _solver) :
    lastTimeWentUntil(0)
    , numCalls(0)
    , solver(_solver)
{}


/**
@brief Performs clause vivification (by Hamadi et al.)

This is the only thing that does not fit under the aegis of tryBoth(), since
it is not part of failed literal probing, really. However, it is here because
it seems to be a function that fits into the idology of failed literal probing.
Maybe I am off-course and it should be in another class, or a class of its own.
*/
bool ClauseVivifier::vivifyClauses()
{
    assert(solver.ok);
    #ifdef VERBOSE_DEBUG
    std::cout << "c clauseVivifier started" << std::endl;
    //solver.printAllClauses();
    #endif //VERBOSE_DEBUG


    solver.clauseCleaner->cleanClauses(solver.clauses, ClauseCleaner::clauses);
    numCalls++;

    if (solver.ok) {
        if (!vivifyClauses2(solver.clauses)) return false;
        if (!vivifyClauses2(solver.learnts)) return false;
    }

    bool failed;
    uint32_t effective = 0;
    uint32_t effectiveLit = 0;
    double myTime = cpuTime();
    uint64_t maxNumProps = 20*1000*1000;
    if (solver.clauses_literals + solver.learnts_literals < 500000)
        maxNumProps *=2;
    uint64_t extraDiff = 0;
    uint64_t oldProps = solver.propagations;
    bool needToFinish = false;
    uint32_t checkedClauses = 0;
    uint32_t potentialClauses = solver.clauses.size();
    if (lastTimeWentUntil + 500 > solver.clauses.size())
        lastTimeWentUntil = 0;
    uint32_t thisTimeWentUntil = 0;
    vec<Lit> lits;
    vec<Lit> unused;

    if (solver.clauses.size() < 1000000) {
        //if too many clauses, random order will do perfectly well
        std::sort(solver.clauses.getData(), solver.clauses.getDataEnd(), sortBySize());
    }

    uint32_t queueByBy = 2;
    if (numCalls > 8
        && (solver.clauses_literals + solver.learnts_literals < 4000000)
        && (solver.clauses.size() < 50000))
        queueByBy = 1;

    Clause **i, **j;
    i = j = solver.clauses.getData();
    for (Clause **end = solver.clauses.getDataEnd(); i != end; i++) {
        if (needToFinish || lastTimeWentUntil > 0) {
            if (!needToFinish) {
                lastTimeWentUntil--;
                thisTimeWentUntil++;
            }
            *j++ = *i;
            continue;
        }

        //if done enough, stop doing it
        if (solver.propagations-oldProps + extraDiff > maxNumProps) {
            //std::cout << "Need to finish -- ran out of prop" << std::endl;
            needToFinish = true;
        }

        //if bad performance, stop doing it
        /*if ((i-solver.clauses.getData() > 5000 && effectiveLit < 300)) {
            std::cout << "Need to finish -- not effective" << std::endl;
            needToFinish = true;
        }*/

        Clause& c = **i;
        extraDiff += c.size();
        checkedClauses++;
        thisTimeWentUntil++;

        assert(c.size() > 2);
        assert(!c.learnt());

        unused.clear();
        lits.clear();
        lits.growTo(c.size());
        memcpy(lits.getData(), c.getData(), c.size() * sizeof(Lit));

        failed = false;
        uint32_t done = 0;
        solver.newDecisionLevel();
        for (; done < lits.size();) {
            uint32_t i2 = 0;
            for (; (i2 < queueByBy) && ((done+i2) < lits.size()); i2++) {
                lbool val = solver.value(lits[done+i2]);
                if (val == l_Undef) {
                    solver.uncheckedEnqueueLight(~lits[done+i2]);
                } else if (val == l_False) {
                    unused.push(lits[done+i2]);
                }
            }
            done += i2;
            failed = (!solver.propagate<false>(false).isNULL());
            if (numCalls > 3 && failed) break;
        }
        solver.cancelUntilLight();
        assert(solver.ok);

        if (unused.size() > 0 || (failed && done < lits.size())) {
            effective++;
            uint32_t origSize = lits.size();
            #ifdef ASSYM_DEBUG
            std::cout << "Assym branch effective." << std::endl;
            std::cout << "-- Orig clause:"; c.plainPrint();
            #endif
            solver.detachClause(c);

            lits.shrink(lits.size() - done);
            for (uint32_t i2 = 0; i2 < unused.size(); i2++) {
                remove(lits, unused[i2]);
            }

            Clause *c2 = solver.addClauseInt(lits);
            #ifdef ASSYM_DEBUG
            std::cout << "-- Origsize:" << origSize << " newSize:" << (c2 == NULL ? 0 : c2->size()) << " toRemove:" << c.size() - done << " unused.size():" << unused.size() << std::endl;
            #endif
            extraDiff += 20;
            //TODO cheating here: we don't detect a NULL return that is in fact a 2-long clause
            effectiveLit += origSize - (c2 == NULL ? 0 : c2->size());
            solver.clauseAllocator.clauseFree(&c);

            if (c2 != NULL) {
                #ifdef ASSYM_DEBUG
                std::cout << "-- New clause:"; c2->plainPrint();
                #endif
                *j++ = c2;
            }

            if (!solver.ok) needToFinish = true;
        } else {
            *j++ = *i;
        }
    }
    solver.clauses.shrink(i-j);

    lastTimeWentUntil = thisTimeWentUntil;

    if (solver.conf.verbosity  >= 1) {
        std::cout << "c asymm "
        << " cl-useful: " << effective << "/" << checkedClauses << "/" << potentialClauses
        << " lits-rem:" << effectiveLit
        << " time: " << cpuTime() - myTime
        << std::endl;
    }

    return solver.ok;
}


bool ClauseVivifier::vivifyClauses2(vec<Clause*>& clauses)
{
    assert(solver.ok);

    vec<char> seen;
    seen.growTo(solver.nVars()*2, 0);
    vec<char> seen_subs;
    seen_subs.growTo(solver.nVars()*2, 0);

    uint32_t litsRem = 0;
    uint32_t clShrinked = 0;
    uint64_t countTime = 0;
    uint64_t maxCountTime = 800*1000*1000;
    maxCountTime *= 6;
    if (solver.clauses_literals + solver.learnts_literals < 500000)
        maxCountTime *= 2;
    uint32_t clTried = 0;
    vec<Lit> lits;
    bool needToFinish = false;
    double myTime = cpuTime();
    uint32_t subsumed_tri_num = 0;
    uint32_t subsumed_bin_num = 0;

    Clause** i = clauses.getData();
    Clause** j = i;
    for (Clause** end = clauses.getDataEnd(); i != end; i++) {
        if (needToFinish) {
            *j++ = *i;
            continue;
        }
        if (countTime > maxCountTime)
            needToFinish = true;

        Clause& cl = **i;
        countTime += cl.size()*2;
        clTried++;

        bool subsumed = false;
        const bool learnt = cl.learnt();
        for (uint32_t i2 = 0; i2 < cl.size(); i2++) {
            seen[cl[i2].toInt()] = 1; //for strengthening
            seen_subs[cl[i2].toInt()] = 1; //for subsumption
        }

        for (const Lit *l = cl.getData(), *end = cl.getDataEnd(); l != end; l++) {
            const Lit *l_other = l;
            l_other++;
            if (l_other != end)
                __builtin_prefetch(solver.watches[(~*l_other).toInt()].getData());

            const vec<Watched>& ws = solver.watches[(~*l).toInt()];
            countTime += ws.size()*2;
            for(vec<Watched>::const_iterator it = ws.getData(), end = ws.getDataEnd(); it != end; it++) {
                //Handle tri clause
                if (it->isTriClause() && cl.size() > 3)
                {
                    if (learnt //we cannot decide if TRI is learnt or not
                        && seen_subs[it->getOtherLit().toInt()]
                        && seen_subs[it->getOtherLit2().toInt()]
                    ) {
                        subsumed_tri_num++;
                        subsumed = true;
                    }

                    if (seen[l->toInt()]) { //we may have removed it already
                        //one way
                        if (seen[(it->getOtherLit2()).toInt()])
                            seen[(~it->getOtherLit()).toInt()] = 0;

                        //other way
                        if (seen[(it->getOtherLit()).toInt()])
                            seen[(~it->getOtherLit2()).toInt()] = 0;
                    }
                }

                //Handle Binary clause
                if (it->isBinary()) {
                    if (seen_subs[it->getOtherLit().toInt()])
                    {
                        if (!learnt && it->getLearnt())
                            makeNonLearntBin(*l, it->getOtherLit(), it->getLearnt());
                        subsumed_bin_num++;
                        subsumed = true;
                    }

                    if (seen[l->toInt()]) //we may have removed it already
                        seen[(~it->getOtherLit()).toInt()] = 0;

                }
            }

            if (seen[l->toInt()] == 0)
                continue;

            countTime += solver.transOTFCache[l->toInt()].lits.size();
            for (vector<Lit>::const_iterator it2 = solver.transOTFCache[l->toInt()].lits.begin()
                , end2 = solver.transOTFCache[l->toInt()].lits.end(); it2 != end2; it2++) {
                seen[(~(*it2)).toInt()] = 0;
            }
        }

        lits.clear();
        for (const Lit *it2 = cl.getData(), *end2 = cl.getDataEnd(); it2 != end2; it2++) {
            if (seen[it2->toInt()]) lits.push(*it2);
            else litsRem++;
            seen[it2->toInt()] = 0;
            seen_subs[it2->toInt()] = 0;
        }

        if (subsumed) {
            solver.removeClause(cl);
        } else if (lits.size() < cl.size()) {
            solver.detachClause(cl);
            clShrinked++;
            Clause* c2 = solver.addClauseInt(lits, cl.learnt(), cl.getGlue(), cl.getMiniSatAct());
            solver.clauseAllocator.clauseFree(&cl);

            if (c2 != NULL) *j++ = c2;
            if (!solver.ok) needToFinish = true;
        } else {
            *j++ = *i;
        }
    }

    clauses.shrink(i-j);

    if (solver.conf.verbosity >= 1) {
        std::cout << "c vivif2 -- "
        << " cl tried " << std::setw(8) << clTried
        << " cl rem " << std::setw(8) << (subsumed_bin_num + subsumed_tri_num)
        << " cl shrink " << std::setw(8) << clShrinked
        << " lits rem " << std::setw(10) << litsRem
        << " time: " << cpuTime() - myTime
        << std::endl;
    }

    return solver.ok;
}

void ClauseVivifier::makeNonLearntBin(const Lit lit1, const Lit lit2, const bool learnt)
{
    assert(learnt == true);
    findWatchedOfBin(solver.watches, lit1 ,lit2, learnt).setLearnt(false);
    findWatchedOfBin(solver.watches, lit2 ,lit1, learnt).setLearnt(false);
    solver.learnts_literals -= 2;
    solver.clauses_literals += 2;
}
