278       Variable Var = NextVar;  in buildCNF()  local
282       if (!SubValsToVar.try_emplace(Val, Var).second)  in buildCNF()
289         Atomics[Var] = Val->getAtom();  in buildCNF()
316     const Variable Var = GetVar(Val);  in buildCNF()  local
318     if (ProcessedSubVals[Var])  in buildCNF()
320     ProcessedSubVals[Var] = true;  in buildCNF()
326       CNF.addClause(Val->literal() ? posLit(Var) : negLit(Var));  in buildCNF()
336         builder.addClause({negLit(Var), posLit(LHS)});  in buildCNF()
337         builder.addClause({posLit(Var), negLit(LHS)});  in buildCNF()
342         builder.addClause({negLit(Var), posLit(LHS)});  in buildCNF()
343         builder.addClause({negLit(Var), posLit(RHS)});  in buildCNF()
344         builder.addClause({posLit(Var), negLit(LHS), negLit(RHS)});  in buildCNF()
356         builder.addClause({negLit(Var), posLit(LHS)});  in buildCNF()
357         builder.addClause({posLit(Var), negLit(LHS)});  in buildCNF()
362         builder.addClause({negLit(Var), posLit(LHS), posLit(RHS)});  in buildCNF()
363         builder.addClause({posLit(Var), negLit(LHS)});  in buildCNF()
364         builder.addClause({posLit(Var), negLit(RHS)});  in buildCNF()
374       builder.addClause({negLit(Var), negLit(Operand)});  in buildCNF()
375       builder.addClause({posLit(Var), posLit(Operand)});  in buildCNF()
386       builder.addClause({posLit(Var), posLit(LHS)});  in buildCNF()
387       builder.addClause({posLit(Var), negLit(RHS)});  in buildCNF()
388       builder.addClause({negLit(Var), negLit(LHS), posLit(RHS)});  in buildCNF()
399         builder.addClause(posLit(Var));  in buildCNF()
408       builder.addClause({posLit(Var), posLit(LHS), posLit(RHS)});  in buildCNF()
409       builder.addClause({posLit(Var), negLit(LHS), negLit(RHS)});  in buildCNF()
410       builder.addClause({negLit(Var), posLit(LHS), negLit(RHS)});  in buildCNF()
411       builder.addClause({negLit(Var), negLit(LHS), posLit(RHS)});  in buildCNF()
517     for (Variable Var = CNF.LargestVar; Var != NullVar; --Var) {  in WatchedLiteralsSolverImpl()  local
518       if (isWatched(posLit(Var)) || isWatched(negLit(Var)))  in WatchedLiteralsSolverImpl()
519         ActiveVars.push_back(Var);  in WatchedLiteralsSolverImpl()
568         const Variable Var = LevelVars[Level];  in solve()  local
569         VarAssignments[Var] = VarAssignments[Var] == Assignment::AssignedTrue  in solve()
644       const Variable Var = LevelVars[Level];  in reverseForcedMoves()  local
646       VarAssignments[Var] = Assignment::Unassigned;  in reverseForcedMoves()
650       if (isWatched(posLit(Var)) || isWatched(negLit(Var)))  in reverseForcedMoves()
651         ActiveVars.push_back(Var);  in reverseForcedMoves()
657     const Variable Var = LevelVars[Level];  in updateWatchedLiterals()  local
661     const Literal FalseLit = VarAssignments[Var] == Assignment::AssignedTrue  in updateWatchedLiterals()
662                                  ? negLit(Var)  in updateWatchedLiterals()
663                                  : posLit(Var);  in updateWatchedLiterals()
736   Assignment decideAssignment(Variable Var) const {  in decideAssignment()
737     return !isWatched(posLit(Var)) || isWatched(negLit(Var))  in decideAssignment()
755     return llvm::all_of(ActiveVars, [this](Variable Var) {  in activeVarsAreUnassigned()  argument
756       return VarAssignments[Var] == Assignment::Unassigned;  in activeVarsAreUnassigned()
763     return llvm::all_of(ActiveVars, [&WatchedLiterals](Variable Var) {  in activeVarsFormWatchedLiterals()  argument
764       return WatchedLiterals.contains(posLit(Var)) ||  in activeVarsFormWatchedLiterals()
765              WatchedLiterals.contains(negLit(Var));  in activeVarsFormWatchedLiterals()
775       const Variable Var = var(Lit);  in unassignedVarsFormingWatchedLiteralsAreActive()  local
776       if (VarAssignments[Var] != Assignment::Unassigned)  in unassignedVarsFormingWatchedLiteralsAreActive()
778       if (ActiveVarsSet.contains(Var))  in unassignedVarsFormingWatchedLiteralsAreActive()