"ummmm. excellent question. idk." <- okay, so according to the smt code: - first compute, for each pattern, disregarding priorities, whether the pattern matches: - if all choices of values for the X would match the pattern, this is 1 - if all choices of values for the X would reject the pattern, this is 0 - otherwise, this is X - now, for each case, do a trit-level OR of the signals for each alternative pattern of this case - now, take priorities into account. iterating over the cases in order: - if the signal computed for this case in the previous step is 1, output onehot as appropriate. whether there's Xs for any later patterns doesn't matter - if the signal is 0, continue with the next pattern - if the signal is X, all further outputs of the match cell are X - at the very end, mux(enable, , all_zeros)