41   /// Maps literals (indices of the vector) to clause identifiers (elements of
44   /// For a given clause, its watched literal is always its first literal in
48   /// Maps clause identifiers (elements of the vector) to identifiers of other
51   /// The element at index 0 stands for the identifier of the clause that
52   /// follows the null clause. It is set to 0 and isn't used. Identifiers of
123       // Designate the first literal as the "watched" literal of the clause.  in WatchedLiteralsSolverImpl()
196         // We found a unit clause! The value of its unassigned variable is  in solve()
301       // the clause.  in updateWatchedLiterals()
305       // If the new watched literal isn't watched by any other clause and its  in updateWatchedLiterals()
314       // Go to the next clause that watches `FalseLit`.  in updateWatchedLiterals()
320   /// clause.
324       llvm::ArrayRef<Literal> Clause = CNF.clauseLiterals(LitWatcher);  in watchedByUnitClause()  local
327       // in the clause.  in watchedByUnitClause()
331       assert(Clause.front() == Lit);  in watchedByUnitClause()
333       if (isUnit(Clause))  in watchedByUnitClause()
339   /// Returns true if and only if `Clause` is a unit clause.
340   bool isUnit(llvm::ArrayRef<Literal> Clause) const {  in isUnit()
341     return llvm::all_of(Clause.drop_front(),  in isUnit()
352   /// Returns true if and only if `Lit` is watched by a clause in `Formula`.