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