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 与恶龙缠斗过久,自身亦成为恶龙;凝视深渊过久,深渊将回以凝视…