319   /// Returns true if and only if one of the clauses that watch `Lit` is a unit
321   bool watchedByUnitClause(Literal Lit) const {  in watchedByUnitClause()
322     for (ClauseID LitWatcher = WatchedHead[Lit]; LitWatcher != NullClause;  in watchedByUnitClause()
331       assert(Clause.front() == Lit);  in watchedByUnitClause()
345   /// Returns true if and only if `Lit` evaluates to `false` in the current
347   bool isCurrentlyFalse(Literal Lit) const {  in isCurrentlyFalse()
348     return static_cast<int8_t>(VarAssignments[var(Lit)]) ==  in isCurrentlyFalse()
349            static_cast<int8_t>(Lit & 1);  in isCurrentlyFalse()
352   /// Returns true if and only if `Lit` is watched by a clause in `Formula`.
353   bool isWatched(Literal Lit) const { return WatchedHead[Lit] != NullClause; }  in isWatched()
365     for (Literal Lit = 2; Lit < WatchedHead.size(); Lit++) {  in watchedLiterals()  local
366       if (WatchedHead[Lit] == NullClause)  in watchedLiterals()
368       WatchedLiterals.insert(Lit);  in watchedLiterals()
394     for (Literal Lit : watchedLiterals()) {  in unassignedVarsFormingWatchedLiteralsAreActive()  local
395       const Variable Var = var(Lit);  in unassignedVarsFormingWatchedLiteralsAreActive()