Lines Matching refs:Literal
124 Literal FirstLit = CNF.clauseLiterals(C).front(); in WatchedLiteralsSolverImpl()
282 const Literal FalseLit = VarAssignments[Var] == Assignment::AssignedTrue in updateWatchedLiterals()
296 const Literal NewWatchedLit = *NewWatchedLitIter; in updateWatchedLiterals()
321 bool watchedByUnitClause(Literal Lit) const { in watchedByUnitClause()
324 llvm::ArrayRef<Literal> Clause = CNF.clauseLiterals(LitWatcher); 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()