diff --git a/nnf/__init__.py b/nnf/__init__.py index 7742784..0c1e3a9 100644 --- a/nnf/__init__.py +++ b/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 #: `_. 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() diff --git a/test_nnf.py b/test_nnf.py index 11880a9..f1d4a9c 100644 --- a/test_nnf.py +++ b/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})})