optimization - CVC4 モデルの最適化を最小化/最大化

Question

CVC4 は、Z3のようにビットベクトルの結果モデルを最大化または最小化するオプションですか?

ありがとう。

Answer 1

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