Skip to content

Commit

Permalink
BUG: exhaust the enumeration in fol.Context.pick_iter
Browse files Browse the repository at this point in the history
Only one value of the generator was consumed, instead of
the entire enumeration. This affected only calls without
`care_vars`, which anyway raised an `AssertionError` in
`dd < 0.5.0`, because `care_vars` was replaced with an empty
set, and `BDD.sat_iter` interpreted `care_bits` as a constraint.

In other words, this error in enumeration matters only for
bits that aren't enumerated exhaustively by `sat_iter`.
A call with `care_vars` had to include the entire support,
and each integer results in all its bits being included in
`care_bits`, so there weren't any bits not exhaustively enumerated.

Trying to omit integers in support from `care_vars` resulted
in errors in `sat_iter`. This behavior will change in
`omega == 0.1.0`, so this incorrect enumeration would
become observable, if left uncorrected.
  • Loading branch information
johnyf committed Feb 13, 2017
1 parent 766d3bd commit fa37694
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions omega/symbolic/fol.py
Original file line number Diff line number Diff line change
Expand Up @@ -171,9 +171,9 @@ def pick_iter(self, u, full, care_vars):
care_bits = set()
for bit_assignment in self.bdd.sat_iter(
u, full=full, care_bits=care_bits):
d = next(enum._bitfields_to_int_iter(
bit_assignment, self.vars))
yield d
for d in enum._bitfields_to_int_iter(
bit_assignment, self.vars):
yield d

def add_expr(self, e):
"""Add first-order predicate.
Expand Down

0 comments on commit fa37694

Please sign in to comment.