Lines Matching full:clause

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.
196         // We found a unit clause! The value of its unassigned variable is
301       // the clause.
305       // If the new watched literal isn't watched by any other clause and its
314       // Go to the next clause that watches `FalseLit`.
320   /// clause.
324       llvm::ArrayRef<Literal> Clause = CNF.clauseLiterals(LitWatcher);
327       // in the clause.
331       assert(Clause.front() == Lit);
333       if (isUnit(Clause))
339   /// Returns true if and only if `Clause` is a unit clause.
340   bool isUnit(llvm::ArrayRef<Literal> Clause) const {
341     return llvm::all_of(Clause.drop_front(),
352   /// Returns true if and only if `Lit` is watched by a clause in `Formula`.