定义 |
// Solver state: |
初始化 | , ok (true) |
使用 |
在以下函数中数据成员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_() model.clear(); 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 :
|
|
赋值改变的操作体现在几个化简函数体中。主要代码段如下: 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 }
|
|