search

reactive-systems / syfco

Synthesis Format Conversion Tool
MIT License
23 stars 12 forks source link

Negation normal form rewrites equivalence to top-level and #32

Closed meyerphi closed 5 months ago

meyerphi commented 4 years ago

I propose that the negation normal form rewrite rules rewrite equivalences x ↔ y as (¬x ∨ y)∧(x ∨ ¬y) instead of the previous (x ∧ y)∨(¬x ∧ ¬y). They are semantically equivalent, but the former allows the changes proposed in #30 and #31 to split more specifications with top-level equivalences, if combined with the -nnf option.

kleinreact commented 4 years ago

Although they are semantically equivalent, this change will affect the generated output of potentially many input instances, making future benchmark evaluations less comparable to previous ones. I instead suggest to add a flag that allows to choose the desired change and keeping the default as it is.

There is the issue anyway that changes on the Boolean level cannot be controled as well as on the temporal level at the moment. Hence, this may be a good opportunity to introduce support for such controls accordingly.

meyerphi commented 4 years ago

I agree, a flag would be the better option. If you want to implement that together with other options (I'm not sure which other changes on the Boolean level should be controllable), you can close this PR. Otherwise I can keep it open and implement a flag for the NNF toggle (when I get to it, don't have time right now).