minisat数据成员ok的使用分析

Posted 2021-05-16 海阔凭鱼跃越

 

定义	// Solver state: // bool ok; // If FALSE, the constraints are already unsatisfiable. No part of the solver state may be used!
初始化	, 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_() {     // 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 }