better handling of silly histories in sat_minimize()
Currently if the acceptance is Fin(0)&Inf(1)
the SAT-minimization code detects that any history containing 0
is rejecting and cannot be augmented into an accepting history. Hence it removes 1
from any history where 0
is present.
The code generalizes this example from the DNF of the acceptance. However we should at least also implement the dual version and simplify histories that are accepting and cannot be augmented into a rejecting history. For instance if the acceptance is Fin(0)|Inf(1)
, we do not need to distinguish between history {0,1}
and history {1}
.
I suspect that doing both might help the case of parity acceptance, where the only histories that matter have at most 1 element (the min or max seen so far).