48 using Variable = uint32_t;  typedef
52 static constexpr Variable NullVar = 0;
65 static constexpr Literal posLit(Variable V) { return 2 * V; }  in posLit()
72 static constexpr Literal negLit(Variable V) { return 2 * V + 1; }  in negLit()
78 static constexpr Variable var(Literal L) { return L >> 1; }  in var()
91   const Variable LargestVar;
132   llvm::DenseMap<Variable, Atom> Atomics;
138   explicit CNFFormula(Variable LargestVar,  in CNFFormula()
139                       llvm::DenseMap<Variable, Atom> Atomics)  in CNFFormula()
240       const Variable v = var(lit);  in addClause()
255   llvm::DenseSet<Variable> trueVars;
256   llvm::DenseSet<Variable> falseVars;
269   llvm::DenseMap<const Formula *, Variable> SubValsToVar;  in buildCNF()
271   llvm::DenseMap<Variable, Atom> Atomics;  in buildCNF()
272   Variable NextVar = 1;  in buildCNF()
278       Variable Var = NextVar;  in buildCNF()
316     const Variable Var = GetVar(Val);  in buildCNF()
329       const Variable LHS = GetVar(Val->operands()[0]);  in buildCNF()
330       const Variable RHS = GetVar(Val->operands()[1]);  in buildCNF()
349       const Variable LHS = GetVar(Val->operands()[0]);  in buildCNF()
350       const Variable RHS = GetVar(Val->operands()[1]);  in buildCNF()
369       const Variable Operand = GetVar(Val->operands()[0]);  in buildCNF()
379       const Variable LHS = GetVar(Val->operands()[0]);  in buildCNF()
380       const Variable RHS = GetVar(Val->operands()[1]);  in buildCNF()
392       const Variable LHS = GetVar(Val->operands()[0]);  in buildCNF()
393       const Variable RHS = GetVar(Val->operands()[1]);  in buildCNF()
466   std::vector<Variable> LevelVars;
499   std::vector<Variable> ActiveVars;
517     for (Variable Var = CNF.LargestVar; Var != NullVar; --Var) {  in WatchedLiteralsSolverImpl()
548       const Variable ActiveVar = ActiveVars[I];  in solve()
568         const Variable Var = LevelVars[Level];  in solve()
644       const Variable Var = LevelVars[Level];  in reverseForcedMoves()
657     const Variable Var = LevelVars[Level];  in updateWatchedLiterals()
675       const Variable NewWatchedLitVar = var(NewWatchedLit);  in updateWatchedLiterals()
736   Assignment decideAssignment(Variable Var) const {  in decideAssignment()
755     return llvm::all_of(ActiveVars, [this](Variable Var) {  in activeVarsAreUnassigned()
763     return llvm::all_of(ActiveVars, [&WatchedLiterals](Variable Var) {  in activeVarsFormWatchedLiterals()
772     const llvm::DenseSet<Variable> ActiveVarsSet(ActiveVars.begin(),  in unassignedVarsFormingWatchedLiteralsAreActive()
775       const Variable Var = var(Lit);  in unassignedVarsFormingWatchedLiteralsAreActive()