Merge pull request #27 from beckydvn/add-implication-remove-nesting

Add Implication and Remove Nesting

nnf/__init__.py

@@ -90,12 +90,32 @@ class NNF(metaclass=abc.ABCMeta):
 
     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.
 
@@ -1788,6 +1808,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 +1860,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,85 @@ def test_models(sentence: nnf.NNF):
     models = list(sentence.models())
     assert len(real_models) == len(models)
     assert model_set(real_models) == model_set(models)
+
+
+@config(auto_simplify=False)
+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})})