implement method `dd.sylvan.BDD.pick_iter`

[glarange]

Hi Johnny,

I was able to use pick.iter in dd.cudd but not in the dd.sylvan. Any suggestions would be much appreciated. Thanks again! Gui

[johnyf]

The method dd.sylvan.BDD.pick_iter has not been implemented as of f9aa4d1. The exception NotImplementedError is documented here.

dd/dd/sylvan.pyx

Lines 293 to 296 in f9aa4d1

	def pick_iter(self, Function u,
	full=False, care_vars=None):
	"""Return generator over assignments."""
	raise NotImplementedError

An implementation would be similar to dd.cudd.BDD.pick_iter:

dd/dd/cudd.pyx

Lines 906 to 946 in f9aa4d1

	def pick_iter(self, Function u, care_vars=None):
	assert self.manager == u.manager
	support = self.support(u)
	if care_vars is None:
	care_vars = support
	missing = {v for v in support if v not in care_vars}
	if missing:
	logger.warning((
	'Missing bits: '
	'support - care_vars = {missing}').format(
	missing=missing))
	cube = dict()
	value = True
	config = self.configure(reordering=False)
	for cube in self._sat_iter(u, cube, value, support):
	for m in _bdd._enumerate_minterms(cube, care_vars):
	yield m
	self.configure(reordering=config['reordering'])
	def _sat_iter(self, u, cube, value, support):
	"""Recurse to enumerate models."""
	if u.negated:
	value = not value
	# terminal ?
	if u.var is None:
	if value:
	assert set(cube).issubset(support), set(
	cube).difference(support)
	yield cube
	return
	# non-terminal
	i, v, w = self.succ(u)
	var = self.var_at_level(i)
	d0 = dict(cube)
	d0[var] = False
	d1 = dict(cube)
	d1[var] = True
	for x in self._sat_iter(v, d0, value, support):
	yield x
	for x in self._sat_iter(w, d1, value, support):
	yield x

taking into account how sylvan_low works:

dd/dd/sylvan.pyx

Line 557 in f9aa4d1

# propagates complement bit

[johnyf]

Addressed in c3d6919.