45 using Variable = uint32_t;  typedef
49 static constexpr Variable NullVar = 0;
62 static constexpr Literal posLit(Variable V) { return 2 * V; }  in posLit()
65 static constexpr Literal negLit(Variable V) { return 2 * V + 1; }  in negLit()
71 static constexpr Variable var(Literal L) { return L >> 1; }  in var()
84   const Variable LargestVar;
125   llvm::DenseMap<Variable, AtomicBoolValue *> Atomics;
127   explicit BooleanFormula(Variable LargestVar,  in BooleanFormula()
128                           llvm::DenseMap<Variable, AtomicBoolValue *> Atomics)  in BooleanFormula()
188   llvm::DenseMap<BoolValue *, Variable> SubValsToVar;  in buildBooleanFormula()
190   llvm::DenseMap<Variable, AtomicBoolValue *> Atomics;  in buildBooleanFormula()
191   Variable NextVar = 1;  in buildBooleanFormula()
197       Variable Var = NextVar;  in buildBooleanFormula()
268     const Variable Var = GetVar(Val);  in buildBooleanFormula()
275       const Variable LeftSubVar = GetVar(&C->getLeftSubValue());  in buildBooleanFormula()
276       const Variable RightSubVar = GetVar(&C->getRightSubValue());  in buildBooleanFormula()
300       const Variable LeftSubVar = GetVar(&D->getLeftSubValue());  in buildBooleanFormula()
301       const Variable RightSubVar = GetVar(&D->getRightSubValue());  in buildBooleanFormula()
325       const Variable SubVar = GetVar(&N->getSubVal());  in buildBooleanFormula()
336       const Variable LeftSubVar = GetVar(&I->getLeftSubValue());  in buildBooleanFormula()
337       const Variable RightSubVar = GetVar(&I->getRightSubValue());  in buildBooleanFormula()
351       const Variable LeftSubVar = GetVar(&B->getLeftSubValue());  in buildBooleanFormula()
352       const Variable RightSubVar = GetVar(&B->getRightSubValue());  in buildBooleanFormula()
400   std::vector<Variable> LevelVars;
433   std::vector<Variable> ActiveVars;
450     for (Variable Var = Formula.LargestVar; Var != NullVar; --Var) {  in WatchedLiteralsSolverImpl()
470       const Variable ActiveVar = ActiveVars[I];  in solve()
490         const Variable Var = LevelVars[Level];  in solve()
567       const Variable Var = LevelVars[Level];  in reverseForcedMoves()
580     const Variable Var = LevelVars[Level];  in updateWatchedLiterals()
598       const Variable NewWatchedLitVar = var(NewWatchedLit);  in updateWatchedLiterals()
660   Assignment decideAssignment(Variable Var) const {  in decideAssignment()
679     return llvm::all_of(ActiveVars, [this](Variable Var) {  in activeVarsAreUnassigned()
687     return llvm::all_of(ActiveVars, [&WatchedLiterals](Variable Var) {  in activeVarsFormWatchedLiterals()
696     const llvm::DenseSet<Variable> ActiveVarsSet(ActiveVars.begin(),  in unassignedVarsFormingWatchedLiteralsAreActive()
699       const Variable Var = var(Lit);  in unassignedVarsFormingWatchedLiteralsAreActive()