Allow empty clauses when dumping CNF

Author: blyxxyz

nnf/dimacs.py

@@ -145,8 +145,6 @@ def _dump_cnf(
         if not isinstance(clause, Or):
             raise TypeError("CNF sentences must be conjunctions of "
                             "disjunctions")
-        if not len(clause.children) > 0:
-            raise TypeError("CNF sentences shouldn't have empty clauses")
         first = True
         for child in clause.children:
             if not isinstance(child, Var):
@@ -294,16 +292,15 @@ def _parse_cnf(tokens: t.Iterable[str]) -> And[Or[Var]]:
     clause = set()  # type: t.Set[Var]
     for token in tokens:
         if token == '0':
-            if clause:
-                clauses.add(Or(clause))
+            clauses.add(Or(clause))
             clause = set()
         elif token == '%':
             # Some example files end with:
             # 0
             # %
             # 0
             # I don't know why.
-            pass
+            break
         elif token.startswith('-'):
             clause.add(Var(int(token[1:]), False))
         else:

nnf/dsharp.py

@@ -25,7 +25,7 @@
 import tempfile
 import typing as t
 
-from nnf import NNF, And, Or, Var, false, dimacs
+from nnf import NNF, And, Or, Var, false, true, dimacs
 from nnf.util import Name
 
 __all__ = ('load', 'loads', 'compile')
@@ -100,6 +100,12 @@ def compile(
     if not sentence.is_CNF():
         raise ValueError("Sentence must be in CNF")
 
+    # Handle cases D# doesn't like
+    if not sentence.children:
+        return true
+    if false in sentence.children:
+        return false
+
     var_labels = dict(enumerate(sentence.vars(), start=1))
     var_labels_inverse = {v: k for k, v in var_labels.items()}
 

test_nnf.py

@@ -126,7 +126,6 @@ def DNF(draw):
 @st.composite
 def CNF(draw):
     sentence = And(draw(st.frozensets(clauses())))
-    assume(len(sentence.children) > 0)
     return sentence
 
 
@@ -319,21 +318,15 @@ def test_arbitrary_dimacs_sat_serialize(sentence: nnf.NNF):
 
 
 @given(CNF())
-def test_arbitrary_dimacs_cnf_serialize(sentence: nnf.And):
-    assume(all(len(clause.children) > 0 for clause in sentence.children))
+def test_arbitrary_dimacs_cnf_serialize(sentence: And[Or[Var]]):
     reloaded = dimacs.loads(dimacs.dumps(sentence, mode='cnf'))
     assert reloaded.is_CNF()
     assert reloaded == sentence
 
 
 @given(NNF())
 def test_dimacs_cnf_serialize_accepts_only_cnf(sentence: nnf.NNF):
-    if (isinstance(sentence, And)
-            and all(isinstance(clause, Or)
-                    and all(isinstance(var, Var)
-                            for var in clause.children)
-                    and len(clause.children) > 0
-                    for clause in sentence.children)):
+    if sentence.is_CNF():
         event("CNF sentence")
         dimacs.dumps(sentence, mode='cnf')
     else:
@@ -818,18 +811,17 @@ def test_copying_does_not_copy(sentence: nnf.NNF):
 
 if shutil.which('dsharp') is not None:
     def test_dsharp_compile_uf20():
-        for sentence in uf20_cnf:
-            compiled = dsharp.compile(sentence)
-            compiled_smooth = dsharp.compile(sentence, smooth=True)
-            assert sentence.equivalent(compiled)
-            assert sentence.equivalent(compiled_smooth)
-            assert compiled.decomposable()
-            assert compiled_smooth.decomposable()
-            assert compiled_smooth.smooth()
+        sentence = uf20_cnf[0]
+        compiled = dsharp.compile(sentence)
+        compiled_smooth = dsharp.compile(sentence, smooth=True)
+        assert sentence.equivalent(compiled)
+        assert sentence.equivalent(compiled_smooth)
+        assert compiled.decomposable()
+        assert compiled_smooth.decomposable()
+        assert compiled_smooth.smooth()
 
     @given(CNF())
     def test_dsharp_compile(sentence: And[Or[Var]]):
-        assume(all(len(clause) > 0 for clause in sentence))
         compiled = dsharp.compile(sentence)
         compiled_smooth = dsharp.compile(sentence, smooth=True)
         assert compiled.decomposable()
@@ -841,7 +833,6 @@ def test_dsharp_compile(sentence: And[Or[Var]]):
 
     @given(CNF())
     def test_dsharp_compile_converting_names(sentence: And[Or[Var]]):
-        assume(all(len(clause) > 0 for clause in sentence))
         sentence = And(Or(Var(str(var.name), var.true) for var in clause)
                        for clause in sentence)
         compiled = dsharp.compile(sentence)
@@ -924,7 +915,6 @@ def test_kissat_uf20():
 
     @given(CNF())
     def test_kissat_cnf(sentence: And[Or[Var]]):
-        assume(all(len(clause) > 0 for clause in sentence))
         with using_kissat():
             assert sentence.satisfiable() == sentence._cnf_satisfiable_native()