Add Implication and Remove Nesting

nnf/__init__.py

@@ -62,6 +62,7 @@
     "tseitin",
     "operators",
     "pysat",
+    "flatten_one_level"
 )
 
 
@@ -83,19 +84,33 @@ 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})"""
+        """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})
         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})
         return Or({self, other})
 
+    def __rshift__(self: T_NNF, other: U_NNF)-> 'Or[t.Union[T_NNF.negate(), U_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 +1729,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.
@@ -1842,4 +1856,4 @@ def __call__(self, **settings: str) -> _ConfigContext:
 config = _Config()
 
 
-from nnf import amc, dsharp, kissat, operators, pysat, tseitin  # noqa: E402
+from nnf import amc, dsharp, kissat, operators, pysat, tseitin  # noqa: E402