| A formula represented in Conjunctive Normal Form. | A formula is a set of clauses. | For example, | {{A1, A2, A3'}, {A5', A2', A1}} is ((A1 v A2 v A3') and (A5' v A2' v A1))
| 97 | |
| 98 | |
| 99 | class Formula: |
| 100 | """ |
| 101 | | A formula represented in Conjunctive Normal Form. |
| 102 | | A formula is a set of clauses. |
| 103 | | For example, |
| 104 | | {{A1, A2, A3'}, {A5', A2', A1}} is ((A1 v A2 v A3') and (A5' v A2' v A1)) |
| 105 | """ |
| 106 | |
| 107 | def __init__(self, clauses: Iterable[Clause]) -> None: |
| 108 | """ |
| 109 | Represent the number of clauses and the clauses themselves. |
| 110 | """ |
| 111 | self.clauses = list(clauses) |
| 112 | |
| 113 | def __str__(self) -> str: |
| 114 | """ |
| 115 | To print a formula as in Conjunctive Normal Form. |
| 116 | |
| 117 | >>> str(Formula([Clause(["A1", "A2'", "A3"]), Clause(["A5'", "A2'", "A1"])])) |
| 118 | "{{A1 , A2' , A3} , {A5' , A2' , A1}}" |
| 119 | """ |
| 120 | return "{" + " , ".join(str(clause) for clause in self.clauses) + "}" |
| 121 | |
| 122 | |
| 123 | def generate_clause() -> Clause: |