Fix .implicates() docs and tests. Resolves #3.

Author: blyxxyz

nnf/__init__.py

@@ -781,13 +781,16 @@ def implicants(self) -> 'Or[And[Var]]':
         return Or(self._do_PI()[0])
 
     def implicates(self) -> 'And[Or[Var]]':
-        """Extract the prime implicates of the sentence.
+        """Extract a prime implicate cover of the sentence.
 
         Prime implicates are the minimal implied clauses. This method
         returns a conjunction of clauses that's equivalent to the original
         sentence, and minimal, meaning that there are no clauses implied by
         the sentence that are strict subsets of any of the clauses in this
         representation, so no clauses could be made smaller.
+
+        While :meth:`NNF.implicants` returns all implicants, this method may
+        only return some of the implicates.
         """
         return And(self._do_PI()[1])
 

test_nnf.py

@@ -610,20 +610,37 @@ def test_implicates_implicants_idempotent(sentence: nnf.NNF):
     assert implicates.implicants() == implicants
 
 
-# TODO: This test fails, see the example below.
-# I don't know if this is a bug in the test or in the implementation.
-@pytest.mark.xfail
 @given(NNF())
 def test_implicates_implicants_negation_rule(sentence: nnf.NNF):
-    assert sentence.negate().implicants().negate() == sentence.implicates()
-    assert sentence.negate().implicates().negate() == sentence.implicants()
+    """Any implicate is also a negated implicant of the negated sentence.
+
+    .implicates() gives some implicates, and .implicants() gives all
+    implicants.
+
+    So sentence.negate().implicants().negate() gives all implicates,
+    and sentence.negate().implicates().negate() gives some implicants.
+    """
+    assert (
+        sentence.negate().implicants().negate().children
+        >= sentence.implicates().children
+    )
+    assert (
+        sentence.negate().implicates().negate().children
+        <= sentence.implicants().children
+    )
 
 
-@pytest.mark.xfail(strict=True)
 def test_implicates_implicants_negation_rule_example():
+    """These failed an old version of the previous test. See issue #3."""
     sentence = Or({And({~Var(1), Var(2)}), And({~Var(3), Var(1)})})
-    assert sentence.negate().implicants().negate() == sentence.implicates()
-    assert sentence.negate().implicates().negate() == sentence.implicants()
+    assert (
+        sentence.negate().implicants().negate().children
+        >= sentence.implicates().children
+    )
+    assert (
+        sentence.negate().implicates().negate().children
+        <= sentence.implicants().children
+    )
 
 
 @given(NNF(), NNF())