z3 - Z3 maxsat smtlib 2.0

Question

smtlib2.0 インスタンスを使用して c++ API で maxsat を実行する方法はありますか。つまり、関数 get_soft_constraints を smtlib2.0 インスタンスで動作させる方法は?

Answer 1

いいえ、maxsat例は SMT 2.0 が導入される前に実装されました。この例を変更して、SMT 2.0 ファイルを読み取ることができます。基本的な考え方は、SMT 1.0 の代わりに SMT 2.0 パーサーを使用し、ソフトな制約を特定するメカニズムを考案することです。