跑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是用什麼神奇的方法得到的?
或是我其他地方理解有誤?