Lines Matching refs:Clauses
100 /// `Clauses` will be `[0, L1, L2, L2, L3, L4]`.
101 std::vector<Literal> Clauses;
103 /// Start indices of clauses of the formula in `Clauses`.
119 /// `Clauses`. This invariant is maintained when watched literals change.
142 Clauses.push_back(0);
160 const size_t S = Clauses.size();
162 Clauses.insert(Clauses.end(), lits.begin(), lits.end());
171 return C == ClauseStarts.size() - 1 ? Clauses.size() - ClauseStarts[C]
177 return llvm::ArrayRef<Literal>(&Clauses[ClauseStarts[C]], clauseSize(C));
672 while (isCurrentlyFalse(CNF.Clauses[NewWatchedLitIdx]))
674 const Literal NewWatchedLit = CNF.Clauses[NewWatchedLitIdx];
680 CNF.Clauses[NewWatchedLitIdx] = FalseLit;
681 CNF.Clauses[FalseLitWatcherStart] = NewWatchedLit;