197       Variable Var = NextVar;  in buildBooleanFormula()  local
201       if (!SubValsToVar.try_emplace(Val, Var).second)  in buildBooleanFormula()
237         Atomics[Var] = cast<AtomicBoolValue>(Val);  in buildBooleanFormula()
268     const Variable Var = GetVar(Val);  in buildBooleanFormula()  local
270     if (ProcessedSubVals[Var])  in buildBooleanFormula()
272     ProcessedSubVals[Var] = true;  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()
450     for (Variable Var = Formula.LargestVar; Var != NullVar; --Var) {  in WatchedLiteralsSolverImpl()  local
451       if (isWatched(posLit(Var)) || isWatched(negLit(Var)))  in WatchedLiteralsSolverImpl()
452         ActiveVars.push_back(Var);  in WatchedLiteralsSolverImpl()
490         const Variable Var = LevelVars[Level];  in solve()  local
491         VarAssignments[Var] = VarAssignments[Var] == Assignment::AssignedTrue  in solve()
567       const Variable Var = LevelVars[Level];  in reverseForcedMoves()  local
569       VarAssignments[Var] = Assignment::Unassigned;  in reverseForcedMoves()
573       if (isWatched(posLit(Var)) || isWatched(negLit(Var)))  in reverseForcedMoves()
574         ActiveVars.push_back(Var);  in reverseForcedMoves()
580     const Variable Var = LevelVars[Level];  in updateWatchedLiterals()  local
584     const Literal FalseLit = VarAssignments[Var] == Assignment::AssignedTrue  in updateWatchedLiterals()
585                                  ? negLit(Var)  in updateWatchedLiterals()
586                                  : posLit(Var);  in updateWatchedLiterals()
660   Assignment decideAssignment(Variable Var) const {  in decideAssignment()
661     return !isWatched(posLit(Var)) || isWatched(negLit(Var))  in decideAssignment()
679     return llvm::all_of(ActiveVars, [this](Variable Var) {  in activeVarsAreUnassigned()  argument
680       return VarAssignments[Var] == Assignment::Unassigned;  in activeVarsAreUnassigned()
687     return llvm::all_of(ActiveVars, [&WatchedLiterals](Variable Var) {  in activeVarsFormWatchedLiterals()  argument
688       return WatchedLiterals.contains(posLit(Var)) ||  in activeVarsFormWatchedLiterals()
689              WatchedLiterals.contains(negLit(Var));  in activeVarsFormWatchedLiterals()
699       const Variable Var = var(Lit);  in unassignedVarsFormingWatchedLiteralsAreActive()  local
700       if (VarAssignments[Var] != Assignment::Unassigned)  in unassignedVarsFormingWatchedLiteralsAreActive()
702       if (ActiveVarsSet.contains(Var))  in unassignedVarsFormingWatchedLiteralsAreActive()