44   /// For a given clause, its watched literal is always its first literal in
123       // Designate the first literal as the "watched" literal of the clause.  in WatchedLiteralsSolverImpl()
124       Literal FirstLit = CNF.clauseLiterals(C).front();  in WatchedLiteralsSolverImpl()
280     // Update the watched literals of clauses that currently watch the literal  in updateWatchedLiterals()
282     const Literal FalseLit = VarAssignments[Var] == Assignment::AssignedTrue  in updateWatchedLiterals()
290       // Pick the first non-false literal as the new watched literal.  in updateWatchedLiterals()
296       const Literal NewWatchedLit = *NewWatchedLitIter;  in updateWatchedLiterals()
299       // Swap the old watched literal for the new one in `FalseLitWatcher` to  in updateWatchedLiterals()
300       // maintain the invariant that the watched literal is at the beginning of  in updateWatchedLiterals()
305       // If the new watched literal isn't watched by any other clause and its  in updateWatchedLiterals()
321   bool watchedByUnitClause(Literal Lit) const {  in watchedByUnitClause()
324       llvm::ArrayRef<Literal> Clause = CNF.clauseLiterals(LitWatcher);  in watchedByUnitClause()
326       // Assert the invariant that the watched literal is always the first one  in watchedByUnitClause()
340   bool isUnit(llvm::ArrayRef<Literal> Clause) const {  in isUnit()
342                         [this](Literal L) { return isCurrentlyFalse(L); });  in isUnit()
347   bool isCurrentlyFalse(Literal Lit) const {  in isCurrentlyFalse()
353   bool isWatched(Literal Lit) const { return WatchedHead[Lit] != NullClause; }  in isWatched()
363   llvm::DenseSet<Literal> watchedLiterals() const {  in watchedLiterals()
364     llvm::DenseSet<Literal> WatchedLiterals;  in watchedLiterals()
365     for (Literal Lit = 2; Lit < WatchedHead.size(); Lit++) {  in watchedLiterals()
382     const llvm::DenseSet<Literal> WatchedLiterals = watchedLiterals();  in activeVarsFormWatchedLiterals()
394     for (Literal Lit : watchedLiterals()) {  in unassignedVarsFormingWatchedLiteralsAreActive()