5

z3 で QF_AUFLIA の式を分析しました。結果は でしたsat。によって返されたモデルには(get-model)、次の行が含まれていました。

  (define-fun PCsc5_ () Int
    (ite (= 2 false) 23 33)

SMTLIBv2 言語に関する私の理解によれば、このステートメントは形式が正しくありません。=同じ種類の引数にのみ適用する必要があります。ただし、2sortIntとsortfalseがありますBool。

この 2 行だけを z3 にフィードバックすると、次のように同意してくれます。

invalid function application, sort mismatch on argument at position 2

これはバグですか？

そうでない場合、どのように解釈すればよい(= 2 false)ですか?

4

1 に答える 1

5

この問題は、入力の型エラーが原因でした。Z3 3.2 では、マクロ アプリケーションのいくつかの型エラーが見逃されます。この問題は修正されました。次のリリースでは、型エラー (別名、並べ替えの不一致) が正しく報告されるようになります。問題を明らかにする最小限の例を次に示します。

(set-option :produce-models true)
(declare-fun q (Int) Bool)
;; p1 is a macro
(define-fun p1 ((z Int) (y Int)) Bool
  (ite (q y) (= z 0) (= z 1)))
(declare-const a Int)
(declare-const b Bool)
(assert (p1 a b)) ;; << TYPE ERROR: b must be an Int
(check-sat)
(get-model)
于 2012-01-05T00:45:43.200 に答える