Following the TLA+ proof syntax PICK x: P(x). A method pick has been added in a2dfd2a4108da8fdaab2e39465bb271554ef3e5d, following the example of omega.symbolic.fol.Context.pick, which includes a method pick_iter. The pick method is only a convenience wrapper around pick_iter.
Motivation:
"pick" is a verb, so compliance to standard practice (use verbs for functions/methods that modify program state)
"sat" is not a word
sat_iter isn't readable
sat_iter contains an underscore
"pick" emphasizes the operation's metatheoretic nature, reminding that the returned entity is an assignment as dict, not a BDD (syntactic entity)
Following the TLA+ proof syntax
PICK x: P(x). A methodpickhas been added in a2dfd2a4108da8fdaab2e39465bb271554ef3e5d, following the example ofomega.symbolic.fol.Context.pick, which includes a methodpick_iter. Thepickmethod is only a convenience wrapper aroundpick_iter.Motivation:
sat_iterisn't readablesat_itercontains an underscoredict, not a BDD (syntactic entity)Cudd_bddPickOneCubeandCudd_bddPickOneMinterm.