2016-07-18 15 views
1

私が働いている会社では、複数のSATソルバーにアクセスできます。 各SATソルバがZ3 SMTソルバのパフォーマンスにどのように影響するかを分析したいと思います。Z3から外部SATソルバーを呼び出す

Z3から外部SATソルバーを呼び出すことはできますか? そうでなければ、外部ソルバーを呼び出すためにZ3を変更する必要がありますか?

答えて

0

Z3は緊密に統合された内部SATソルバーを使用しているので、これは簡単な作業ではないと思います。 SATソルバとの緊密な統合は、Z3が外部SATソルバの低レベルAPI、例えばプッシュ&ポップ機能を備えています。これらのAPIは標準化されていないので、例えば、 MiniSatは、例えば、 Lingelingとの統合の課題。私はそれが不可能ではないと言いません.Z3は拡張されることになっているモジュラーアーキテクチャーを持っているからですが、これは大きな仕事になると思います。

Z3デベロッパーの1人が出てきて、間違っていると分かるかもしれません。

関連する問題