Skip to content

Commit

Permalink
small bug
Browse files Browse the repository at this point in the history
  • Loading branch information
Guillermo A. Perez committed Apr 29, 2015
1 parent 75487d0 commit 079f163
Showing 1 changed file with 10 additions and 2 deletions.
12 changes: 10 additions & 2 deletions comp_algos.py
Original file line number Diff line number Diff line change
Expand Up @@ -43,18 +43,26 @@ def merge_some_signals(cube, C, aig, argv):
dep_map = dict()
for c in C:
deps = frozenset(cube_deps | aig.get_lit_deps(c))
log.DBG_MSG("Current deps: " + str(deps))
found = False
for key in dep_map:
if key >= deps:
log.DBG_MSG("Some key subsumes deps")
dep_map[key] &= aig.lit2bdd(c)
found = True
break
elif key <= deps:
dep_map[deps] = dep_map[key] & aig.lit2bdd(c)
log.DBG_MSG("New deps subsumes some key")
if deps in dep_map:
log.DBG_MSG("AND... the deps existed already")
dep_map[deps] &= dep_map[key] & aig.lit2bdd(c)
else:
dep_map[deps] = dep_map[key] & aig.lit2bdd(c)
del dep_map[key]
found = True
break
if not found:
log.DBG_MSG("Adding a new dict element")
dep_map[deps] = aig.lit2bdd(c)
log.LOG_MSG(str(len(dep_map.keys())) + " sub-games after incl. red.")
for key in dep_map:
Expand Down Expand Up @@ -91,7 +99,7 @@ def decompose(aig, argv):
rem_AND_leaves = filter(lambda x: strip_lit(x) != b, A)
rdeps = set()
for r in rem_AND_leaves:
rdeps |= aig.get_lit_latch_deps(strip_lit(r))
rdeps |= aig.get_lit_deps(strip_lit(r))
log.DBG_MSG("Rem. AND leaves' deps: " + str(rdeps))
cube = BDD.make_cube(map(aig.lit2bdd, rem_AND_leaves))
log.DBG_MSG(str(len(C)) + " OR leaves: " +
Expand Down

0 comments on commit 079f163

Please sign in to comment.