（デフォルトのチェックを使用）など

Question

論理が指定されずにZ3が実行され、(check-sat)が発行されると、default_tactic.cppのロジックが条件付きで「最良」のソルバーを起動します。私はSMT-LIB 2インターフェースからこのデフォルトの戦術にアクセスしたいと思います。

私はSMT-LIBにdefault_tactic.cppからロジックを翻訳してみました、と私はこの思い付いた：

(check-sat-using (and-then simplify 
    (cond is-qfbv qfbv 
    (cond is-qflia qflia 
    (cond is-qflra qflra 
    (cond is-qfnra qfnra 
    (cond is-qfnia qfnia 
    (cond is-nra nra 
    (cond is-lira lira 
    (cond is-qffpabv qffpa 
    smt)))))))))) 

この「ほとんど」の作品は、その中で、あなたは、liranraで行を削除した場合、qffpaとすると、Z3はこれを問題なく実行します。これら3つの戦術は、Z3 4.4.1のSMT-LIB 2インターフェースでは公開されていないようです。しかし、この問題のもう一つの問題は、Z3の将来のリビジョンでデフォルトの戦術が更新された場合、上記のようなハードコードされた戦略は更新されないということです。

は、私が本当にやりたいことは(check-sat-using default)、または類似した何かのようにコマンドを発行し、(check-sat)で得られたとして、同じ結果を得ることです。これは可能ですか？

Answer 1

あなたが参照しているファイルは非常に古いです。その後、Z3はGitHubに移動し、default_tactic.cppの最新バージョンはhereになりました。 QF_FPのデフォルトの戦術は今qffp呼ばれる

、lira戦術は、以来、同様エクスポートされたと私はちょうど（this commitのような）だけでなくnraを輸出しました。

---

編集：this commitのよう、default戦術にも輸出されているので、要求されたとして、それは(check-sat-using default)を書きできるようになりました。