CVC4最小化/最大化モデル最適化

Question

ビットベクトルas Z3 doesの結果モデルを最大化または最小化するオプションはありますか？

ありがとうございました。

Answer 1

残念ながら、CVC4は（まだ）最適化をサポートしていません。ビットベクトルの場合は、複数のクエリとバイナリ検索を使用していつでも自分で行うことができますが、ビルトインではありません。