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 {
99   std::vector<Assignment> VarAssignments;
135     VarAssignments.resize(CNF.largestVar() + 1, Assignment::Unassigned);
178         // assignment.
190         VarAssignments[Var] = VarAssignments[Var] == Assignment::AssignedTrue
191                                   ? Assignment::AssignedFalse
192                                   : Assignment::AssignedTrue;
203             unitPosLit ? Assignment::AssignedTrue : Assignment::AssignedFalse;
246   /// Returns a satisfying truth assignment to the atoms in the boolean formula.
247   llvm::DenseMap<Atom, Solver::Result::Assignment> buildSolution() {
248     llvm::DenseMap<Atom, Solver::Result::Assignment> Solution;
250       // A variable may have a definite true/false assignment, or it may be
254           VarAssignments[Atomic.first] == Assignment::AssignedFalse
255               ? Solver::Result::Assignment::AssignedFalse
256               : Solver::Result::Assignment::AssignedTrue;
262   /// made on the assignment of a variable.
267       VarAssignments[Var] = Assignment::Unassigned;
276   /// Updates watched literals that are affected by a variable assignment.
282     const Literal FalseLit = VarAssignments[Var] == Assignment::AssignedTrue
308           VarAssignments[NewWatchedLitVar] == Assignment::Unassigned)
346   /// partial assignment.
355   /// Returns an assignment for an unassigned variable.
356   Assignment decideAssignment(Variable Var) const {
358                ? Assignment::AssignedFalse
359                : Assignment::AssignedTrue;
376       return VarAssignments[Var] == Assignment::Unassigned;
396       if (VarAssignments[Var] != Assignment::Unassigned)