Refactor the parameter name.

Author: haz

nnf/__init__.py

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

nnf/tseitin.py

@@ -10,11 +10,11 @@
 from nnf.util import memoize
 
 
-def to_CNF(theory: NNF, simplify_tautologies: bool = True) -> And[Or[Var]]:
+def to_CNF(theory: NNF, simplify: 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.
+    :param simplify: If True, remove clauses that are always true.
     """
 
     clauses = []
@@ -35,7 +35,7 @@ def process_node(node: NNF) -> Var:
 
         aux = Var.aux()
 
-        if simplify_tautologies and any(~var in children for var in children):
+        if simplify and any(~var in children for var in children):
             if isinstance(node, And):
                 clauses.append(Or({~aux}))
             else:
@@ -74,7 +74,7 @@ def process_required(node: NNF) -> None:
 
         elif isinstance(node, Or):
             children = {process_node(c) for c in node.children}
-            if simplify_tautologies and any(~v in children for v in children):
+            if simplify and any(~v in children for v in children):
                 return
             clauses.append(Or(children))
 

test_nnf.py

@@ -1108,19 +1108,19 @@ def test_models(sentence: nnf.NNF):
 
 
 @given(NNF())
-def test_tautology_simplification_names(sentence: nnf.NNF):
+def test_toCNF_simplification_names(sentence: nnf.NNF):
     names1 = set(sentence.vars())
-    T = sentence.to_CNF(simplify_tautologies=False)
+    T = sentence.to_CNF(simplify=False)
     names2 = set({v for v in T.vars() if not isinstance(v, nnf.Aux)})
     assert names1 == names2
 
 
-def test_tautology_simplification():
+def test_toCNF_simplification():
     x = Var("x")
     T = x | ~x
 
     T1 = T.to_CNF()
-    T2 = T.to_CNF(simplify_tautologies=False)
+    T2 = T.to_CNF(simplify=False)
 
     assert T1 == nnf.true
     assert T1.is_CNF()