1

次の SMT-Lib2 スクリプトがあります。

(set-option :produce-models true)
(declare-fun s0 () Int)
(declare-fun table0 (Int) (_ BitVec 8))
(assert (= (table0 0) #x00))
(assert
   (let ((s3 (ite (or (< s0 0) (<= 1 s0)) #x01 (table0 s0))))
   (let ((s5 (ite (bvuge s3 #x02) #b1 #b0)))
   (= s5 #b1))))
(check-sat)
(get-model)

Z3 v3.2 を Mac で実行すると、次のようになります。

sat
(model 
  ;; universe for (_ BitVec 8):
  ;;   bv!val!2 bv!val!3 bv!val!0 bv!val!1 
  ;; -----------
  ;; definitions for universe elements:
  (declare-fun bv!val!2 () (_ BitVec 8))
  (declare-fun bv!val!3 () (_ BitVec 8))
  (declare-fun bv!val!0 () (_ BitVec 8))
  (declare-fun bv!val!1 () (_ BitVec 8))
  ;; cardinality constraint:
  (forall ((x (_ BitVec 8)))
          (and (= x bv!val!2) (= x bv!val!3) (= x bv!val!0) (= x bv!val!1)))
  ;; -----------
  (define-fun s0 () Int
    (- 1))
  (define-fun table0 ((x!1 Int)) (_ BitVec 8)
    (ite (= x!1 0) bv!val!0
    (ite (= x!1 (- 1)) bv!val!3
      bv!val!0)))
)

これは、s0 = -1 がモデルであることを示しています。ただし、s0 = -1 の場合、s3 = 1 および s5 = #b0 となり、アサーションが偽になります。実際、記載されているベンチマークは満足できないものであると確信しています。

Z3 の出力で気づいたことの 1 つは、カーディナリティ制約に対して与えられる定量化された式です。それは言います：

  ;; cardinality constraint:
  (forall ((x (_ BitVec 8)))
          (and (= x bv!val!2) (= x bv!val!3) (= x bv!val!0) (= x bv!val!1)))

アサーションは接続詞で、かなり奇妙に聞こえます。それは分離ではないでしょうか？これが問題の根本的な原因であるかどうかはわかりませんが、怪しげに聞こえます。

4

1 に答える 1

1

Z3には2つの問題があります。まず、あなたは正しいです。モデル プリンターにタイプミスがあります。「and」ではなく「or」にする必要があります。2 つ目の問題は、Z3 がビットベクトル理論をインストールせず(_ BitVec 8)、解釈されないソートとして扱われたことです。これは、問題が発生しているロジックを判断するために使用されるプリプロセッサのバグでした。ファイルの先頭に次のコマンドを追加することで、このバグを回避できます。

(set-option :auto-config false)

これらのバグは修正されており、修正は次のリリースで利用可能になります。

于 2012-02-24T16:48:29.490 に答える