make requested changes

Author: beckydvn

nnf/__init__.py

@@ -14,6 +14,7 @@
 
 __version__ = '0.2.1'
 
+from _typeshed import IdentityFunction
 import abc
 import functools
 import itertools
@@ -62,7 +63,6 @@
     "tseitin",
     "operators",
     "pysat",
-    "flatten_one_level"
 )
 
 
@@ -86,28 +86,36 @@ def all_models(names: 't.Iterable[Name]') -> t.Iterator[Model]:
 
 auto_simplify = False
 
+
 class NNF(metaclass=abc.ABCMeta):
     """Base class for all NNF sentences."""
     __slots__ = ("__weakref__",)
-    
-    
+
     def __and__(self: T_NNF, other: U_NNF) -> 'And[t.Union[T_NNF, U_NNF]]':
-        """And({self, other})""" 
+        """And({self, other})"""
         # prevent unnecessary nesting
-        if auto_simplify:
-            if type(self) == And:
-                return And({*self.children, *other.children}) if type(other) == And else And({*self.children, other})
+        if config.auto_simplify:
+            if not isinstance(self, And) and isinstance(other, And):
+                return And({self, *other.children})
+            elif isinstance(self, And) and not isinstance(other, And):
+                return And({*self.children, other})
+            elif isinstance(self, And) and isinstance(other, And):
+                return And({*self.children, *other.children})
         return And({self, other})
 
     def __or__(self: T_NNF, other: U_NNF) -> 'Or[t.Union[T_NNF, U_NNF]]':
         """Or({self, other})"""
         # prevent unnecessary nesting
-        if auto_simplify:
-            if type(self) == Or:
-                return Or({*self.children, *other.children}) if type(other) == Or else Or({*self.children, other})
+        if config.auto_simplify:
+            if not isinstance(self, Or) and isinstance(other, Or):
+                return Or({self, *other.children})
+            elif isinstance(self, Or) and not isinstance(other, Or):
+                return Or({*self.children, other})
+            elif isinstance(self, Or) and isinstance(other, Or):
+                return Or({*self.children, *other.children})
         return Or({self, other})
 
-    def __rshift__(self: T_NNF, other: U_NNF)-> 'Or[t.Union[T_NNF.negate(), U_NNF]]':
+    def __rshift__(self, other: 'NNF')-> 'Or[NNF]':
         """Or({self.negate(), other})"""
         return Or({self.negate(), other})
 
@@ -1802,6 +1810,7 @@ class _Config:
     sat_backend = _Setting("auto", {"auto", "native", "kissat", "pysat"})
     models_backend = _Setting("auto", {"auto", "native", "pysat"})
     pysat_solver = _Setting("minisat22")
+    auto_simplify = _Setting(False, {True, False})
 
     __slots__ = ()
 
@@ -1853,7 +1862,15 @@ def __call__(self, **settings: str) -> _ConfigContext:
 #:   `pysat.solvers.SolverNames
 #:   <https://pysathq.github.io/docs/html/api/solvers.html
 #:   #pysat.solvers.SolverNames>`_. Default: ``minisat22``.
+#:
+#: - ``auto_simplify``: An optional setting to prevent "extra" nesting when
+#:     NNF formulas are added onto with & or |.
+#:
+#:   - ``True``: Remove nesting whenever & or | are used on an NNF formula.
+#:   - ``False``: Generate formulas as normal, with nesting reflecting exactly
+#:     how the formula was created.
+
 config = _Config()
 
 
-from nnf import amc, dsharp, kissat, operators, pysat, tseitin  # noqa: E402
+from nnf import amc, dsharp, kissat, operators, pysat, tseitin  # noqa: E402

test_nnf.py

@@ -1105,3 +1105,84 @@ def test_models(sentence: nnf.NNF):
     models = list(sentence.models())
     assert len(real_models) == len(models)
     assert model_set(real_models) == model_set(models)
+
+
+def test_nesting():
+    a, b, c, d, e, f = Var("a"), Var("b"), Var("c"), Var("d"), \
+                       Var("e"), Var("f")
+
+    # test left nestings on And
+    config.auto_simplify = False
+    formula = a & (b & c)
+    formula = formula & (d | e)
+    assert formula == And({And({And({b, c}), a}), Or({d, e})})
+    config.auto_simplify = True
+    formula = a & (b & c)
+    formula = formula & (d | e)
+    assert formula == And({a, b, c, Or({d, e})})
+
+    # test right nestings on And
+    config.auto_simplify = False
+    formula = a & (b & c)
+    formula = (d | e) & formula
+    assert formula == And({And({And({b, c}), a}), Or({d, e})})
+    config.auto_simplify = True
+    formula = a & (b & c)
+    formula = (d | e) & formula
+    assert formula == And({a, b, c, Or({d, e})})
+
+    # test nestings on both sides with And
+    config.auto_simplify = False
+    formula = a & (b & c)
+    formula2 = d & (e & f)
+    formula = formula & formula2
+    assert formula == And({(And({a, And({b, c})})), And({d, And({e, f})})})
+    config.auto_simplify = True
+    formula = a & (b & c)
+    formula2 = d & (e & f)
+    formula = formula & formula2
+    assert formula == And({a, b, c, d, e, f})
+
+    # test left nestings on Or
+    config.auto_simplify = False
+    formula = a | (b | c)
+    formula = formula | (d & e)
+    assert formula == Or({Or({Or({b, c}), a}), And({d, e})})
+    config.auto_simplify = True
+    formula = a | (b | c)
+    formula = formula | (d & e)
+    assert formula == Or({a, b, c, And({d, e})})
+
+    # test right nestings on Or
+    config.auto_simplify = False
+    formula = a | (b | c)
+    formula = (d & e) | formula
+    assert formula == Or({Or({Or({b, c}), a}), And({d, e})})
+    config.auto_simplify = True
+    formula = a | (b | c)
+    formula = (d & e) | formula
+    assert formula == Or({a, b, c, And({d, e})})
+
+    # test nestings on both sides with Or
+    config.auto_simplify = False
+    formula = a | (b | c)
+    formula2 = d | (e | f)
+    formula = formula | formula2
+    assert formula == Or({(Or({a, Or({b, c})})), Or({d, Or({e, f})})})
+    config.auto_simplify = True
+    formula = a | (b | c)
+    formula2 = d | (e | f)
+    formula = formula | formula2
+    assert formula == Or({a, b, c, d, e, f})
+
+    # test nestings with both And and Or
+    config.auto_simplify = False
+    formula = a & (b | c)
+    formula2 = d & (e & f)
+    formula = formula | formula2
+    assert formula == Or({(And({a, Or({b, c})})), And({d, And({e, f})})})
+    config.auto_simplify = True
+    formula = a & (b | c)
+    formula2 = d & (e & f)
+    formula = formula | formula2
+    assert formula == Or({(And({a, Or({b, c})})), And({d, e, f})})