Simpler formula produced after second simplification round

[tomas789]

In my sample code I have a formula which after call to .simplify() produces a correct formula. When calling .simplify() second times we get an even simpler result. This might be considered for future improvements.

Also note that the formula given is not a minimal example.

import boolean

algebra = boolean.BooleanAlgebra()
TRUE, FALSE, NOT, AND, OR, symbol = algebra.definition()

x = algebra.parse("""
(~((~((0)|x3|(1)))&((x8&x8)|(x0|(0)|x2|x0|x6))&(x2&((1)&(0)&x5)&(1))&(~(x3|x7|x1|x10|(0)))&(1)))&(~((x6&(x4&x2)&~x7&~x9&(x3|(0)))&((x6&x9&x8)|x7)))&((~(~x10|~x7|x2|~x8))|(~(~x5&~x10))|(~x4&x6&(~((1)|x8|(1)))&((x4|x8|x9|(1)|(0))|x7|(x7&x2))&(0))|((0)|((x2|(0))&(x2&x2&x9&x0)&(x6&x4&x3&(0))&(x6&x7&(0))&(x9|x0|(0)|(0)|x10))|(x6|(~(0))|(x6&(1)&x3&x0&(1)))))
""".strip())
x1 = x.simplify()
x2 = x1.simplify()
print(x)
print(x1)
print(x2)

The snippet produces following output

(~((~((0)|x3|(1)))&((x8&x8)|(x0|(0)|x2|x0|x6))&(x2&((1)&(0)&x5)&(1))&(~(x3|x7|x1|x10|(0)))&(1)))&(~((x6&(x4&x2)&~x7&~x9&(x3|(0)))&((x6&x9&x8)|x7)))&((~(~x10|~x7|x2|~x8))|(~(~x5&~x10))|(~x4&x6&(~((1)|x8|(1)))&((x4|x8|x9|(1)|(0))|x7|(x7&x2))&(0))|((0)|((x2|(0))&(x2&x2&x9&x0)&(x6&x4&x3&(0))&(x6&x7&(0))&(x9|x0|(0)|(0)|x10))|(x6|(~(0))|(x6&(1)&x3&x0&(1)))))
~x2|~x3|~x4|~x6|x7|x9|(~x6|~x8|~x9)
1

[tomas789]

Here is another example. Not all the operands were merged into a single operation.

(~((((1)&x2&x2&x1&x10)|~x2)&x2&((x2|x0|x8)&((0)|(1)|x7|x9|x2)&x2&~x9)&((x6|(1)|(0))|x10|x7|(x10|(1)|x4|x10)|(x6&(0)&(1)&x4&(0)))))&(((~(x10&x1&(0)&x9&x8))|((x4|(0)|x3|x0|(1))&(x9|(1)|x1|(1)|x6)&((0)&(0)))|((x8|(0)|(1)|x8)&((1)|x10|x5)&(x10|x6|(1)|x2|x9)&(x0|x1|x7)&x3))&((~x3|(x6&x0&(0)&x6&x10)|~x6|x1|(x6|x4))|x3)&(((x4&x7&x2&x5&(0))|(x7|x6)|x2)|x9|(1)|(1)|((x4|x5|x1|(0)|(1))&(x3&x7&x4)&(x3&(0)&x7&x3&x9)&((1)&(0)&(1)&x9&x2)&(x8&(0)&x5))))
~x2|x9|(~x1|~x10)
~x1|~x10|~x2|x9

[tomas789]

I will just list a few examples falling into the same category of not being the same after two consecutive simplifications.

(((x9|~x2|(x6|x0|x1|(0)|x9)|((1)|x9|x8)|~x2)|(x5&(~(1)))|(~(~x0))|((x5&x2&(0)&x6&(1))|(x9&x4))|((x10|x0)&((1)|x2)&(~(0))))&x2&((~(~x9))&x7&(((0)|x1|x0|x9)|(0)|(~(1))|(0)|(x9&(0)))&(0))&((((0)|(1)|(0))|((0)|x9|x5|x7)|~x3|(x0&(0)&(1)&(0)))&~x8&(x10|(x8&x1)|(x1&(1)&x6&(0))|(x6|x6)|(0))&(x8|((0)&(0)&(1)&x0)|x4|(x1&x9))&((x3&x7)|x2|(x8&x4&(0)&(0)&x10)))&((~(x5&x8&x7))|((x8|(0)|x3)|(x2|(0))|(x6&x7&x10&x1&x2))))|(~((~x10&(x7|x5)&(x2|x8|(1)|x4))|((x2|x3|(0)|x10|x4)|(x0|x7|x9|x3|x10)|(x5&x5&x5)|x0)|x4|(((0)&(0)&x6)&~x4&(x5&x4)&(1))))
~x0&~x10&~x2&~x3&~x4&~x5&~x7&~x9&(~x5&~x7)
~x0&~x10&~x2&~x3&~x4&~x5&~x7&~x9

(~((((1)&x3&x10)|(x4&x0&(1)&(0)&x2)|~x0)&((x6&(0)&x1)&((1)|x9|x4|x6|(1)))&(~(~x4))&(1)))&(~((~x3&(~(0))&(x10&x9)&((0)|x6|(0)|x2|x10)&(x9|x7|(0)|x0))&(x9|~x0|(x0|x1|(1)))&(~(~(1)))&(~x4|(x4&x1))&(~(x4|(0)|x3|(0)|x1))))
x1|~x10|x3|x4|x4|~x9
x1|~x10|x3|x4|~x9

(x7|(((x2|x5|x5|x8|x9)|~x7|(x6|(0)|x8|x6|x4))&((~(0))|((0)|x1|(1))|((0)&x9&(0)&x10&x5)|((1)|x5|(0)|x7|x5))&(((1)|(0))&(x8&x5&x10&(1))&~x6)&~x4)|((x8|~x10)|((x1&x6&x0)|((0)&x5&(0)))|(~x6|(x8&x9&(1)&(1)&x2)|~x2|~x6|x8)|((~(1))|(x10&(0)&x2&(1))|(~(1))|~x10)|(~x9|(x5&x10&x7&(0)&(1))))|(x4|(~(~x9))))&(~(((x7&x4&x3&x0)|~x3|x0)&((x6&x3&x1)|(x6&(0)&x4))&(~x9&(x10&x2)&~x8&((1)|x6|x1|x3|(1))&(x4|x0))))
~x0|~x1|~x10|~x2|~x3|~x6|x8|x9|(~x0&~x4)
~x0|~x1|~x10|~x2|~x3|~x6|x8|x9

(((((0)&x5&x4&(0))|(x2&x9&x3)|((0)|(1)|(1)|(1)|x4))&(((1)|(1)|x10|(1))&(x7&x3))&((x4|x2)&~x3)&(~(x9|x2|x10|x4))&(~x0|~x0|(x5|x0)))|((((1)&x6)|~x8|(x5&(0)&x9&x7&x6)|((0)&x7&x10)|~x9)|((x5|(0)|(1)|(0))|~x0)|((x10&x1&(1)&x0&(0))|~x8|x9|x3)|(x1&((0)|x3))|(~x7|(~(0))|~x9))|(((x3|x3)|(x5|x1|x0|x3))|(((0)|x2|x10|(0)|(0))|(x0|(0)|x5|x3|x5)|x6|~x0|~x1))|(~(~((1)|x2|x1))))&(~(x2&(((0)|x1|x9|x1)&((0)|(1)|x10|x4)&(x9|(1)|x6|x0|(1)))&(~((1)&x6&x2&x2))&(~(~x6))))
~x2|~x6|x6|(~x1&~x9)
1

(~(~((x1|(1)|x8)&x3&(x1&x6&x0&(0))&(x10&x5&(0)&x6&x0)&(~(0)))))|(~(((x7&x3)&(~(0))&((0)|(0)|x6))|(~(x3&x6&x7&x1))|(~(x9|(1)|(1)|x7))))|(((((0)|(1)|(0))&(x3&x7&x7)&(x6&x5&(0))&(x8|(1)|(0)|(0))&(1))&((x0|(0)|x2|x6)|(x5|x9|(0)|(0)|x2))&(~((0)|x9|x2|x5))&(((0)|x1|(0)|x6|x10)&(x9|(0)|(1))))&(((~(0))&(~(1))&((0)&(0)&(1)&(0))&(x0&x2)&~x0)&x5&x5)&((~(x7&(1)&(0)))&(x4|(x10&x5&x7&x4&x7))&(((0)|(1)|(0)|(1))|(x5|x4|x3|x5|(0))|(x2|x6|x10|(0)|x2))&((x10&x2)|~x3|(x3|(0)|x1)|((0)|x1|x9|x3))))
x1&x3&x6&~x7&x7
0

(~(1))|((x5&(~((1)|(1)|x0|x1|x3))&((1)|x0|(1)|x4)&x6)&((((1)&(0)&x2&x2)|(x0|x10))|(x6|(x0|(0))|~x1|(x9&x6&x6&x9&(1)))|x9)&(~x4|(~(x6|(1))))&(((~(0))|((1)&x8))|(~(1)))&(((x1|x8|x8)&(x10&(0))&x1&x10)&(~(x1|(0)|x7|x6|(0)))))|(0)|(~(((x10|(1)|x9)&~x6&~x6&(~(0)))|((x6&x6&(1)&x8&(1))|x5|(x3&x4&x2&x1))|~x4|((x9|x7|(1))&(x1&x5&(0)))|(~((1)&(1)&x8))))
x4&~x5&x6&~x8&x8&(~x1|~x2|~x3)
0

((((x6&(1)&(0)&x8&x3)|(x3|(0)))&(((0)|(1)|x3|(1))&(x6&(0)&x6&(0))&(~(1)))&(~((0)|(0)))&(~(x2|(1)|x4|x7|x10))&(~x1|~x3))|((0)|((x0|x5|x10)|x0)|((~(0))&(x7|(1)|x8|x9|x4)&(x9&x9&(0)&x8)&x8&(x8&x1&x1))|(~((0)&x5&(0)&(1)&x4)))|(x0|(((0)&x9)&(x6&x7&(1)&x1&(0))&(x6&x5&(1))&((0)|x1|x2|x5))|((x9&(1)&x7)&((0)&(0)&x4&x2)&(1))|(((0)&x8&x6)&~x2&x10)|(x10|(x2|x2|x5|x1|x0)|((1)&(0)&x2))))&(~(x8&(~x7|(x3&x7)|(x2|(0)|(0)|x3|x2)|~x9)))&(x2|(~(((0)&x3&(0))&x2))|x10)
~x8|(~x2&~x3&~x3&x7&x9)
~x8|(~x2&~x3&x7&x9)

(x5|(x10|(((1)|x9|(1)|(1))|((0)&(0)&(1)&x0)|((0)&(0)))|(x8|((0)|(0)|x2|(1))|~x10|(~(1)))|(((0)|(0))|(x3|(0)|x5|x8)|(x4|(0))|((1)&x10&(0)&(1))|(~(1)))|(((0)|(1)|x9)|~x0|~x8|(x2|x5)))|((~(~x10))|(~(x5&x10))|(~(x3&x4&x5&x0&x5)))|((((0)|(0)|x2)&(x0&(1)&(1))&(~(1))&((0)|x4|x10|x7))|(~(x1|x0))|(((0)|x2)|x2|(x9|x10|(0))|(~(0))|(x0&(1)&(0)&x2&x3))|(~((1)&x0))|(0))|((~(x5&x8))&x7&(1)&(~(x3|(1)|x0|(1)))))&(x3|(((~(1))&((0)&x5&x1)&((1)|x6|x3|x6))|((x2|x7|(1))|(x3|(0))|~x10))|(0)|(~(~((0)|x10|(0)|x7|(0))))|((((1)|x7|x10|(1))|(x5|x5|x5|(0)))|~x2|(x9|(~(1))|(1)|(0)|(x9&x7&x7&(0)))|((x6&x0&x4&x3&(1))&~x4&(x3|(1)|x4|x8|x7))))&(((((1)|(1)|x7|(0))&~x1)&(~(x9|x3|x8))&(0)&((x6|x2|x1|(0))|(x0&x10&x8)|((1)|(1)|(0)|x9)|(~(0)))&((x6&x1&x9&x6)|(1)))|((~x9&x9&(x0&x0))|((x0|x7|x6|(1)|(0))|(x3|x2|x3|x2)|(0))|x8|((x4&x3&x1&x4&x9)&(x7|x7)&(x9&x9&(0)&x5&x3)&x4&(0)))|((((1)&(1)&x3&(1)&(0))&x8&(x1|(1)))|(x3|(0)))|((~(~(0)))&x10&(((1)|x0|x0|x9)&(1)&(x2|x7|(0)|(0)|x5)&((1)|x0))&((x3|x8|x6|(1)|(1))&(x0&x3)&(x9|x5|x5|x6|x4))&(~x1|(~(0))|((0)&(1)&x0&x4&x7)|(x0|x7|(1)|(1)|x7)))|((~((1)&x2))|(~x7|((1)&x3&(1))|(x0|x4|(1))|(0)|x2)))&(~(((x7&x8)&x1&x1&(x4|x1)&(x2&(1)))&(~(x7&x5))&((x1|(0)|x8|x2|x7)&(x0&x2&x6&x5)&(x9|(0)|x0|(0)|x5)&(~(0)))))
~x0|~x1|~x2|~x5|x5|~x6|~x7|~x8
1

((~((x0&(0))|(~(1))|x7|((1)&x0&(1)&(0)&x7)))&(((x4&(1))|((1)|x5|(0)|x1|x3)|(x9|(1)|(0)|x7)|(x1&x8&(1))|(~(0)))|(~x3|(x0&x2&x3&(1)&(0))|~x6|~x7))&((~(x9|x0|(0)|x6))&(((1)|(1)|x1|x2|x2)&((0)&x2)&((0)&(0)&(1)&x7&(1))))&(~(1)))|((~((x5&x7&(1)&x1)|(x4|x8)|(1)|(x3|x10|x2|x2)|((1)|(0)|x9|x8|(1))))&(~((x8&x10&x0&x5)|(x10|x1|x2|x1|(1))|x7|(1)))&((x10&(x5&x1&(1)))&~x6&(~x2&(x10&(0)&x1))&x10&(~((1)|x8|x10|x5)))&(~(((1)&x10&x6&x4)&(x10&x0&x10)&(x6|(0)|(1)|x3)&x5)))|(~(~(x4&(x2&x0&(0)))))|(~((~(x9|x7))|((~(1))&~x4&~x4&~x2&(x8|x3|x0|x7|x10))|(x9|~x6|(x4&(1)&x5)|(x8&(1)&x10&x7)|x1)))
~x1&x6&x7&~x9&(~x10|~x7|~x8)&(~x4|~x5)
~x1&x6&x7&~x9&(~x10|~x8)&(~x4|~x5)