| 定义 |
// 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 }
|
|
原文：https://www.cnblogs.com/yuweng1689/p/14773445.html