move 'ands'/'ors' into Formula module
use optimizing ops for fromCNF
unwind latches explicitly, partition differently
remove k parameter from 'rewind'
add test cases