58   /// (inclusive). The current level is stored in `Level`. At each level the
60   /// consistent partial assignment, `Level` will be incremented. Otherwise, if
62   /// `Level` until it reaches the most recent level where a decision was made.
63   size_t Level = 0;  member in clang::dataflow::__anond292cd9c0111::WatchedLiteralsSolverImpl
72   /// State of the solver at a particular level.
81   /// State of the solver at a particular level. It keeps track of previous
129     // Initialize the state at the root level to a decision so that in  in WatchedLiteralsSolverImpl()
130     // `reverseForcedMoves` we don't have to check that `Level >= 0` on each  in WatchedLiteralsSolverImpl()
177         // Backtrack and rewind the `Level` until the most recent non-forced  in solve()
181         // If the root level is reached, then all possible assignments lead to  in solve()
183         if (Level == 0)  in solve()
186         // Otherwise, take the other branch at the most recent level where a  in solve()
188         LevelStates[Level] = State::Forced;  in solve()
189         const Variable Var = LevelVars[Level];  in solve()
198         ++Level;  in solve()
200         LevelVars[Level] = ActiveVar;  in solve()
201         LevelStates[Level] = State::Forced;  in solve()
221         // for one of the active variables at the current level.  in solve()
222         ++Level;  in solve()
224         LevelVars[Level] = ActiveVar;  in solve()
225         LevelStates[Level] = State::Decision;  in solve()
261   /// Reverses forced moves until the most recent level where a decision was
264     for (; LevelStates[Level] == State::Forced; --Level) {  in reverseForcedMoves()
265       const Variable Var = LevelVars[Level];  in reverseForcedMoves()
278     const Variable Var = LevelVars[Level];  in updateWatchedLiterals()