622   bool watchedByUnitClause(Literal Lit) const {  in watchedByUnitClause()
623     for (ClauseID LitWatcher = Formula.WatchedHead[Lit];  in watchedByUnitClause()
633       assert(Clause.front() == Lit);  in watchedByUnitClause()
649   bool isCurrentlyFalse(Literal Lit) const {  in isCurrentlyFalse()
650     return static_cast<int8_t>(VarAssignments[var(Lit)]) ==  in isCurrentlyFalse()
651            static_cast<int8_t>(Lit & 1);  in isCurrentlyFalse()
655   bool isWatched(Literal Lit) const {  in isWatched()
656     return Formula.WatchedHead[Lit] != NullClause;  in isWatched()
669     for (Literal Lit = 2; Lit < Formula.WatchedHead.size(); Lit++) {  in watchedLiterals()  local
670       if (Formula.WatchedHead[Lit] == NullClause)  in watchedLiterals()
672       WatchedLiterals.insert(Lit);  in watchedLiterals()
698     for (Literal Lit : watchedLiterals()) {  in unassignedVarsFormingWatchedLiteralsAreActive()  local
699       const Variable Var = var(Lit);  in unassignedVarsFormingWatchedLiteralsAreActive()