257   BooleanFormula Formula(NextVar - 1, std::move(Atomics));  in buildBooleanFormula()  local
263     Formula.addClause(posLit(GetVar(Val)));  in buildBooleanFormula()
287         Formula.addClause(negLit(Var), posLit(LeftSubVar));  in buildBooleanFormula()
288         Formula.addClause(posLit(Var), negLit(LeftSubVar));  in buildBooleanFormula()
296         Formula.addClause(negLit(Var), posLit(LeftSubVar));  in buildBooleanFormula()
297         Formula.addClause(negLit(Var), posLit(RightSubVar));  in buildBooleanFormula()
298         Formula.addClause(posLit(Var), negLit(LeftSubVar), negLit(RightSubVar));  in buildBooleanFormula()
312         Formula.addClause(negLit(Var), posLit(LeftSubVar));  in buildBooleanFormula()
313         Formula.addClause(posLit(Var), negLit(LeftSubVar));  in buildBooleanFormula()
321         Formula.addClause(negLit(Var), posLit(LeftSubVar), posLit(RightSubVar));  in buildBooleanFormula()
322         Formula.addClause(posLit(Var), negLit(LeftSubVar));  in buildBooleanFormula()
323         Formula.addClause(posLit(Var), negLit(RightSubVar));  in buildBooleanFormula()
335       Formula.addClause(negLit(Var), negLit(SubVar));  in buildBooleanFormula()
336       Formula.addClause(posLit(Var), posLit(SubVar));  in buildBooleanFormula()
348       Formula.addClause(posLit(Var), posLit(LeftSubVar));  in buildBooleanFormula()
349       Formula.addClause(posLit(Var), negLit(RightSubVar));  in buildBooleanFormula()
350       Formula.addClause(negLit(Var), negLit(LeftSubVar), posLit(RightSubVar));  in buildBooleanFormula()
363         Formula.addClause(posLit(Var));  in buildBooleanFormula()
371         Formula.addClause(posLit(Var), posLit(LeftSubVar), posLit(RightSubVar));  in buildBooleanFormula()
372         Formula.addClause(posLit(Var), negLit(LeftSubVar), negLit(RightSubVar));  in buildBooleanFormula()
373         Formula.addClause(negLit(Var), posLit(LeftSubVar), negLit(RightSubVar));  in buildBooleanFormula()
374         Formula.addClause(negLit(Var), negLit(LeftSubVar), posLit(RightSubVar));  in buildBooleanFormula()
383   return Formula;  in buildBooleanFormula()
389   BooleanFormula Formula;  member in clang::dataflow::WatchedLiteralsSolverImpl
442       : Formula(buildBooleanFormula(Vals)), LevelVars(Formula.LargestVar + 1),  in WatchedLiteralsSolverImpl()
443         LevelStates(Formula.LargestVar + 1) {  in WatchedLiteralsSolverImpl()
452     VarAssignments.resize(Formula.LargestVar + 1, Assignment::Unassigned);  in WatchedLiteralsSolverImpl()
455     for (Variable Var = Formula.LargestVar; Var != NullVar; --Var) {  in WatchedLiteralsSolverImpl()
556     for (auto &Atomic : Formula.Atomics) {  in buildSolution()
592     ClauseID FalseLitWatcher = Formula.WatchedHead[FalseLit];  in updateWatchedLiterals()
593     Formula.WatchedHead[FalseLit] = NullClause;  in updateWatchedLiterals()
595       const ClauseID NextFalseLitWatcher = Formula.NextWatched[FalseLitWatcher];  in updateWatchedLiterals()
598       const size_t FalseLitWatcherStart = Formula.ClauseStarts[FalseLitWatcher];  in updateWatchedLiterals()
600       while (isCurrentlyFalse(Formula.Clauses[NewWatchedLitIdx]))  in updateWatchedLiterals()
602       const Literal NewWatchedLit = Formula.Clauses[NewWatchedLitIdx];  in updateWatchedLiterals()
608       Formula.Clauses[NewWatchedLitIdx] = FalseLit;  in updateWatchedLiterals()
609       Formula.Clauses[FalseLitWatcherStart] = NewWatchedLit;  in updateWatchedLiterals()
617       Formula.NextWatched[FalseLitWatcher] = Formula.WatchedHead[NewWatchedLit];  in updateWatchedLiterals()
618       Formula.WatchedHead[NewWatchedLit] = FalseLitWatcher;  in updateWatchedLiterals()
628     for (ClauseID LitWatcher = Formula.WatchedHead[Lit];  in watchedByUnitClause()
630          LitWatcher = Formula.NextWatched[LitWatcher]) {  in watchedByUnitClause()
631       llvm::ArrayRef<Literal> Clause = Formula.clauseLiterals(LitWatcher);  in watchedByUnitClause()
661     return Formula.WatchedHead[Lit] != NullClause;  in isWatched()
674     for (Literal Lit = 2; Lit < Formula.WatchedHead.size(); Lit++) {  in watchedLiterals()
675       if (Formula.WatchedHead[Lit] == NullClause)  in watchedLiterals()