| A clause represented in Conjunctive Normal Form. | A clause is a set of literals, either complemented or otherwise. For example: * {A1, A2, A3'} is the clause (A1 v A2 v A3') * {A5', A2', A1} is the clause (A5' v A2' v A1) Create model >>> clause = Clause(["
| 16 | |
| 17 | |
| 18 | class Clause: |
| 19 | """ |
| 20 | | A clause represented in Conjunctive Normal Form. |
| 21 | | A clause is a set of literals, either complemented or otherwise. |
| 22 | |
| 23 | For example: |
| 24 | * {A1, A2, A3'} is the clause (A1 v A2 v A3') |
| 25 | * {A5', A2', A1} is the clause (A5' v A2' v A1) |
| 26 | |
| 27 | Create model |
| 28 | |
| 29 | >>> clause = Clause(["A1", "A2'", "A3"]) |
| 30 | >>> clause.evaluate({"A1": True}) |
| 31 | True |
| 32 | """ |
| 33 | |
| 34 | def __init__(self, literals: list[str]) -> None: |
| 35 | """ |
| 36 | Represent the literals and an assignment in a clause." |
| 37 | """ |
| 38 | # Assign all literals to None initially |
| 39 | self.literals: dict[str, bool | None] = dict.fromkeys(literals) |
| 40 | |
| 41 | def __str__(self) -> str: |
| 42 | """ |
| 43 | To print a clause as in Conjunctive Normal Form. |
| 44 | |
| 45 | >>> str(Clause(["A1", "A2'", "A3"])) |
| 46 | "{A1 , A2' , A3}" |
| 47 | """ |
| 48 | return "{" + " , ".join(self.literals) + "}" |
| 49 | |
| 50 | def __len__(self) -> int: |
| 51 | """ |
| 52 | To print a clause as in Conjunctive Normal Form. |
| 53 | |
| 54 | >>> len(Clause([])) |
| 55 | 0 |
| 56 | >>> len(Clause(["A1", "A2'", "A3"])) |
| 57 | 3 |
| 58 | """ |
| 59 | return len(self.literals) |
| 60 | |
| 61 | def assign(self, model: dict[str, bool | None]) -> None: |
| 62 | """ |
| 63 | Assign values to literals of the clause as given by model. |
| 64 | """ |
| 65 | for literal in self.literals: |
| 66 | symbol = literal[:2] |
| 67 | if symbol in model: |
| 68 | value = model[symbol] |
| 69 | else: |
| 70 | continue |
| 71 | # Complement assignment if literal is in complemented form |
| 72 | if value is not None and literal.endswith("'"): |
| 73 | value = not value |
| 74 | self.literals[literal] = value |
| 75 |