z3の 'smt_tactic'はQF_BV式をどのように解決しますか？

-1

z3がQF_BV式を解くために（ 'qfbv'戦術の代わりに） 'smt_tacitc'を使用すると、SATエンジンがビットブラストされて使用されますか？私がverbose 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も役立ちます）。 –

z3の 'smt_tactic'はQF_BV式をどのように解決しますか？

答えて

関連する問題