aboutsummaryrefslogtreecommitdiffstats
path: root/kernel/qcsat.h
Commit message (Collapse)AuthorAgeFilesLines
* Refactor common parts of SAT-using optimizations into a helper.Marcelina Kościelnicka2021-08-091-0/+76
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