推 justmyself:thx~~~ 01/17 00:14
※ 引述《justmyself (hsin)》之銘言：
: 請問一下喔
: 那個BDD長的格式都一樣嗎?
: 意思是：
: XOR
: ----。 ----
: ─。○ ○ (1)
: ── ──
: 還是說，一定要變成這樣
: ---- ----。
: ─ ○ ○ (1)
: ──。 ──
: 謝謝~
(躺下來的 BDD 很可愛 ~~~ XD)
請參見講義 Ch-13 page 28 ---
===============================================
* What’s the problem?
* (v, Fv, Fv) and (v, Fv, Fv) will have different hash key and thus hash to
different nodes
阴=> While using complement edges, they should point to the same node!!
* Solution
* The “Then” child should NOT have bubble
阴=> If happens, apply the rules above
===============================================
就 BddManager::ite() 而言 妳應該移動一下 bubble before checking the unique
table... ==> Make sure 所有的 BddNodeInt 的 left (then) child 都沒有 bubble!
--
※ 發信站: 批踢踢實業坊(ptt.cc)
◆ From: 140.112.21.240