SymbolicBHV.synth or simplify sometimes gives the wrong Boolean form

[ethol]

For some ECA rules https://github.com/Adam-Vandervorst/PyBHV/blob/2f41a186f03caf0525331da66a4a8b40586c64d3/examples/ca_rules.py#L9-L10 Results in the wrong formula

Rule 90 works, but many other rules do not work like 30, 110 or 204 as examples.

Trivial example Rule 204: (~center), but should be just (center) examples Boolean form

less trivial example Rule 30: (left ^ (center & right)) but (i think) should be (left ^ ( center | right)) examples Boolean form

[Adam-Vandervorst]

Thanks for noticing! Luckily, this was not an error with the synth or simplify but with calculating the mask (wrong endianness). You can always check the correctness of a synthesized or processed formula that doesn't include permute with

print(mask)
print(formula.truth_assignments([Var("left"), Var("center"), Var("right")]))

Fixed in a4eddc8098819372e446306d6279737e334fd980

[ethol]

Thanks for responding so fast. That indeed fixed the rules mentioned but sadly there are some that still have issues, such as rule 150 or rule 122 (maybe more)

Rule 150 as an example translate correctly back(via formula.truth_assignments) to the same mask but sadly the formula does seem slightly off left.select((center ^ (~right)), (center ^ right)) vs left ^ center ^ right (atlas) Rule 150: should be http://atlas.wolfram.com/01/01/150/01_01_103_150.gif

[Adam-Vandervorst]

Interesting. Seems to be an issue with the roll. What point did you use? For now, you can use the latest (already patched) version, 0.8.6, with the updated example.

[Adam-Vandervorst]

left.select((center ^ (~right)), (center ^ right)) is equivalent to left ^ center ^ right, but less pretty.

I opened a ticket for using the smallest/prettiest form https://github.com/Adam-Vandervorst/PyBHV/issues/14 which you may like to subscribe to @ethol.

In case you're interested (or don't believe the truth assignments function), you can expand the select into binary operations: formula.simplify(expand_select_xor=True) and then enter that in Wolfram, which gives us the ANF we were looking for.

[ethol]

I was on vanilla on the 0e73cbb1627fb1cef8684c3846f0b2613c1d8b5b commit as the latest, after the newest commit 1beff1f80e0a988470dd510a14ba33a2a77c81c7 this seems resolved. Though now all the images are mirrored in standard form eg example 30. thats not a major issue though, as they are equivalent under trivial transformation Trivial transformation equivivalent

[Adam-Vandervorst]

I had the roll_bits wrong, which caused it to roll the other way. This is fixed in 0.8.7, but it raised a few other warts and uncovered some opportunities for faster execution and synthesis. Thanks for your involvement!