z3シェルとjava apiの異なる解決

Question

私はz3シェルとjava apiの両方で同じ仮定を試みました。次のように：

(declare-const x (_ BitVec 32)) 

(assert (not (bvsle (bvadd x #xfffffff8) #x00000000))) 
(check-sat) 
(get-model) 

をZ3シェルでは、解決策はあります。x = 9 しかし、Z3 APIでは、解決策はあります。x = 0x80000000の 私のアプリケーションでは、私はシェルの結果を好みます。 APIの使い方でいくつかのオプションが欠けていたら

BTW。私は、ソリューションの値を制御するために使用できる任意のオプションは、私はいくつかのより合理的な値が欲しいです。しかし、しばしばZ3は私にランダムな価値のように見える本当に大きな価値を与えます。

Answer 1

私の知る限り、充足式のモデルがZ3にランダムに選択されると言うことができます。

妥当な値あなたは小さなを意味することによって場合は、原則として返されるモデルは#x00000009に等しいxを設定することを確実にするためにZ3でx上で最適化することができます。例えば、。難しい問題の検索にかかった時間に大きな影響があるかもしれません。もちろん、

(declare-const x (_ BitVec 32)) 

(assert (not (bvsle (bvadd x #xfffffff8) #x00000000))) 
(minimize x) 
(check-sat) 
(get-model) 

。

これは、最適化検索上タイムアウトを設定するこれらの状況の一つであり、まだ最適解の最良の近似（もしあれば）に関連したモデルを取得することができるという、理想的です。しかし、z3がこの機能を持っているかどうかわかりません。