Performs functional_reduction on the miter before converting into CNF to reduce the size. It is now (hopefully) a little bit more usable. (For example, using aig_resubstitution with max_inserts=1 as the optimization script and using a conflict limit of 100K, about half of the EPFL benchmarks can be solved within seconds --- div, hyp, log2, multiplier, sin, sqrt, and square timed-out). (Currently skipped for klut_network because functional_reduction needs to be adapted)
Improves functional_reduction by (1) re-seed with random patterns when exceeding a certain amount and (2) add a parameter to run for up to a certain iterations or until saturation.
functional_reductionon the miter before converting into CNF to reduce the size. It is now (hopefully) a little bit more usable. (For example, usingaig_resubstitutionwithmax_inserts=1as the optimization script and using a conflict limit of 100K, about half of the EPFL benchmarks can be solved within seconds --- div, hyp, log2, multiplier, sin, sqrt, and square timed-out). (Currently skipped forklut_networkbecausefunctional_reductionneeds to be adapted)functional_reductionby (1) re-seed with random patterns when exceeding a certain amount and (2) add a parameter to run for up to a certain iterations or until saturation.clonetoklut_networkpercy