minisat数据成员ok的使用分析

// Solver state:
//
bool ok; // If FALSE, the constraints are already unsatisfiable. No part of the solver state may be used!

在以下函数中数据成员ok被使用

bool Solver::simplifyLearnt_x(vec<CRef>& learnts_x)；

bool Solver::simplifyLearnt_core()；

bool Solver::simplifyLearnt_tier2()；

bool Solver::simplifyAll()；

bool Solver::addClause_(vec<Lit>& ps);

bool Solver::simplify();

lbool Solver::search(int& nof_conflicts){assert(ok);......}

lbool Solver::solve_()
{
    // signal(SIGALRM, SIGALRM_switch);
    // alarm(2500);

    model.clear();
    conflict.clear();
    if (!ok) return l_False;

    solves++;

     ......

}

void Solver::toDimacs(FILE* f, const vec<Lit>& assumps);

集中使用在：

bool Solver::simplifyAll()
{
    ////
    simplified_length_record = original_length_record = 0;

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

    //// cleanLearnts(also can delete these code), here just for analyzing
    //if (local_learnts_dirty) cleanLearnts(learnts_local, LOCAL);
    //if (tier2_learnts_dirty) cleanLearnts(learnts_tier2, TIER2);
    //local_learnts_dirty = tier2_learnts_dirty = false;

    if (!simplifyLearnt_core()) return ok = false;
    if (!simplifyLearnt_tier2()) return ok = false;
    //if (!simplifyLearnt_x(learnts_local)) return ok = false;

    checkGarbage();

    ////
    //  printf("c size_reduce_ratio     : %4.2f%%\n",
    //         original_length_record == 0 ? 0 : 
    //(original_length_record - simplified_length_record) * 100 / (double)original_length_record);

    return true;
}

 赋值改变的操作体现在几个化简函数体中。主要代码段如下：

 1 if (c.size() == 1){
 2                     // when unit clause occur, enqueue and propagate
 3                     uncheckedEnqueue(c[0]);
 4                     if (propagate() != CRef_Undef){
 5                         ok = false;
 6                         return false;
 7                     }
 8                     // delete the clause memory in logic
 9                     c.mark(1);
10                     ca.free(cr);
11 //#ifdef BIN_DRUP
12 //                    binDRUP('d', c, drup_file);
13 //#else
14 //                    fprintf(drup_file, "d ");
15 //                    for (int i = 0; i < c.size(); i++)
16 //                        fprintf(drup_file, "%i ", (var(c[i]) + 1) * (-2 * sign(c[i]) + 1));
17 //                    fprintf(drup_file, "0\n");
18 //#endif
19                 }
20 。。。。。。。
21 }