void DistillerLongWithImpl::str_and_sub_using_watch(
    Clause& cl
    , const Lit lit
    , const bool alsoStrengthen
) {
    //Go through the watchlist
    watch_subarray thisW = solver->watches[lit];
    timeAvailable -= (long)thisW.size()*2 + 5;
    for(Watched* wit = thisW.begin(), *wend = thisW.end()
        ; wit != wend
        ; wit++
    ) {
        //Can't do anything with a clause
        if (wit->isClause())
            continue;

        timeAvailable -= 5;

        if (alsoStrengthen) {
            strengthen_clause_with_watch(lit, wit);
        }

        const bool subsumed = subsume_clause_with_watch(lit, wit, cl);
        if (subsumed)
            return;
    }
}

bool ClauseCleaner::satisfied(const Watched& watched, Lit lit)
{
    assert(watched.isBinary());
    if (solver.value(lit) == l_True) return true;
    if (solver.value(watched.getOtherLit()) == l_True) return true;
    return false;
}

bool CNF::redundant_or_removed(const Watched& ws) const
{
    if (ws.isBin() || ws.isTri()) {
        return ws.red();
    }

   assert(ws.isClause());
   const Clause* cl = cl_alloc.ptr(ws.get_offset());
   return cl->red() || cl->getRemoved();
}

bool CNF::redundant_or_removed(const Watched& ws) const
{
    if (ws.isBinary() || ws.isTri()) {
        return ws.red();
    }

   assert(ws.isClause());
   const Clause* cl = clAllocator.getPointer(ws.getOffset());
   return cl->red() || cl->getRemoved();
}

void PosixSelectorBase::TryConnecting()
{
	for (Watched *toconnect = m_connecting.First(), *next; toconnect; toconnect = next)
	{
		next = toconnect->Suc();
		TryConnecting(toconnect);

		// "next" element can be detached during
		// the "TryConnecting(toconnect)" call.
		// If it happened - restart the loop.
		if (next && !m_connecting.HasLink(next))
			next = m_connecting.First();
	}
}

void PosixSelectorBase::SetMode(List<Watched>& from, const PosixSelectListener* listener, int fd, Type mode)
{
	for (Watched *watched = from.First(); watched; watched = watched->Suc())
	{
		if (watched->m_listener == listener && (fd == -1 || fd == watched->m_fd))
		{
			if (watched->m_mode == mode)
				continue;

			Log(SPEW, "%010p: Adjusting %010p listener (file %d=%d) mode %d -> %d\n",
				this, listener, fd, watched->m_fd, (int)watched->m_mode, (int)mode);
			watched->m_mode = mode;
			OpStatus::Ignore(SetModeInternal(watched, mode));
		}
	}
}

ClOffset GateFinder::find_pair_for_and_gate_reduction(
    const Watched& ws
    , const size_t minSize
    , const size_t maxSize
    , const cl_abst_type general_abst
    , const OrGate& gate
    , const bool only_irred
) {
    //Only long clauses
    if (!ws.isClause())
        return CL_OFFSET_MAX;

    const ClOffset this_cl_offs = ws.get_offset();
    Clause& this_cl = *solver->cl_alloc.ptr(this_cl_offs);
    if ((ws.getAbst() | general_abst) != general_abst
        || (this_cl.red() && only_irred)
        || (!this_cl.red() && gate.red)
        || this_cl.size() > solver->conf.maxGateBasedClReduceSize
        || this_cl.size() > maxSize //Size must be smaller or equal to maxSize
        || this_cl.size() < minSize //Size must be larger or equal than minsize
        || sizeSortedOcc[this_cl.size()].empty()) //this bracket for sizeSortedOcc must be non-empty
    {
        //cout << "Not even possible, this clause cannot match any other" << endl;
        return CL_OFFSET_MAX;
    }

    if (!check_seen_and_gate_against_cl(this_cl, gate))
        return CL_OFFSET_MAX;


    const cl_abst_type this_cl_abst = calc_abst_and_set_seen(this_cl, gate);
    const ClOffset other_cl_offs = findAndGateOtherCl(
        sizeSortedOcc[this_cl.size()] //in this occur list that contains clauses of specific size
        , ~(gate.lit2) //this is the LIT that is meant to be in the clause
        , this_cl_abst //clause MUST match this abst
        , gate.red
        , only_irred
    );

    //Clear 'seen' from bits set
    *(simplifier->limit_to_decrease) -= this_cl.size();
    for (const Lit lit: this_cl) {
        seen[lit.toInt()] = 0;
    }

    return other_cl_offs;
}

void PosixSelectorBase::Detach(List<Watched>& from, const PosixSelectListener* listener, int fd)
{
	for (Watched *watched = from.First(), *next; watched; watched = next)
	{
		next = watched->Suc();
		if (watched->m_listener == listener && (fd == -1 || fd == watched->m_fd))
		{
			Log(VERBOSE, "%010p: Detach %010p listener (file %d=%d).\n",
				this, listener, fd, watched->m_fd);
			DetachInternal(watched);
			watched->SetWatched(false);

			/* Remove from list. If they are not referenced elsewhere (e.g. in
			 * the list of waiting poll events), it is deleted. */
			watched->Out();
			watched->Destroy();
		}
	}
}

size_t CNF::cl_size(const Watched& ws) const
{
    switch(ws.getType()) {
        case watch_binary_t:
            return 2;

        case CMSat::watch_tertiary_t:
            return 3;

        case watch_clause_t: {
            const Clause* cl = cl_alloc.ptr(ws.get_offset());
            return cl->size();
        }

        default:
            assert(false);
            return 0;
    }
}

bool PropEngine::propagate_binary_clause_occur(const Watched& ws)
{
    const lbool val = value(ws.lit2());
    if (val == l_False) {
        ok = false;
        return false;
    }

    if (val == l_Undef) {
        enqueue(ws.lit2());
        #ifdef STATS_NEEDED
        if (ws.red())
            propStats.propsBinRed++;
        else
            propStats.propsBinIrred++;
        #endif
    }

    return true;
}

size_t CNF::cl_size(const Watched& ws) const
{
    switch(ws.getType()) {
        case watch_binary_t:
            return 2;
            break;

        case CMSat::watch_tertiary_t:
            return 3;
            break;

        case watch_clause_t: {
            const Clause* cl = clAllocator.getPointer(ws.getOffset());
            return cl->size();
            break;
        }

        default:
            assert(false);
            return 0;
            break;
    }
}

bool CNF::redundant(const Watched& ws) const
{
    return (   (ws.isBin() && ws.red())
            || (ws.isTri()   && ws.red())
            || (ws.isClause()
                && cl_alloc.ptr(ws.get_offset())->red()
                )
    );
}

bool CNF::redundant(const Watched& ws) const
{
    return (   (ws.isBinary() && ws.red())
            || (ws.isTri()   && ws.red())
            || (ws.isClause()
                && clAllocator.getPointer(ws.getOffset())->red()
                )
    );
}

bool PropEngine::propagate_tri_clause_occur(const Watched& ws)
{
    const lbool val2 = value(ws.lit2());
    const lbool val3 = value(ws.lit3());
    if (val2 == l_True
        || val3 == l_True
    ) {
        return true;
    }

    if (val2 == l_Undef
        && val3 == l_Undef
    ) {
        return true;
    }

    if (val2 == l_False
        && val3 == l_False
    ) {
        ok = false;
        return false;
    }

    #ifdef STATS_NEEDED
    if (ws.red())
        propStats.propsTriRed++;
    else
        propStats.propsTriIrred++;
    #endif

    if (val2 == l_Undef) {
        enqueue(ws.lit2());
    } else {
        enqueue(ws.lit3());
    }
    return true;
}

bool GateFinder::find_pair_for_and_gate_reduction_tri(
    const Watched& ws
    , const OrGate& gate
    , const bool only_irred
    , Watched& found_pair
) {
    //Only long clauses
    if (!ws.isTri())
        return false;

    if (ws.red() && only_irred) {
        //cout << "Not even possible, this clause cannot match any other" << endl;
        return false;
    }

    //Check that we are not removing irred info based on learnt gate
    if (!ws.red() && gate.red)
        return false;

    if (!check_seen_and_gate_against_lit(ws.lit2(), gate)
        || !check_seen_and_gate_against_lit(ws.lit3(), gate))
    {
        return false;
    }

    seen[ws.lit2().toInt()] = 1;
    seen[ws.lit3().toInt()] = 1;
    const bool ret = findAndGateOtherCl_tri(
        solver->watches[~(gate.lit2)]
        , gate.red
        , only_irred
        , found_pair
    );

    seen[ws.lit2().toInt()] = 0;
    seen[ws.lit3().toInt()] = 0;

    return ret;
}

string CNF::watched_to_string(Lit otherLit, const Watched& ws) const
{
    std::stringstream ss;
    switch(ws.getType()) {
        case watch_binary_t:
            ss << otherLit << ", " << ws.lit2();
            if (ws.red()) {
                ss << "(red)";
            }
            break;

        case CMSat::watch_tertiary_t:
            ss << otherLit << ", " << ws.lit2() << ", " << ws.lit3();
            if (ws.red()) {
                ss << "(red)";
            }
            break;

        case watch_clause_t: {
            const Clause* cl = cl_alloc.ptr(ws.get_offset());
            for(size_t i = 0; i < cl->size(); i++) {
                ss << (*cl)[i];
                if (i + 1 < cl->size())
                    ss << ", ";
            }
            if (cl->red()) {
                ss << "(red)";
            }
            break;
        }

        default:
            assert(false);
            break;
    }

    return ss.str();
}

bool Distiller::distill_tri_irred_cls()
{
    if (solver->conf.verbosity >= 6) {
        cout
        << "c Doing distill for tri irred clauses"
        << endl;
    }

    //solver->watches.size()-1 would overflow
    if (solver->watches.size() == 0) {
        return solver->ok;
    }

    uint64_t origShorten = runStats.numClShorten;
    uint64_t origLitRem = runStats.numLitsRem;
    const double myTime = cpuTime();
    uint64_t maxNumProps =
        2LL*1000LL*solver->conf.distill_time_limitM
        *solver->conf.global_timeout_multiplier;
    uint64_t oldBogoProps = solver->propStats.bogoProps;
    size_t origTrailSize = solver->trail_size();

    //Randomize start in the watchlist
    size_t upI;
    upI = solver->mtrand.randInt(solver->watches.size()-1);
    size_t numDone = 0;
    for (; numDone < solver->watches.size()
        ; upI = (upI +1) % solver->watches.size(), numDone++

    ) {
        if (solver->propStats.bogoProps-oldBogoProps + extraTime > maxNumProps
            || solver->must_interrupt_asap()
        ) {
            break;
        }

        Lit lit = Lit::toLit(upI);
        for (size_t i = 0; i < solver->watches[upI].size(); i++) {
            if (solver->propStats.bogoProps-oldBogoProps + extraTime > maxNumProps) {
                break;
            }

            Watched ws = solver->watches[upI][i];

            //Only irred TRI and each TRI only once
            if (ws.isTri()
                && !ws.red()
                && lit < ws.lit2()
                && ws.lit2() < ws.lit3()
            ) {
                uselessLits.clear();
                lits.resize(3);
                lits[0] = lit;
                lits[1] = ws.lit2();
                lits[2] = ws.lit3();
                try_distill_clause_and_return_new(
                    CL_OFFSET_MAX
                    , ws.red()
                    , 2
                );

                //We could have modified the watchlist, better exit now
                break;
            }
        }

        if (!solver->okay()) {
            break;
        }
    }

    int64_t diff_bogoprops = (int64_t)solver->propStats.bogoProps-(int64_t)oldBogoProps;
    const bool time_out =  diff_bogoprops + extraTime > maxNumProps;
    const double time_used = cpuTime() - myTime;
    const double time_remain = 1.0 - float_div(diff_bogoprops + extraTime, maxNumProps);
    if (solver->conf.verbosity >= 3) {
        cout
        << "c [distill] tri irred"
        << " shorten: " << runStats.numClShorten - origShorten
        << " lit-rem: " << runStats.numLitsRem - origLitRem
        << " 0-depth ass: " << solver->trail_size() - origTrailSize
        << solver->conf.print_times(time_used, time_out, time_remain)
        << endl;
    }
    if (solver->sqlStats) {
        solver->sqlStats->time_passed(
            solver
            , "distill tri irred"
            , time_used
            , time_out
            , time_remain
        );
    }

    runStats.zeroDepthAssigns = solver->trail_size() - origTrailSize;

    return solver->ok;
}

void FeaturesCalc::for_one_clause(
    const Watched& cl
    , const Lit lit
    ,  Function func_each_cl
    ,  Function2 func_each_lit
) const {
    unsigned neg_vars = 0;
    unsigned pos_vars = 0;
    unsigned size = 0;

    switch (cl.getType()) {
        case CMSat::watch_binary_t: {
            if (cl.red()) {
                //only irred cls
                break;
            }
            if (lit > cl.lit2()) {
                //only count once
                break;
            }

            pos_vars += !lit.sign();
            pos_vars += !cl.lit2().sign();
            size = 2;
            neg_vars = size - pos_vars;
            func_each_cl(size, pos_vars, neg_vars);
            func_each_lit(lit, size, pos_vars, neg_vars);
            func_each_lit(cl.lit2(), size, pos_vars, neg_vars);
            break;
        }

        case CMSat::watch_tertiary_t: {
            if (cl.red()) {
                //only irred cls
                break;
            }
            if (lit > cl.lit2()) {
                //only count once
                break;
            }

            assert(cl.lit2() < cl.lit3());

            pos_vars += !lit.sign();
            pos_vars += !cl.lit2().sign();
            pos_vars += !cl.lit3().sign();
            size = 3;
            neg_vars = size - pos_vars;
            func_each_cl(size, pos_vars, neg_vars);
            func_each_lit(lit, size, pos_vars, neg_vars);
            func_each_lit(cl.lit2(), size, pos_vars, neg_vars);
            func_each_lit(cl.lit3(), size, pos_vars, neg_vars);
            break;
        }

        case CMSat::watch_clause_t: {
            const Clause& clause = *solver->cl_alloc.ptr(cl.get_offset());
            if (clause.red()) {
                //only irred cls
                break;
            }
            if (clause[0] < clause[1]) {
                //only count once
                break;
            }

            for (const Lit cl_lit : clause) {
                pos_vars += !cl_lit.sign();
            }
            size = clause.size();
            neg_vars = size - pos_vars;
            func_each_cl(size, pos_vars, neg_vars);
            for (const Lit cl_lit : clause) {
                func_each_lit(cl_lit, size, pos_vars, neg_vars);
            }
            break;
        }

        case CMSat::watch_idx_t: {
             // This should never be here
            assert(false);
            exit(-1);
            break;
        }
    }
}

void SubsumeImplicit::subsume_implicit(const bool check_stats)
{
    assert(solver->okay());
    const double myTime = cpuTime();
    const uint64_t orig_timeAvailable =
        1000LL*1000LL*solver->conf.subsume_implicit_time_limitM
        *solver->conf.global_timeout_multiplier;
    timeAvailable = orig_timeAvailable;
    const bool doStamp = solver->conf.doStamp;
    runStats.clear();

    //For randomization, we must have at least 1
    if (solver->watches.size() == 0) {
        return;
    }

    //Randomize starting point
    const size_t rnd_start = solver->mtrand.randInt(solver->watches.size()-1);
    size_t numDone = 0;
    for (;numDone < solver->watches.size() && timeAvailable > 0 && !solver->must_interrupt_asap()
         ;numDone++
    ) {
        const size_t at = (rnd_start + numDone)  % solver->watches.size();
        runStats.numWatchesLooked++;
        const Lit lit = Lit::toLit(at);
        watch_subarray ws = solver->watches[lit.toInt()];

        //We can't do much when there is nothing, or only one
        if (ws.size() < 2)
            continue;

        if (ws.size() > 1) {
            timeAvailable -= ws.size()*std::ceil(std::log((double)ws.size())) + 20;
            std::sort(ws.begin(), ws.end(), WatchSorterBinTriLong());
        }
        /*cout << "---> Before" << endl;
        print_watch_list(ws, lit);*/

        Watched* i = ws.begin();
        Watched* j = i;
        clear();

        for (Watched* end = ws.end(); i != end; i++) {
            if (timeAvailable < 0) {
                *j++ = *i;
                continue;
            }

            switch(i->getType()) {
                case CMSat::watch_clause_t:
                    *j++ = *i;
                    break;

                case CMSat::watch_tertiary_t:
                    try_subsume_tri(lit, i, j, doStamp);
                    break;

                case CMSat::watch_binary_t:
                    try_subsume_bin(lit, i, j);
                    break;

                default:
                    assert(false);
                    break;
            }
        }
        ws.shrink(i-j);
    }

    const double time_used = cpuTime() - myTime;
    const bool time_out = (timeAvailable <= 0);
    const double time_remain = float_div(timeAvailable, orig_timeAvailable);
    runStats.numCalled++;
    runStats.time_used += time_used;
    runStats.time_out += time_out;
    if (solver->conf.verbosity >= 1) {
        runStats.print_short(solver);
    }
    if (solver->sqlStats) {
        solver->sqlStats->time_passed(
            solver
            , "subsume implicit"
            , time_used
            , time_out
            , time_remain
        );
    }

    if (check_stats) {
        #ifdef DEBUG_IMPLICIT_STATS
        solver->check_stats();
        #endif
    }

    globalStats += runStats;
}

Lit HyperEngine::propagate_bfs(const uint64_t timeout)
{
    timedOutPropagateFull = false;
    propStats.otfHyperPropCalled++;
    #ifdef VERBOSE_DEBUG_FULLPROP
    cout << "Prop full BFS started" << endl;
    #endif

    PropBy confl;

    //Assert startup: only 1 enqueued, uselessBin is empty
    assert(uselessBin.empty());
    //assert(decisionLevel() == 1);

    //The toplevel decision has to be set specifically
    //If we came here as part of a backtrack to decision level 1, then
    //this is already set, and there is no need to set it
    if (trail.size() - trail_lim.back() == 1) {
        //Set up root node
        Lit root = trail[qhead];
        varData[root.var()].reason = PropBy(~lit_Undef, false, false, false);
    }

    uint32_t nlBinQHead = qhead;
    uint32_t lBinQHead = qhead;

    needToAddBinClause.clear();
    PropResult ret = PROP_NOTHING;
    start:

    //Early-abort if too much time was used (from prober)
    if (propStats.otfHyperTime + propStats.bogoProps > timeout) {
        timedOutPropagateFull = true;
        return lit_Undef;
    }

    //Propagate binary irred
    while (nlBinQHead < trail.size()) {
        const Lit p = trail[nlBinQHead++];
        watch_subarray_const ws = watches[~p];
        propStats.bogoProps += 1;
        for(const Watched *k = ws.begin(), *end = ws.end()
            ; k != end
            ; k++
        ) {

            //If something other than irred binary, skip
            if (!k->isBin() || k->red())
                continue;

            ret = prop_bin_with_ancestor_info(p, k, confl);
            if (ret == PROP_FAIL)
                return analyzeFail(confl);

        }
        propStats.bogoProps += ws.size()*4;
    }

    //Propagate binary redundant
    ret = PROP_NOTHING;
    while (lBinQHead < trail.size()) {
        const Lit p = trail[lBinQHead];
        watch_subarray_const ws = watches[~p];
        propStats.bogoProps += 1;
        size_t done = 0;

        for(const Watched *k = ws.begin(), *end = ws.end(); k != end; k++, done++) {

            //If something other than redundant binary, skip
            if (!k->isBin() || !k->red())
                continue;

            ret = prop_bin_with_ancestor_info(p, k, confl);
            if (ret == PROP_FAIL) {
                return analyzeFail(confl);
            } else if (ret == PROP_SOMETHING) {
                propStats.bogoProps += done*4;
                goto start;
            } else {
                assert(ret == PROP_NOTHING);
            }
        }
        lBinQHead++;
        propStats.bogoProps += done*4;
    }

    ret = PROP_NOTHING;
    while (qhead < trail.size()) {
        const Lit p = trail[qhead];
        watch_subarray ws = watches[~p];
        propStats.bogoProps += 1;

        Watched* i = ws.begin();
        Watched* j = ws.begin();
        Watched* end = ws.end();
        for(; i != end; i++) {
            if (i->isBin()) {
                *j++ = *i;
                continue;
            }
//.........这里部分代码省略.........