From 6404074774883d69753f6c67cec6161ac0750a52 Mon Sep 17 00:00:00 2001 From: beckydvn Date: Sat, 18 Sep 2021 20:35:18 -0400 Subject: [PATCH 01/18] add __rshift__ --- nnf/__init__.py | 3 +++ 1 file changed, 3 insertions(+) diff --git a/nnf/__init__.py b/nnf/__init__.py index 7742784..09db320 100644 --- a/nnf/__init__.py +++ b/nnf/__init__.py @@ -96,6 +96,9 @@ def __or__(self: T_NNF, other: U_NNF) -> 'Or[t.Union[T_NNF, U_NNF]]': """Or({self, other})""" return Or({self, other}) + def __rshift__(self: T_NNF, other: U_NNF): + return Or({self.negate(), other}) + def walk(self) -> t.Iterator['NNF']: """Yield all nodes in the sentence, depth-first. From 56037e076f57ec64d7877bbccc51c5d8982b0653 Mon Sep 17 00:00:00 2001 From: beckydvn Date: Sun, 19 Sep 2021 11:48:14 -0400 Subject: [PATCH 02/18] add docs --- nnf/__init__.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/nnf/__init__.py b/nnf/__init__.py index 09db320..e077b9e 100644 --- a/nnf/__init__.py +++ b/nnf/__init__.py @@ -96,7 +96,8 @@ def __or__(self: T_NNF, other: U_NNF) -> 'Or[t.Union[T_NNF, U_NNF]]': """Or({self, other})""" return Or({self, other}) - def __rshift__(self: T_NNF, other: U_NNF): + 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']: From cc7e5adcbff948257654987abc7a208ca84f8b2a Mon Sep 17 00:00:00 2001 From: beckydvn Date: Sun, 19 Sep 2021 12:27:35 -0400 Subject: [PATCH 03/18] fix nesting issue --- nnf/__init__.py | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/nnf/__init__.py b/nnf/__init__.py index e077b9e..ff2120e 100644 --- a/nnf/__init__.py +++ b/nnf/__init__.py @@ -90,10 +90,16 @@ 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 type(self) == And: + return 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 type(self) == Or: + return Or({*self.children, other}) return Or({self, other}) def __rshift__(self: T_NNF, other: U_NNF)-> 'Or[t.Union[T_NNF.negate(), U_NNF]]': @@ -1846,4 +1852,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 \ No newline at end of file From d3dc209acc948dbaf2a90fb0bdede947bf3b1617 Mon Sep 17 00:00:00 2001 From: beckydvn Date: Sun, 19 Sep 2021 15:24:14 -0400 Subject: [PATCH 04/18] allow for two And's to be joined --- nnf/__init__.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/nnf/__init__.py b/nnf/__init__.py index ff2120e..803e4aa 100644 --- a/nnf/__init__.py +++ b/nnf/__init__.py @@ -92,7 +92,7 @@ def __and__(self: T_NNF, other: U_NNF) -> 'And[t.Union[T_NNF, U_NNF]]': """And({self, other})""" # prevent unnecessary nesting if type(self) == And: - return And({*self.children, other}) + 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]]': From af2d101c523fa7e160386a201f04bca7a0c6ac6e Mon Sep 17 00:00:00 2001 From: beckydvn Date: Tue, 21 Sep 2021 16:23:53 -0400 Subject: [PATCH 05/18] convert to flatten function --- nnf/__init__.py | 84 ++++++++++++++++++++++++++++++++++++++++++++----- 1 file changed, 77 insertions(+), 7 deletions(-) diff --git a/nnf/__init__.py b/nnf/__init__.py index 803e4aa..196276f 100644 --- a/nnf/__init__.py +++ b/nnf/__init__.py @@ -90,17 +90,24 @@ 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 type(self) == And: - return And({*self.children, *other.children}) if type(other) == And else And({*self.children, other}) return And({self, other}) + # if not flatten: + # return And({self, other}) + # else: + # # optionally prevent unnecessary nesting + # if type(self) == And: + # return And({*self.children, *other.children}) if type(other) == And else And({*self.children, other}) + def __or__(self: T_NNF, other: U_NNF) -> 'Or[t.Union[T_NNF, U_NNF]]': """Or({self, other})""" - # prevent unnecessary nesting - if type(self) == Or: - return Or({*self.children, other}) return Or({self, other}) + # if not flatten: + # return Or({self, other}) + # else: + # # optionally prevent unnecessary nesting + # if type(self) == Or: + # return Or({*self.children, *other.children}) if type(other) == Or else Or({*self.children, other}) def __rshift__(self: T_NNF, other: U_NNF)-> 'Or[t.Union[T_NNF.negate(), U_NNF]]': """Or({self.negate(), other})""" @@ -1724,6 +1731,26 @@ def decision( """ return (var & if_true) | (~var & if_false) +def flatten(nnf: NNF, operator_type: t.Union[And, Or]): + set_and_children = set() + set_other = set() + if type(nnf) == operator_type: + for c in nnf.children: + if type(c) == Var: + set_and_children.add(c) + elif len(c.children) == 1: + set_and_children.update(c.children) + elif type(c) == operator_type: + set_and_children.update(c.children) + else: + set_other.update(c) + nnf = operator_type(set_and_children | set_other) + + for c in nnf.children: + if type(c) == operator_type: + return flatten(nnf, operator_type) + return nnf + #: A node that's always true. Technically an And node without children. true = And() # type: And[Bottom] @@ -1852,4 +1879,47 @@ def __call__(self, **settings: str) -> _ConfigContext: config = _Config() -from nnf import amc, dsharp, kissat, operators, pysat, tseitin # noqa: E402 \ No newline at end of file +from nnf import amc, dsharp, kissat, operators, pysat, tseitin # noqa: E402 + +""" +# test nnf nesting - and +print() +nnf_formula = Var(1) +for i in range(10): + nnf_formula = nnf_formula & Var(i) +print(nnf_formula) +print(flatten(nnf_formula, And)) + +nnf_formula_2 = Var(10) +for i in range(11, 20): + nnf_formula_2 = nnf_formula_2 & Var(i) +nnf_formula_3 = nnf_formula & nnf_formula_2 +print() +print(nnf_formula_3) +print(flatten(nnf_formula_3, And)) + +# test nnf nesting - or +print() +nnf_formula = Var(1) +for i in range(10): + nnf_formula = nnf_formula | Var(i) +print(nnf_formula) +print(flatten(nnf_formula, Or)) + +nnf_formula_2 = Var(10) +for i in range(11, 20): + nnf_formula_2 = nnf_formula_2 | Var(i) +nnf_formula_3 = nnf_formula | nnf_formula_2 +print() +print(nnf_formula_3) +print(flatten(nnf_formula_3, Or)) +""" + +#test nnf nesting - both and's and or's +print() +nnf_formula = Var(1) +for i in range(10): + nnf_formula = nnf_formula & (Var(i) | Var(i + 1)) +print(nnf_formula) +print() +print(flatten(nnf_formula, And)) \ No newline at end of file From 667a886d74c40bd4a99698d0d5348d718c1ca3ae Mon Sep 17 00:00:00 2001 From: beckydvn Date: Tue, 21 Sep 2021 16:33:28 -0400 Subject: [PATCH 06/18] add flatten to __all__ --- nnf/__init__.py | 1 + 1 file changed, 1 insertion(+) diff --git a/nnf/__init__.py b/nnf/__init__.py index 196276f..43aa88a 100644 --- a/nnf/__init__.py +++ b/nnf/__init__.py @@ -62,6 +62,7 @@ "tseitin", "operators", "pysat", + "flatten" ) From 98e22b1e3d8ae9a7bd1a5d8be282f8bde116c6e3 Mon Sep 17 00:00:00 2001 From: beckydvn Date: Tue, 21 Sep 2021 17:04:58 -0400 Subject: [PATCH 07/18] flatten add children bug fix --- nnf/__init__.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/nnf/__init__.py b/nnf/__init__.py index 43aa88a..9e65860 100644 --- a/nnf/__init__.py +++ b/nnf/__init__.py @@ -1744,7 +1744,7 @@ def flatten(nnf: NNF, operator_type: t.Union[And, Or]): elif type(c) == operator_type: set_and_children.update(c.children) else: - set_other.update(c) + set_other.add(c) nnf = operator_type(set_and_children | set_other) for c in nnf.children: @@ -1919,7 +1919,7 @@ def __call__(self, **settings: str) -> _ConfigContext: #test nnf nesting - both and's and or's print() nnf_formula = Var(1) -for i in range(10): +for i in range(3): nnf_formula = nnf_formula & (Var(i) | Var(i + 1)) print(nnf_formula) print() From 182dcd72a6e4d3dba0c1444222946e5006c1823e Mon Sep 17 00:00:00 2001 From: beckydvn Date: Tue, 21 Sep 2021 17:19:54 -0400 Subject: [PATCH 08/18] make operator type the type of the current nnf --- nnf/__init__.py | 40 ++++++++++++++++++++-------------------- 1 file changed, 20 insertions(+), 20 deletions(-) diff --git a/nnf/__init__.py b/nnf/__init__.py index 9e65860..3466788 100644 --- a/nnf/__init__.py +++ b/nnf/__init__.py @@ -1732,25 +1732,26 @@ def decision( """ return (var & if_true) | (~var & if_false) -def flatten(nnf: NNF, operator_type: t.Union[And, Or]): +def flatten(nnf: NNF): set_and_children = set() set_other = set() - if type(nnf) == operator_type: - for c in nnf.children: - if type(c) == Var: - set_and_children.add(c) - elif len(c.children) == 1: - set_and_children.update(c.children) - elif type(c) == operator_type: - set_and_children.update(c.children) - else: - set_other.add(c) - nnf = operator_type(set_and_children | set_other) + operator_type = type(nnf) + + for c in nnf.children: + if type(c) == Var: + set_and_children.add(c) + elif len(c.children) == 1: + set_and_children.update(c.children) + elif type(c) == operator_type: + set_and_children.update(c.children) + else: + set_other.add(c) + nnf = operator_type(set_and_children | set_other) - for c in nnf.children: - if type(c) == operator_type: - return flatten(nnf, operator_type) - return nnf + for c in nnf.children: + if type(c) == operator_type: + return flatten(nnf) + return nnf #: A node that's always true. Technically an And node without children. @@ -1918,9 +1919,8 @@ def __call__(self, **settings: str) -> _ConfigContext: #test nnf nesting - both and's and or's print() -nnf_formula = Var(1) -for i in range(3): - nnf_formula = nnf_formula & (Var(i) | Var(i + 1)) +p, q, r, s, u = Var("p"), Var("q"), Var("r"), Var("s"), Var("u") +nnf_formula = p | (((q | (u | ((p | s) & r)) & s))) print(nnf_formula) print() -print(flatten(nnf_formula, And)) \ No newline at end of file +print(flatten(nnf_formula)) \ No newline at end of file From 1009a3b07de1e6bc98d0bd3e8e7d2a1d09d09c71 Mon Sep 17 00:00:00 2001 From: beckydvn Date: Tue, 21 Sep 2021 17:27:21 -0400 Subject: [PATCH 09/18] remove extra testing --- nnf/__init__.py | 44 +------------------------------------------- 1 file changed, 1 insertion(+), 43 deletions(-) diff --git a/nnf/__init__.py b/nnf/__init__.py index 3466788..fb2fd5b 100644 --- a/nnf/__init__.py +++ b/nnf/__init__.py @@ -1881,46 +1881,4 @@ def __call__(self, **settings: str) -> _ConfigContext: config = _Config() -from nnf import amc, dsharp, kissat, operators, pysat, tseitin # noqa: E402 - -""" -# test nnf nesting - and -print() -nnf_formula = Var(1) -for i in range(10): - nnf_formula = nnf_formula & Var(i) -print(nnf_formula) -print(flatten(nnf_formula, And)) - -nnf_formula_2 = Var(10) -for i in range(11, 20): - nnf_formula_2 = nnf_formula_2 & Var(i) -nnf_formula_3 = nnf_formula & nnf_formula_2 -print() -print(nnf_formula_3) -print(flatten(nnf_formula_3, And)) - -# test nnf nesting - or -print() -nnf_formula = Var(1) -for i in range(10): - nnf_formula = nnf_formula | Var(i) -print(nnf_formula) -print(flatten(nnf_formula, Or)) - -nnf_formula_2 = Var(10) -for i in range(11, 20): - nnf_formula_2 = nnf_formula_2 | Var(i) -nnf_formula_3 = nnf_formula | nnf_formula_2 -print() -print(nnf_formula_3) -print(flatten(nnf_formula_3, Or)) -""" - -#test nnf nesting - both and's and or's -print() -p, q, r, s, u = Var("p"), Var("q"), Var("r"), Var("s"), Var("u") -nnf_formula = p | (((q | (u | ((p | s) & r)) & s))) -print(nnf_formula) -print() -print(flatten(nnf_formula)) \ No newline at end of file +from nnf import amc, dsharp, kissat, operators, pysat, tseitin # noqa: E402 \ No newline at end of file From 273ffbd5846557fc469155a496cc9857ec01b949 Mon Sep 17 00:00:00 2001 From: beckydvn Date: Tue, 21 Sep 2021 18:19:10 -0400 Subject: [PATCH 10/18] update children recursively, simplify algorithm --- nnf/__init__.py | 88 ++++++++++++++++++++++++++++++++++++++++--------- 1 file changed, 72 insertions(+), 16 deletions(-) diff --git a/nnf/__init__.py b/nnf/__init__.py index fb2fd5b..bc08956 100644 --- a/nnf/__init__.py +++ b/nnf/__init__.py @@ -1733,26 +1733,27 @@ def decision( return (var & if_true) | (~var & if_false) def flatten(nnf: NNF): - set_and_children = set() - set_other = set() - operator_type = type(nnf) + """Flattens a formula by removing unnecessary extra nestings. + param var: The formula to be flattened. + """ + new_children = set() + outer_operator = type(nnf) + # iterate through all children for c in nnf.children: if type(c) == Var: - set_and_children.add(c) + new_children.add(c) + # atoms don't need to be nested elif len(c.children) == 1: - set_and_children.update(c.children) - elif type(c) == operator_type: - set_and_children.update(c.children) + new_children.update(c.children) + # if the operator type is the same as the outer operator, flatten the formula + # and remove the nested operator by only taking the children (i.e. And(And()) or Or(Or())) + elif type(c) == outer_operator: + new_children.update(flatten(c).children) else: - set_other.add(c) - nnf = operator_type(set_and_children | set_other) - - for c in nnf.children: - if type(c) == operator_type: - return flatten(nnf) - return nnf - + # otherwise, continue to flatten the children but keep the operator (i.e. And(Or) or Or(And)) + new_children.add(flatten(c)) + return outer_operator(new_children) #: A node that's always true. Technically an And node without children. true = And() # type: And[Bottom] @@ -1881,4 +1882,59 @@ def __call__(self, **settings: str) -> _ConfigContext: config = _Config() -from nnf import amc, dsharp, kissat, operators, pysat, tseitin # noqa: E402 \ No newline at end of file +from nnf import amc, dsharp, kissat, operators, pysat, tseitin # noqa: E402 + +if __name__ == "__main__": + # test nnf nesting - and + nnf_formula = Var(1) + for i in range(10): + nnf_formula = nnf_formula & Var(i) + nnf_formula_2 = Var(10) + for i in range(11, 20): + nnf_formula_2 = nnf_formula_2 & Var(i) + nnf_formula_3 = nnf_formula & nnf_formula_2 + print() + print(nnf_formula) + print(nnf_formula_2) + print(nnf_formula_3) + print(flatten(nnf_formula_3)) + + # test nnf nesting - or + nnf_formula = Var(1) + for i in range(10): + nnf_formula = nnf_formula | Var(i) + nnf_formula_2 = Var(10) + for i in range(11, 20): + nnf_formula_2 = nnf_formula_2 | Var(i) + nnf_formula_3 = nnf_formula | nnf_formula_2 + print() + print(nnf_formula) + print(nnf_formula_2) + print(nnf_formula_3) + print(flatten(nnf_formula_3)) + + #test nnf nesting - both and's and or's + print() + nnf_formula = Var(1) + for i in range(10): + nnf_formula = nnf_formula & (Var(i) | Var(i + 1)) + print(nnf_formula) + print(flatten(nnf_formula)) + + print() + nnf_formula = Var(1) + for i in range(10): + nnf_formula = nnf_formula | (Var(i) & Var(i + 1)) + print(nnf_formula) + print(flatten(nnf_formula)) + + x, a, y, z, b, c = Var("x"), Var("a"), Var("y"), Var("z"), Var("b"), Var("c") + nnf_formula = x | ((a & y) & z & (b | c)) + print() + print(nnf_formula) + print(flatten(nnf_formula)) + + nnf_formula = x | (((a & ((y | ((x | z) & b)) & c)))) + print() + print(nnf_formula) + print(flatten(nnf_formula)) \ No newline at end of file From eafb02d3e16f9a3b76b407eb71a544b60445db39 Mon Sep 17 00:00:00 2001 From: beckydvn Date: Tue, 21 Sep 2021 18:53:06 -0400 Subject: [PATCH 11/18] clean up --- nnf/__init__.py | 70 +------------------------------------------------ 1 file changed, 1 insertion(+), 69 deletions(-) diff --git a/nnf/__init__.py b/nnf/__init__.py index bc08956..69a5e1a 100644 --- a/nnf/__init__.py +++ b/nnf/__init__.py @@ -92,23 +92,10 @@ class NNF(metaclass=abc.ABCMeta): def __and__(self: T_NNF, other: U_NNF) -> 'And[t.Union[T_NNF, U_NNF]]': """And({self, other})""" return And({self, other}) - # if not flatten: - # return And({self, other}) - # else: - # # optionally prevent unnecessary nesting - # if type(self) == And: - # return And({*self.children, *other.children}) if type(other) == And else And({*self.children, other}) - def __or__(self: T_NNF, other: U_NNF) -> 'Or[t.Union[T_NNF, U_NNF]]': """Or({self, other})""" return Or({self, other}) - # if not flatten: - # return Or({self, other}) - # else: - # # optionally prevent unnecessary nesting - # if type(self) == Or: - # return Or({*self.children, *other.children}) if type(other) == Or else Or({*self.children, other}) def __rshift__(self: T_NNF, other: U_NNF)-> 'Or[t.Union[T_NNF.negate(), U_NNF]]': """Or({self.negate(), other})""" @@ -1882,59 +1869,4 @@ def __call__(self, **settings: str) -> _ConfigContext: config = _Config() -from nnf import amc, dsharp, kissat, operators, pysat, tseitin # noqa: E402 - -if __name__ == "__main__": - # test nnf nesting - and - nnf_formula = Var(1) - for i in range(10): - nnf_formula = nnf_formula & Var(i) - nnf_formula_2 = Var(10) - for i in range(11, 20): - nnf_formula_2 = nnf_formula_2 & Var(i) - nnf_formula_3 = nnf_formula & nnf_formula_2 - print() - print(nnf_formula) - print(nnf_formula_2) - print(nnf_formula_3) - print(flatten(nnf_formula_3)) - - # test nnf nesting - or - nnf_formula = Var(1) - for i in range(10): - nnf_formula = nnf_formula | Var(i) - nnf_formula_2 = Var(10) - for i in range(11, 20): - nnf_formula_2 = nnf_formula_2 | Var(i) - nnf_formula_3 = nnf_formula | nnf_formula_2 - print() - print(nnf_formula) - print(nnf_formula_2) - print(nnf_formula_3) - print(flatten(nnf_formula_3)) - - #test nnf nesting - both and's and or's - print() - nnf_formula = Var(1) - for i in range(10): - nnf_formula = nnf_formula & (Var(i) | Var(i + 1)) - print(nnf_formula) - print(flatten(nnf_formula)) - - print() - nnf_formula = Var(1) - for i in range(10): - nnf_formula = nnf_formula | (Var(i) & Var(i + 1)) - print(nnf_formula) - print(flatten(nnf_formula)) - - x, a, y, z, b, c = Var("x"), Var("a"), Var("y"), Var("z"), Var("b"), Var("c") - nnf_formula = x | ((a & y) & z & (b | c)) - print() - print(nnf_formula) - print(flatten(nnf_formula)) - - nnf_formula = x | (((a & ((y | ((x | z) & b)) & c)))) - print() - print(nnf_formula) - print(flatten(nnf_formula)) \ No newline at end of file +from nnf import amc, dsharp, kissat, operators, pysat, tseitin # noqa: E402 \ No newline at end of file From 77b641a0b2fb5e9d551651669f4f3a1bf1088364 Mon Sep 17 00:00:00 2001 From: beckydvn Date: Wed, 22 Sep 2021 11:37:30 -0400 Subject: [PATCH 12/18] remove recursion so only 1 level is flattened --- nnf/__init__.py | 13 +++++-------- 1 file changed, 5 insertions(+), 8 deletions(-) diff --git a/nnf/__init__.py b/nnf/__init__.py index 69a5e1a..e1a594d 100644 --- a/nnf/__init__.py +++ b/nnf/__init__.py @@ -1719,8 +1719,8 @@ def decision( """ return (var & if_true) | (~var & if_false) -def flatten(nnf: NNF): - """Flattens a formula by removing unnecessary extra nestings. +def flatten_one_level(nnf: NNF): + """Flattens the first "level" of a formula by removing unnecessary extra nestings. param var: The formula to be flattened. """ @@ -1730,16 +1730,13 @@ def flatten(nnf: NNF): for c in nnf.children: if type(c) == Var: new_children.add(c) - # atoms don't need to be nested - elif len(c.children) == 1: - new_children.update(c.children) # if the operator type is the same as the outer operator, flatten the formula # and remove the nested operator by only taking the children (i.e. And(And()) or Or(Or())) elif type(c) == outer_operator: - new_children.update(flatten(c).children) + new_children.update(c.children) else: - # otherwise, continue to flatten the children but keep the operator (i.e. And(Or) or Or(And)) - new_children.add(flatten(c)) + # otherwise, keep the operator as is if it is a different type (i.e. And(Or) or Or(And)) + new_children.add(c) return outer_operator(new_children) #: A node that's always true. Technically an And node without children. From 627bcec9f70a46b62223a9fab3d552ffdcb43e2b Mon Sep 17 00:00:00 2001 From: beckydvn Date: Wed, 22 Sep 2021 11:44:57 -0400 Subject: [PATCH 13/18] add to imports --- nnf/__init__.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/nnf/__init__.py b/nnf/__init__.py index e1a594d..193612b 100644 --- a/nnf/__init__.py +++ b/nnf/__init__.py @@ -62,7 +62,7 @@ "tseitin", "operators", "pysat", - "flatten" + "flatten_one_level" ) From 40e203354a8a92db38f1f75e09349dba06c6f00f Mon Sep 17 00:00:00 2001 From: beckydvn Date: Wed, 22 Sep 2021 17:07:17 -0400 Subject: [PATCH 14/18] optionally remove nesting when operator is used --- nnf/__init__.py | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) diff --git a/nnf/__init__.py b/nnf/__init__.py index 193612b..373e7f0 100644 --- a/nnf/__init__.py +++ b/nnf/__init__.py @@ -84,17 +84,27 @@ 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]]': From ddcfe8ae5d34629e6a1ec063d51f0c5f4cbb3a0f Mon Sep 17 00:00:00 2001 From: beckydvn Date: Wed, 22 Sep 2021 17:38:40 -0400 Subject: [PATCH 15/18] remove old function --- nnf/__init__.py | 20 -------------------- 1 file changed, 20 deletions(-) diff --git a/nnf/__init__.py b/nnf/__init__.py index 373e7f0..877b4ae 100644 --- a/nnf/__init__.py +++ b/nnf/__init__.py @@ -1729,26 +1729,6 @@ def decision( """ return (var & if_true) | (~var & if_false) -def flatten_one_level(nnf: NNF): - """Flattens the first "level" of a formula by removing unnecessary extra nestings. - - param var: The formula to be flattened. - """ - new_children = set() - outer_operator = type(nnf) - # iterate through all children - for c in nnf.children: - if type(c) == Var: - new_children.add(c) - # if the operator type is the same as the outer operator, flatten the formula - # and remove the nested operator by only taking the children (i.e. And(And()) or Or(Or())) - elif type(c) == outer_operator: - new_children.update(c.children) - else: - # otherwise, keep the operator as is if it is a different type (i.e. And(Or) or Or(And)) - new_children.add(c) - return outer_operator(new_children) - #: 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. From 202efb78cc32a481487d56a6ce10c316551a8fa3 Mon Sep 17 00:00:00 2001 From: beckydvn Date: Mon, 27 Sep 2021 04:12:04 -0400 Subject: [PATCH 16/18] make requested changes --- nnf/__init__.py | 41 +++++++++++++++++-------- test_nnf.py | 81 +++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 110 insertions(+), 12 deletions(-) diff --git a/nnf/__init__.py b/nnf/__init__.py index 877b4ae..a729377 100644 --- a/nnf/__init__.py +++ b/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 #: `_. 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 \ No newline at end of file +from nnf import amc, dsharp, kissat, operators, pysat, tseitin # noqa: E402 diff --git a/test_nnf.py b/test_nnf.py index 11880a9..e5cb249 100644 --- a/test_nnf.py +++ b/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})}) From 8177ae29bbc1e116e3b541cec4750f0f8abb6bac Mon Sep 17 00:00:00 2001 From: Rebecca De Venezia <70995331+beckydvn@users.noreply.github.com> Date: Mon, 25 Oct 2021 09:32:45 -0400 Subject: [PATCH 17/18] Update test_nnf.py config settings Co-authored-by: Jan Verbeek --- test_nnf.py | 1 + 1 file changed, 1 insertion(+) diff --git a/test_nnf.py b/test_nnf.py index e5cb249..f1d4a9c 100644 --- a/test_nnf.py +++ b/test_nnf.py @@ -1107,6 +1107,7 @@ def test_models(sentence: nnf.NNF): 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") From ed3161103d6c934c7a8a87551a5af0497ce0828f Mon Sep 17 00:00:00 2001 From: beckydvn Date: Sat, 23 Oct 2021 02:45:22 -0400 Subject: [PATCH 18/18] fix flake8 --- nnf/__init__.py | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/nnf/__init__.py b/nnf/__init__.py index a729377..0c1e3a9 100644 --- a/nnf/__init__.py +++ b/nnf/__init__.py @@ -14,7 +14,6 @@ __version__ = '0.2.1' -from _typeshed import IdentityFunction import abc import functools import itertools @@ -84,8 +83,6 @@ 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.""" @@ -115,7 +112,7 @@ def __or__(self: T_NNF, other: U_NNF) -> 'Or[t.Union[T_NNF, U_NNF]]': return Or({*self.children, *other.children}) return Or({self, other}) - def __rshift__(self, other: 'NNF')-> 'Or[NNF]': + def __rshift__(self, other: 'NNF') -> 'Or[NNF]': """Or({self.negate(), other})""" return Or({self.negate(), other}) @@ -1737,6 +1734,7 @@ 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.