Marcelina Kościelnicka d25b9088c8 Refactor common parts of SAT-using optimizations into a helper. ...

This also aligns the functionality:

- in all cases, the onehot attribute is used to create appropriate
  constraints (previously, opt_dff didn't do it at all, and share
  created one-hot constraints based on $pmux presence alone, which
  is unsound)
- in all cases, shift and mul/div/pow cells are now skipped when
  importing the SAT problem (previously only memory_share did this)
  — this avoids creating clauses for hard cells that are unlikely
  to help with proving the UNSATness needed for optimization

2021-08-09 16:54:35 +02:00

14 KiB

Raw Blame History

View Raw