Lines Matching refs:Clauses
94 std::vector<Literal> Clauses; member
130 Clauses.push_back(0); in BooleanFormula()
152 const size_t S = Clauses.size(); in addClause()
155 Clauses.push_back(L1); in addClause()
157 Clauses.push_back(L2); in addClause()
159 Clauses.push_back(L3); in addClause()
168 return C == ClauseStarts.size() - 1 ? Clauses.size() - ClauseStarts[C] in clauseSize()
174 return llvm::ArrayRef<Literal>(&Clauses[ClauseStarts[C]], clauseSize(C)); in clauseLiterals()
595 while (isCurrentlyFalse(Formula.Clauses[NewWatchedLitIdx])) in updateWatchedLiterals()
597 const Literal NewWatchedLit = Formula.Clauses[NewWatchedLitIdx]; in updateWatchedLiterals()
603 Formula.Clauses[NewWatchedLitIdx] = FalseLit; in updateWatchedLiterals()
604 Formula.Clauses[FalseLitWatcherStart] = NewWatchedLit; in updateWatchedLiterals()