如何Z3的「smt_tactic」解決QF_BV公式？

-1

當Z3用途（而不是「qfbv」戰術）「smt_tacitc」解決QF_BV公式，將它咬母細胞，並使用SAT發動機？當我將詳細的leval設置爲10時，我看不到爆炸。如何Z3的「smt_tactic」解決QF_BV公式？

2017-03-09 rainoftime

它確實有點爆破，但懶洋洋地。它將使用SMT解算器。但是請注意，是位爆破是相當渴望，雖然。

2017-03-09 09:03:01

感謝。通過「懶惰」，你的意思是解決QF_BV例如當'smt_tacitc'將使用DPLL（T）類的抽象細化循環？ – rainoftime

沒錯。如果您在調試模式下構建Z3並使用-tr：foo選項進行播放，則可以更詳細地打印正在進行的操作。（和-v：999999也有幫助）。 –

回答