252   BooleanFormula Formula(NextVar - 1, std::move(Atomics));  in buildBooleanFormula()  local
258     Formula.addClause(posLit(GetVar(Val)));  in buildBooleanFormula()
282         Formula.addClause(negLit(Var), posLit(LeftSubVar));  in buildBooleanFormula()
283         Formula.addClause(posLit(Var), negLit(LeftSubVar));  in buildBooleanFormula()
291         Formula.addClause(negLit(Var), posLit(LeftSubVar));  in buildBooleanFormula()
292         Formula.addClause(negLit(Var), posLit(RightSubVar));  in buildBooleanFormula()
293         Formula.addClause(posLit(Var), negLit(LeftSubVar), negLit(RightSubVar));  in buildBooleanFormula()
307         Formula.addClause(negLit(Var), posLit(LeftSubVar));  in buildBooleanFormula()
308         Formula.addClause(posLit(Var), negLit(LeftSubVar));  in buildBooleanFormula()
316         Formula.addClause(negLit(Var), posLit(LeftSubVar), posLit(RightSubVar));  in buildBooleanFormula()
317         Formula.addClause(posLit(Var), negLit(LeftSubVar));  in buildBooleanFormula()
318         Formula.addClause(posLit(Var), negLit(RightSubVar));  in buildBooleanFormula()
330       Formula.addClause(negLit(Var), negLit(SubVar));  in buildBooleanFormula()
331       Formula.addClause(posLit(Var), posLit(SubVar));  in buildBooleanFormula()
343       Formula.addClause(posLit(Var), posLit(LeftSubVar));  in buildBooleanFormula()
344       Formula.addClause(posLit(Var), negLit(RightSubVar));  in buildBooleanFormula()
345       Formula.addClause(negLit(Var), negLit(LeftSubVar), posLit(RightSubVar));  in buildBooleanFormula()
358         Formula.addClause(posLit(Var));  in buildBooleanFormula()
366         Formula.addClause(posLit(Var), posLit(LeftSubVar), posLit(RightSubVar));  in buildBooleanFormula()
367         Formula.addClause(posLit(Var), negLit(LeftSubVar), negLit(RightSubVar));  in buildBooleanFormula()
368         Formula.addClause(negLit(Var), posLit(LeftSubVar), negLit(RightSubVar));  in buildBooleanFormula()
369         Formula.addClause(negLit(Var), negLit(LeftSubVar), posLit(RightSubVar));  in buildBooleanFormula()
378   return Formula;  in buildBooleanFormula()
384   BooleanFormula Formula;  member in clang::dataflow::WatchedLiteralsSolverImpl
437       : Formula(buildBooleanFormula(Vals)), LevelVars(Formula.LargestVar + 1),  in WatchedLiteralsSolverImpl()
438         LevelStates(Formula.LargestVar + 1) {  in WatchedLiteralsSolverImpl()
447     VarAssignments.resize(Formula.LargestVar + 1, Assignment::Unassigned);  in WatchedLiteralsSolverImpl()
450     for (Variable Var = Formula.LargestVar; Var != NullVar; --Var) {  in WatchedLiteralsSolverImpl()
551     for (auto &Atomic : Formula.Atomics) {  in buildSolution()
587     ClauseID FalseLitWatcher = Formula.WatchedHead[FalseLit];  in updateWatchedLiterals()
588     Formula.WatchedHead[FalseLit] = NullClause;  in updateWatchedLiterals()
590       const ClauseID NextFalseLitWatcher = Formula.NextWatched[FalseLitWatcher];  in updateWatchedLiterals()
593       const size_t FalseLitWatcherStart = Formula.ClauseStarts[FalseLitWatcher];  in updateWatchedLiterals()
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()
612       Formula.NextWatched[FalseLitWatcher] = Formula.WatchedHead[NewWatchedLit];  in updateWatchedLiterals()
613       Formula.WatchedHead[NewWatchedLit] = FalseLitWatcher;  in updateWatchedLiterals()
623     for (ClauseID LitWatcher = Formula.WatchedHead[Lit];  in watchedByUnitClause()
625          LitWatcher = Formula.NextWatched[LitWatcher]) {  in watchedByUnitClause()
626       llvm::ArrayRef<Literal> Clause = Formula.clauseLiterals(LitWatcher);  in watchedByUnitClause()
656     return Formula.WatchedHead[Lit] != NullClause;  in isWatched()
669     for (Literal Lit = 2; Lit < Formula.WatchedHead.size(); Lit++) {  in watchedLiterals()
670       if (Formula.WatchedHead[Lit] == NullClause)  in watchedLiterals()