可以忽略這篇，我直接再回一篇。
作者: ric2k1 (Ric) 看板: EE_DSnP
標題: Re: [問題] fraig
時間: Sun Jan 15 17:13:42 2012
※ 引述《djshen (djshen)》之銘言：
: 在sim05中
: fraig會用0來merge其他gate
: 但是像
: aag 4 1 0 1 3
: 8
: 6
: 2 0 8
: 4 0 8
: 6 2 4
: cirsim -r
: cirp -fec
: 1 2 3會在一起
: 但fraig沒有作用
: 不太懂到底要不要處理用0 merge的情況
造成這樣的結果是：
在 SAT engine 裏頭 positive phase 的 litID = varID * 2,
negative phase 的 litId = varId * 2 + 1,
但是在我們的 cirMgr 裏頭 constant gate 只有存 const0,
而他的 SAT var ID = 0.
不過根據 SAT engine 的定義，const 0 應屬於 negative phase,
也就是說它的 lit ID 應該是 1, 而不是 0.
不過由於在我們的 cirMgr 裏頭當一個 aig gate 有一個 const 0 的 fanin 的時候，
他的 inv phase 是 positive 的，<== 正好與 SAT 的定義相反!!
簡單的解決辦法是我們的 cir Mgr 應該存的 const gate 應該是 const 1,
而非 const 0. 不過這樣又會和 aag 的 format 有點衝突，
而且在這個節骨眼要改這個定義恐怕影響太大了。
所以解決的辦法是請你在建立 proof model 時，
如果 fanin 是 const gate, 記得呼叫 solver.addAigCNF() 時要把 invPhase反過來
當然比較消極的解決方式是我們在測 CIRFriag 時 一定都會先呼叫 CIROPT,
這樣可以確定 const gate 不會出現在 dfsList 裏頭，也就不會有這樣的問題了!
ref prog 晚一點再來上傳!
--
※ 發信站: 批踢踢實業坊(ptt.cc)
◆ From: 114.36.61.155
1F：推 kickpp:推~ 原來如此 01/15 17:20
2F：推 wmin0:不是只要證之前先assumeProperty(constGate->getVar(), 0); 01/15 17:39
3F：→ wmin0:就可以了嗎@@ 01/15 17:39
4F：→ ric2k1:樓上說的是解決的辦法，但不是這樣加的... 01/15 18:14
5F：→ ric2k1:==> 第二個參數應該是 true, 而非 0 01/15 18:15
6F：→ ric2k1:一個比較根治的辦法是: (1) 在 SatSolver::init() 最後面 01/15 18:16
7F：→ ric2k1:加上 _assump.push(Lit(0)); 01/15 18:16
8F：→ ric2k1:(2) 在 SatSolver::assumpRelease() 最後面也加上 01/15 18:17
9F：→ ric2k1:_assump.push(Lit(0)); 01/15 18:17
10F：→ ric2k1:我等一下吃完飯再來解釋... 01/15 18:17
11F：→ wmin0:不理解...因為我這樣做可以work... 01/15 19:07
12F：→ kickpp:這篇是report上一篇的情況喔 去看看原文 01/15 19:22
13F：→ wmin0:仍然不理解...因為我這樣做可以merge 0囧" 01/15 19:42
14F：→ ric2k1:了解樓上的意思了。基本上你把 const 0 當成是一個獨立的 01/15 19:50
15F：→ ric2k1:變數，的確是可以 work. 01/15 19:51
※ 編輯: ric2k1 來自: 114.36.61.155 (01/15 19:52)
※ 編輯: ric2k1 來自: 114.36.61.155 (01/15 20:21)