138     for (Variable Var = CNF.largestVar(); Var != NullVar; --Var) {  in WatchedLiteralsSolverImpl()  local
139       if (isWatched(posLit(Var)) || isWatched(negLit(Var)))  in WatchedLiteralsSolverImpl()
140         ActiveVars.push_back(Var);  in WatchedLiteralsSolverImpl()
189         const Variable Var = LevelVars[Level];  in solve()  local
190         VarAssignments[Var] = VarAssignments[Var] == Assignment::AssignedTrue  in solve()
265       const Variable Var = LevelVars[Level];  in reverseForcedMoves()  local
267       VarAssignments[Var] = Assignment::Unassigned;  in reverseForcedMoves()
271       if (isWatched(posLit(Var)) || isWatched(negLit(Var)))  in reverseForcedMoves()
272         ActiveVars.push_back(Var);  in reverseForcedMoves()
278     const Variable Var = LevelVars[Level];  in updateWatchedLiterals()  local
282     const Literal FalseLit = VarAssignments[Var] == Assignment::AssignedTrue  in updateWatchedLiterals()
283                                  ? negLit(Var)  in updateWatchedLiterals()
284                                  : posLit(Var);  in updateWatchedLiterals()
356   Assignment decideAssignment(Variable Var) const {  in decideAssignment()
357     return !isWatched(posLit(Var)) || isWatched(negLit(Var))  in decideAssignment()
375     return llvm::all_of(ActiveVars, [this](Variable Var) {  in activeVarsAreUnassigned()  argument
376       return VarAssignments[Var] == Assignment::Unassigned;  in activeVarsAreUnassigned()
383     return llvm::all_of(ActiveVars, [&WatchedLiterals](Variable Var) {  in activeVarsFormWatchedLiterals()  argument
384       return WatchedLiterals.contains(posLit(Var)) ||  in activeVarsFormWatchedLiterals()
385              WatchedLiterals.contains(negLit(Var));  in activeVarsFormWatchedLiterals()
395       const Variable Var = var(Lit);  in unassignedVarsFormingWatchedLiteralsAreActive()  local
396       if (VarAssignments[Var] != Assignment::Unassigned)  in unassignedVarsFormingWatchedLiteralsAreActive()
398       if (ActiveVarsSet.contains(Var))  in unassignedVarsFormingWatchedLiteralsAreActive()