2

Z3 を使用して、線形整数演算、解釈されない関数、ブール変数に対する量指定子を含むロジックの充足可能性をチェックしています。Z3 は、充足可能な問題のモデルを提供しません。これは、量指定子 (または、私が選択したロジック: AUFLIA) によるものだと思います。

すべてのブール変数を自分でインスタンス化する以外に、Z3 にそのような問題のモデルを提供させる方法はありますか?

4

1 に答える 1

2

Z3 は、原則として、このフラグメントを決定できます。「原則として」と言ったのは、このフラグメントの決定問題の複雑さが非常に高いためです。たとえば、NEXPTIME-complete である Bernays-Schönfinkel フラグメント (別名 EPR) を包含します。Z3 で決定できるフラグメントのリストは、http: //rise4fun.com/z3/tutorial/guideにあります。

モデルベースの量指定子のインスタンス化 (MBQI) が Z3 で有効になっていることを確認する必要があります。MBQI=trueこれは、コマンド ライン オプションまたは SMT2 コマンドを使用して行うことができます。

(set-option :mbqi true)

Z3 には、MBQI ステップの反復回数にもしきい値があります。コマンドラインオプションMBQI_MAX_ITERATIONS=<value>またはコマンドを使用して、しきい値を変更できます

(set-option :mbqi-max-iterations 1000000)

MBQI ステップごとに、Z3 に、現在の候補モデルによって満たされていない量指定子を表示するように依頼できます。オプションMBQI_TRACE=true

そうは言っても、あなたが送ってくれた SMT2 スクリプトによって明らかになったバグ (クラッシュ) を最近修正しました。この修正は Z3 3.2 で利用可能になります。

于 2011-09-09T14:38:36.477 に答える