Simplify tautologies

nnf/__init__.py

@@ -574,9 +574,9 @@ def neg(node: NNF) -> NNF:
 
         return neg(self)
 
-    def to_CNF(self) -> 'And[Or[Var]]':
+    def to_CNF(self, simplify_tautologies: bool = True) -> 'And[Or[Var]]':
         """Compile theory to a semantically equivalent CNF formula."""
-        return tseitin.to_CNF(self)
+        return tseitin.to_CNF(self, simplify_tautologies)
 
     def _cnf_satisfiable(self) -> bool:
         """Call a SAT solver on the presumed CNF theory."""

nnf/tseitin.py

@@ -10,10 +10,11 @@
 from nnf.util import memoize
 
 
-def to_CNF(theory: NNF) -> And[Or[Var]]:
+def to_CNF(theory: NNF, simplify_tautologies: bool = True) -> And[Or[Var]]:
     """Convert an NNF into CNF using the Tseitin Encoding.
 
     :param theory: Theory to convert.
+    :param simplify_tautologies: If True, remove clauses that are always true.
     """
 
     clauses = []
@@ -73,7 +74,7 @@ def process_required(node: NNF) -> None:
 
         elif isinstance(node, Or):
             children = {process_node(c) for c in node.children}
-            if any(~var in children for var in children):
+            if simplify_tautologies and any(~v in children for v in children):
                 return
             clauses.append(Or(children))
 

test_nnf.py

@@ -1107,6 +1107,21 @@ def test_models(sentence: nnf.NNF):
     assert model_set(real_models) == model_set(models)
 
 
+def test_tautology_simplification():
+    x = Var("x")
+    T = x | ~x
+
+    T1 = T.to_CNF()
+    T2 = T.to_CNF(simplify_tautologies=False)
+
+    assert T1 == nnf.true
+    assert T1.is_CNF()
+
+    assert T2 != nnf.true
+    assert T2 == And({Or({~x, x})})
+    assert T2.is_CNF()
+
+
 @config(auto_simplify=False)
 def test_nesting():
     a, b, c, d, e, f = Var("a"), Var("b"), Var("c"), Var("d"), \