Evaluates the clause with the assignments in model. This has the following steps: 1. Return ``True`` if both a literal and its complement exist in the clause. 2. Return ``True`` if a single literal has the assignment ``True``. 3. Return ``None`` (unabl
(self, model: dict[str, bool | None])
| 74 | self.literals[literal] = value |
| 75 | |
| 76 | def evaluate(self, model: dict[str, bool | None]) -> bool | None: |
| 77 | """ |
| 78 | Evaluates the clause with the assignments in model. |
| 79 | |
| 80 | This has the following steps: |
| 81 | 1. Return ``True`` if both a literal and its complement exist in the clause. |
| 82 | 2. Return ``True`` if a single literal has the assignment ``True``. |
| 83 | 3. Return ``None`` (unable to complete evaluation) |
| 84 | if a literal has no assignment. |
| 85 | 4. Compute disjunction of all values assigned in clause. |
| 86 | """ |
| 87 | for literal in self.literals: |
| 88 | symbol = literal.rstrip("'") if literal.endswith("'") else literal + "'" |
| 89 | if symbol in self.literals: |
| 90 | return True |
| 91 | |
| 92 | self.assign(model) |
| 93 | for value in self.literals.values(): |
| 94 | if value in (True, None): |
| 95 | return value |
| 96 | return any(self.literals.values()) |
| 97 | |
| 98 | |
| 99 | class Formula: |
no test coverage detected