solver - what do the "do_simp" and "turn_off_simp" mean in Minisat(simpSolver)?

Question

when I read the source code of Minisat, I come across the following code fragment

inline bool SimpSolver::solve (bool do_simp, bool turn_off_simp)  { budgetOff(); assumptions.clear(); return solve_(do_simp, turn_off_simp) == l_True; }

and above it's just a overload-version of solve function, but all the solve functions have the parameter "do_simp" and "turn_off_simp", and I look into the implementation of solve_ and could not figure out what do they mean.

lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp)
{
    vec<Var> extra_frozen;
    lbool    result = l_True;

    do_simp &= use_simplification;

    if (do_simp){
        // Assumptions must be temporarily frozen to run variable elimination:
        for (int i = 0; i < assumptions.size(); i++){
            Var v = var(assumptions[i]);

            // If an assumption has been eliminated, remember it.
            assert(!isEliminated(v));

            if (!frozen[v]){
                // Freeze and store.
                setFrozen(v, true);
                extra_frozen.push(v);
            } }

        result = lbool(eliminate(turn_off_simp));
    }

    if (result == l_True)
        result = Solver::solve_();
    else if (verbosity >= 1)
        printf("===============================================================================
");

    if (result == l_True && extend_model)
        extendModel();

    if (do_simp)
        // Unfreeze the assumptions that were frozen:
        for (int i = 0; i < extra_frozen.size(); i++)
            setFrozen(extra_frozen[i], false);

    return result;
}

Could you intuitively explain them a little for me?

question from:https://stackoverflow.com/questions/65838202/what-do-the-do-simp-and-turn-off-simp-mean-in-minisatsimpsolver

Answer 1

Waitting for answers