冲突层的特殊性——data.nHighestLevel的判断分支

1             ConflictData data = FindConflictLevel(confl);
2 
3             if (data.nHighestLevel == 0) return l_False;
4         
5             if (data.bOnlyOneLitFromHighest)
6             {
7                cancelUntil(data.nHighestLevel - 1);
8                continue;
9             }

 1 inline Solver::ConflictData Solver::FindConflictLevel(CRef cind)
 2 {
 3     ConflictData data;
 4     Clause& conflCls = ca[cind];
 5     data.nHighestLevel = level(var(conflCls[0]));
 6     if (data.nHighestLevel == decisionLevel() && level(var(conflCls[1])) == decisionLevel())
 7     {
 8         return data;
 9     }
10 
11     int highestId = 0;
12     data.bOnlyOneLitFromHighest = true;
13     // find the largest decision level in the clause
14     for (int nLitId = 1; nLitId < conflCls.size(); ++nLitId)
15     {
16         int nLevel = level(var(conflCls[nLitId]));
17         if (nLevel > data.nHighestLevel)
18         {
19             highestId = nLitId;
20             data.nHighestLevel = nLevel;
21             data.bOnlyOneLitFromHighest = true;
22         }
23         else if (nLevel == data.nHighestLevel && data.bOnlyOneLitFromHighest == true)
24         {
25             data.bOnlyOneLitFromHighest = false;
26         }
27     }
28 
29     if (highestId != 0)
30     {
31         std::swap(conflCls[0], conflCls[highestId]);
32         if (highestId > 1)
33         {
34             OccLists<Lit, vec<Watcher>, WatcherDeleted>& ws 
                   = conflCls.size() == 2 ? watches_bin : watches;
35             //ws.smudge(~conflCls[highestId]);
36             remove(ws[~conflCls[highestId]], Watcher(cind, conflCls[1]));
37             ws[~conflCls[0]].push(Watcher(cind, conflCls[1]));
38         }
39     }
40 
41     return data;
42 }