Add Implication and Remove Nesting

nnf/__init__.py

@@ -14,6 +14,7 @@
 
 __version__ = '0.2.1'
 
+from _typeshed import IdentityFunction
 import abc
 import functools
 import itertools
@@ -83,19 +84,41 @@ def all_models(names: 't.Iterable[Name]') -> t.Iterator[Model]:
             new[name] = True
             yield new
 
+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})"""
+        # prevent unnecessary nesting
+        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 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, other: 'NNF')-> 'Or[NNF]':
+        """Or({self.negate(), other})"""
+        return Or({self.negate(), other})
+
     def walk(self) -> t.Iterator['NNF']:
         """Yield all nodes in the sentence, depth-first.
 
@@ -1714,7 +1737,6 @@ def decision(
     """
     return (var & if_true) | (~var & if_false)
 
-
 #: A node that's always true. Technically an And node without children.
 true = And()  # type: And[Bottom]
 #: A node that's always false. Technically an Or node without children.
@@ -1788,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__ = ()
 
@@ -1839,6 +1862,14 @@ 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()
 
 

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})})