可以忽略这篇，我直接再回一篇。
作者: 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)