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()
273     const Variable Var = GetVar(Val);  in buildBooleanFormula()
280       const Variable LeftSubVar = GetVar(&C->getLeftSubValue());  in buildBooleanFormula()
281       const Variable RightSubVar = GetVar(&C->getRightSubValue());  in buildBooleanFormula()
305       const Variable LeftSubVar = GetVar(&D->getLeftSubValue());  in buildBooleanFormula()
306       const Variable RightSubVar = GetVar(&D->getRightSubValue());  in buildBooleanFormula()
330       const Variable SubVar = GetVar(&N->getSubVal());  in buildBooleanFormula()
341       const Variable LeftSubVar = GetVar(&I->getLeftSubValue());  in buildBooleanFormula()
342       const Variable RightSubVar = GetVar(&I->getRightSubValue());  in buildBooleanFormula()
356       const Variable LeftSubVar = GetVar(&B->getLeftSubValue());  in buildBooleanFormula()
357       const Variable RightSubVar = GetVar(&B->getRightSubValue());  in buildBooleanFormula()
405   std::vector<Variable> LevelVars;
438   std::vector<Variable> ActiveVars;
455     for (Variable Var = Formula.LargestVar; Var != NullVar; --Var) {  in WatchedLiteralsSolverImpl()
475       const Variable ActiveVar = ActiveVars[I];  in solve()
495         const Variable Var = LevelVars[Level];  in solve()
572       const Variable Var = LevelVars[Level];  in reverseForcedMoves()
585     const Variable Var = LevelVars[Level];  in updateWatchedLiterals()
603       const Variable NewWatchedLitVar = var(NewWatchedLit);  in updateWatchedLiterals()
665   Assignment decideAssignment(Variable Var) const {  in decideAssignment()
684     return llvm::all_of(ActiveVars, [this](Variable Var) {  in activeVarsAreUnassigned()
692     return llvm::all_of(ActiveVars, [&WatchedLiterals](Variable Var) {  in activeVarsFormWatchedLiterals()
701     const llvm::DenseSet<Variable> ActiveVarsSet(ActiveVars.begin(),  in unassignedVarsFormingWatchedLiteralsAreActive()
704       const Variable Var = var(Lit);  in unassignedVarsFormingWatchedLiteralsAreActive()