194   explicit CNFFormulaBuilder(CNFFormula &CNF)  in CNFFormulaBuilder()
195       : Formula(CNF) {}  in CNFFormulaBuilder()
299   CNFFormula CNF(NextVar - 1, std::move(Atomics));  in buildCNF()  local
301   CNFFormulaBuilder builder(CNF);  in buildCNF()
326       CNF.addClause(Val->literal() ? posLit(Var) : negLit(Var));  in buildCNF()
416       return CNF;  in buildCNF()
425   CNFFormula FinalCNF(NextVar - 1, std::move(CNF.Atomics));  in buildCNF()
429   for (ClauseID C = 1; C < CNF.ClauseStarts.size(); ++C) {  in buildCNF()
430     if (CNF.clauseSize(C) == 1) {  in buildCNF()
431       FinalBuilder.addClause(CNF.clauseLiterals(C)[0]);  in buildCNF()
436   for (ClauseID C = 1; C < CNF.ClauseStarts.size(); ++C) {  in buildCNF()
437     FinalBuilder.addClause(CNF.clauseLiterals(C));  in buildCNF()
450   CNFFormula CNF;  member in clang::dataflow::WatchedLiteralsSolverImpl
504       : CNF(buildCNF(Vals)), LevelVars(CNF.LargestVar + 1),  in WatchedLiteralsSolverImpl()
505         LevelStates(CNF.LargestVar + 1) {  in WatchedLiteralsSolverImpl()
514     VarAssignments.resize(CNF.LargestVar + 1, Assignment::Unassigned);  in WatchedLiteralsSolverImpl()
517     for (Variable Var = CNF.LargestVar; Var != NullVar; --Var) {  in WatchedLiteralsSolverImpl()
526     if (CNF.KnownContradictory) {  in solve()
628     for (auto &Atomic : CNF.Atomics) {  in buildSolution()
664     ClauseID FalseLitWatcher = CNF.WatchedHead[FalseLit];  in updateWatchedLiterals()
665     CNF.WatchedHead[FalseLit] = NullClause;  in updateWatchedLiterals()
667       const ClauseID NextFalseLitWatcher = CNF.NextWatched[FalseLitWatcher];  in updateWatchedLiterals()
670       const size_t FalseLitWatcherStart = CNF.ClauseStarts[FalseLitWatcher];  in updateWatchedLiterals()
672       while (isCurrentlyFalse(CNF.Clauses[NewWatchedLitIdx]))  in updateWatchedLiterals()
674       const Literal NewWatchedLit = CNF.Clauses[NewWatchedLitIdx];  in updateWatchedLiterals()
680       CNF.Clauses[NewWatchedLitIdx] = FalseLit;  in updateWatchedLiterals()
681       CNF.Clauses[FalseLitWatcherStart] = NewWatchedLit;  in updateWatchedLiterals()
689       CNF.NextWatched[FalseLitWatcher] = CNF.WatchedHead[NewWatchedLit];  in updateWatchedLiterals()
690       CNF.WatchedHead[NewWatchedLit] = FalseLitWatcher;  in updateWatchedLiterals()
700     for (ClauseID LitWatcher = CNF.WatchedHead[Lit]; LitWatcher != NullClause;  in watchedByUnitClause()
701          LitWatcher = CNF.NextWatched[LitWatcher]) {  in watchedByUnitClause()
702       llvm::ArrayRef<Literal> Clause = CNF.clauseLiterals(LitWatcher);  in watchedByUnitClause()
732     return CNF.WatchedHead[Lit] != NullClause;  in isWatched()
745     for (Literal Lit = 2; Lit < CNF.WatchedHead.size(); Lit++) {  in watchedLiterals()
746       if (CNF.WatchedHead[Lit] == NullClause)  in watchedLiterals()