跑cirfraig的时候,ref最后面都会有一行Updating by SAT... Total #FEC Group = 0
我原本以为是把SAT的pattern蒐集起来,再simulate一遍,但结果跟我想的不一样?譬如
说:
(my.aag)
aag 9 2 0 2 2
2
4
6
8
6 3 5
8 7 2
(my.pattern)
11
(执行结果)
fraig> cirr my.aag
fraig> cirsim -f my.pattern
Total #FEC Group = 1
1 patterns simulated.
fraig> cirg 1
==================================================
= PI(1), line 2 =
= FECs: =
= Value: 0000_0000_0000_0000_0000_0000_0000_0001 =
==================================================
fraig> cirfraig
Proving (3, !4)...SAT!!
Updating by SAT... Total #FEC Group = 0
fraig> cirg 1
==================================================
= PI(1), line 2 =
= FECs: =
= Value: 0000_0001_0001_1000_0100_1101_0010_0000 =
==================================================
fraig> q -f
fraig之后cirg 1的value应该是从SatSolver::getValue()得到的吧?但是getValue()
一次只能拿到一个bit吧?不知新的simulation pattern是用什么神奇的方法得到的?
或是我其他地方理解有误?