From e8dee23b43f17644d035cc58adfaaa5f32ff3f5f Mon Sep 17 00:00:00 2001
From: Christian Muise <christian.muise@gmail.com>
Date: Thu, 8 Dec 2022 21:13:35 -0500
Subject: [PATCH] Adding option to avoid simplification in conversion to CNF.

---
 nnf/__init__.py |  4 ++--
 nnf/tseitin.py  |  4 ++--
 test_nnf.py     | 15 +++++++++++++++
 3 files changed, 19 insertions(+), 4 deletions(-)

diff --git a/nnf/__init__.py b/nnf/__init__.py
index 0c1e3a9..d107f09 100644
--- a/nnf/__init__.py
+++ b/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=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."""
diff --git a/nnf/tseitin.py b/nnf/tseitin.py
index bfa4ce3..55d685b 100644
--- a/nnf/tseitin.py
+++ b/nnf/tseitin.py
@@ -10,7 +10,7 @@
 from nnf.util import memoize
 
 
-def to_CNF(theory: NNF) -> And[Or[Var]]:
+def to_CNF(theory: NNF, simplify_tautologies=True) -> And[Or[Var]]:
     """Convert an NNF into CNF using the Tseitin Encoding.
 
     :param theory: Theory to convert.
@@ -73,7 +73,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(~var in children for var in children):
                 return
             clauses.append(Or(children))
 
diff --git a/test_nnf.py b/test_nnf.py
index f1d4a9c..427fea9 100644
--- a/test_nnf.py
+++ b/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"), \