Lines Matching refs:Var
197 Variable Var = NextVar; in buildBooleanFormula() local
201 if (!SubValsToVar.try_emplace(Val, Var).second) in buildBooleanFormula()
242 Atomics[Var] = cast<AtomicBoolValue>(Val); in buildBooleanFormula()
273 const Variable Var = GetVar(Val); in buildBooleanFormula() local
275 if (ProcessedSubVals[Var]) in buildBooleanFormula()
277 ProcessedSubVals[Var] = true; in buildBooleanFormula()
287 Formula.addClause(negLit(Var), posLit(LeftSubVar)); in buildBooleanFormula()
288 Formula.addClause(posLit(Var), negLit(LeftSubVar)); in buildBooleanFormula()
296 Formula.addClause(negLit(Var), posLit(LeftSubVar)); in buildBooleanFormula()
297 Formula.addClause(negLit(Var), posLit(RightSubVar)); in buildBooleanFormula()
298 Formula.addClause(posLit(Var), negLit(LeftSubVar), negLit(RightSubVar)); in buildBooleanFormula()
312 Formula.addClause(negLit(Var), posLit(LeftSubVar)); in buildBooleanFormula()
313 Formula.addClause(posLit(Var), negLit(LeftSubVar)); in buildBooleanFormula()
321 Formula.addClause(negLit(Var), posLit(LeftSubVar), posLit(RightSubVar)); in buildBooleanFormula()
322 Formula.addClause(posLit(Var), negLit(LeftSubVar)); in buildBooleanFormula()
323 Formula.addClause(posLit(Var), negLit(RightSubVar)); in buildBooleanFormula()
335 Formula.addClause(negLit(Var), negLit(SubVar)); in buildBooleanFormula()
336 Formula.addClause(posLit(Var), posLit(SubVar)); in buildBooleanFormula()
348 Formula.addClause(posLit(Var), posLit(LeftSubVar)); in buildBooleanFormula()
349 Formula.addClause(posLit(Var), negLit(RightSubVar)); in buildBooleanFormula()
350 Formula.addClause(negLit(Var), negLit(LeftSubVar), posLit(RightSubVar)); in buildBooleanFormula()
363 Formula.addClause(posLit(Var)); in buildBooleanFormula()
371 Formula.addClause(posLit(Var), posLit(LeftSubVar), posLit(RightSubVar)); in buildBooleanFormula()
372 Formula.addClause(posLit(Var), negLit(LeftSubVar), negLit(RightSubVar)); in buildBooleanFormula()
373 Formula.addClause(negLit(Var), posLit(LeftSubVar), negLit(RightSubVar)); in buildBooleanFormula()
374 Formula.addClause(negLit(Var), negLit(LeftSubVar), posLit(RightSubVar)); in buildBooleanFormula()
455 for (Variable Var = Formula.LargestVar; Var != NullVar; --Var) { in WatchedLiteralsSolverImpl() local
456 if (isWatched(posLit(Var)) || isWatched(negLit(Var))) in WatchedLiteralsSolverImpl()
457 ActiveVars.push_back(Var); in WatchedLiteralsSolverImpl()
495 const Variable Var = LevelVars[Level]; in solve() local
496 VarAssignments[Var] = VarAssignments[Var] == Assignment::AssignedTrue in solve()
572 const Variable Var = LevelVars[Level]; in reverseForcedMoves() local
574 VarAssignments[Var] = Assignment::Unassigned; in reverseForcedMoves()
578 if (isWatched(posLit(Var)) || isWatched(negLit(Var))) in reverseForcedMoves()
579 ActiveVars.push_back(Var); in reverseForcedMoves()
585 const Variable Var = LevelVars[Level]; in updateWatchedLiterals() local
589 const Literal FalseLit = VarAssignments[Var] == Assignment::AssignedTrue in updateWatchedLiterals()
590 ? negLit(Var) in updateWatchedLiterals()
591 : posLit(Var); in updateWatchedLiterals()
665 Assignment decideAssignment(Variable Var) const { in decideAssignment()
666 return !isWatched(posLit(Var)) || isWatched(negLit(Var)) in decideAssignment()
684 return llvm::all_of(ActiveVars, [this](Variable Var) { in activeVarsAreUnassigned() argument
685 return VarAssignments[Var] == Assignment::Unassigned; in activeVarsAreUnassigned()
692 return llvm::all_of(ActiveVars, [&WatchedLiterals](Variable Var) { in activeVarsFormWatchedLiterals() argument
693 return WatchedLiterals.contains(posLit(Var)) || in activeVarsFormWatchedLiterals()
694 WatchedLiterals.contains(negLit(Var)); in activeVarsFormWatchedLiterals()
704 const Variable Var = var(Lit); in unassignedVarsFormingWatchedLiteralsAreActive() local
705 if (VarAssignments[Var] != Assignment::Unassigned) in unassignedVarsFormingWatchedLiteralsAreActive()
707 if (ActiveVarsSet.contains(Var)) in unassignedVarsFormingWatchedLiteralsAreActive()