Lines Matching full:assignment
56 /// The search for a satisfying assignment of the variables in `Formula` will
60 /// consistent partial assignment, `Level` will be incremented. Otherwise, if
88 enum class Assignment : int8_t { enum in clang::dataflow::__anondce44e890111::WatchedLiteralsSolverImpl
99 std::vector<Assignment> VarAssignments;
135 VarAssignments.resize(CNF.largestVar() + 1, Assignment::Unassigned); in WatchedLiteralsSolverImpl()
178 // assignment. in solve()
190 VarAssignments[Var] = VarAssignments[Var] == Assignment::AssignedTrue in solve()
191 ? Assignment::AssignedFalse in solve()
192 : Assignment::AssignedTrue; in solve()
203 unitPosLit ? Assignment::AssignedTrue : Assignment::AssignedFalse; in solve()
246 /// Returns a satisfying truth assignment to the atoms in the boolean formula.
247 llvm::DenseMap<Atom, Solver::Result::Assignment> buildSolution() { in buildSolution()
248 llvm::DenseMap<Atom, Solver::Result::Assignment> Solution; in buildSolution()
250 // A variable may have a definite true/false assignment, or it may be in buildSolution()
254 VarAssignments[Atomic.first] == Assignment::AssignedFalse in buildSolution()
255 ? Solver::Result::Assignment::AssignedFalse in buildSolution()
256 : Solver::Result::Assignment::AssignedTrue; in buildSolution()
262 /// made on the assignment of a variable.
267 VarAssignments[Var] = Assignment::Unassigned; in reverseForcedMoves()
276 /// Updates watched literals that are affected by a variable assignment.
282 const Literal FalseLit = VarAssignments[Var] == Assignment::AssignedTrue in updateWatchedLiterals()
308 VarAssignments[NewWatchedLitVar] == Assignment::Unassigned) in updateWatchedLiterals()
346 /// partial assignment.
355 /// Returns an assignment for an unassigned variable.
356 Assignment decideAssignment(Variable Var) const { in decideAssignment()
358 ? Assignment::AssignedFalse in decideAssignment()
359 : Assignment::AssignedTrue; in decideAssignment()
376 return VarAssignments[Var] == Assignment::Unassigned; in activeVarsAreUnassigned()
396 if (VarAssignments[Var] != Assignment::Unassigned) in unassignedVarsFormingWatchedLiteralsAreActive()