1

最新の Z3 バージョン 3.2 を使用しています。「get-value」コマンドから予期しない応答が返されました。SMT-LIB2 準拠モードで実行する小さなスクリプトを次に示します。

(set-option :produce-models true)
(declare-datatypes () ((Object o0 null)))
(declare-fun IF (Object) Int)
(declare-fun i2 () Int) 
(assert (= (IF o0) i2))
(assert (= (IF null) 0))
(check-sat)
(get-value (i2))

応答は次のとおりです。

((i2 (IF o0)))

ちょうど「0」が返ってくると思います。返された項をユニバース定数に評価するように Z3 に依頼する方法はありますか?

完全なモデルは次のとおりです。

(model 
;; universe for Object:
;;   Object!val!0 
;; -----------
;; definitions for universe elements:
(declare-fun Object!val!0 () Object)
;; cardinality constraint:
(forall ((x Object)) (= x Object!val!0))
;; -----------
(define-fun i2 () Int
(IF o0))
(define-fun IF ((x!1 Object)) Int
  (ite (= x!1 Object!val!0) 0
    0))
)

モデルで o0 が定義されていない理由にも困惑しています。

4

1 に答える 1

1

これはZ34.0で修正されています。Z34.0はまもなくリリースされます。それまでの間、オンラインで使用できます:http: //rise4fun.com/Z3/75y

このリンクを使用して、例を実行できます。Z3 4.0は、期待どおりの結果を生成します。

バグに関して、主な問題は、Z3がオブジェクトを解釈されていないソートとして扱っていることです。Z3 3.2では、次のように含めることでこのバグを回避できます。

(set-option:auto-config false)

スクリプトの最初に。

于 2012-04-17T21:08:58.950 に答える