1

プログラムのバグを示すテスト ケースを導出するために使用できるモデルを取得するために、Why3 の Z3 バックエンドを使用しようとしています。ただし、Z3 バージョン 4.3.2 はsat、Why3 の目標に答えることができないようです。Why3 で使用されている公理的な定義の一部が Z3 を混乱させているようです。たとえば、次の例 (Why3 が生成するもののごく一部です)

(declare-fun abs1 (Int) Int)

;; abs_def
  (assert
  (forall ((x Int)) (ite (<= 0 x) (= (abs1 x) x) (= (abs1 x) (- x)))))

(check-sat)

timeout次のコマンドラインで結果が得られます。

z3 -smt2 model.partial=true file.smt2 -T:10

一方、定義を次のように変更すると、

(declare-fun abs1 (Int) Int)

;; abs_def
  (assert
  (forall ((x Int)) (=> (<= 0 x) (= (abs1 x) x))))

  (assert
  (forall ((x Int)) (=> (> 0 x) (= (abs1 x) (- x)))))

モデルを取得します（かなり妥当に見えます）

(model 
  (define-fun abs1 ((x!1 Int)) Int
    (ite (>= x!1 0) x!1 (* (- 1) x!1)))
)

しかし、元のWhy3ファイルに存在する次の公理を追加しようとすると、つまり

;; Abs_pos
(assert (forall ((x Int)) (<= 0 (abs1 x))))

再びZ3が答えますtimeout。

Z3 の設定で何か足りないものはありますか? さらに、Why3 の以前のバージョンには、MODEL_ON_TIMEOUTそのような状況でモデルを取得できるオプションがありました。Z3がチェックを終了できなかったため、これが実際のモデルであるという保証はありませんでしたが、実際には、そのようなモデルには通常、必要なすべての情報が含まれていました. ただし、4.3.2 には同様のオプションが見つかりませんでした。それはまだ存在しますか？

更新最後の公理Abs_posは間違っていました (ここに投稿する前に Why3 の出力を少しいじり、間違ったバージョンの問題を貼り付けてしまいました)。これは修正されました。

4

1 に答える 1

0

追加の公理

(assert (not (forall ((x Int)) (<= 0 (abs1 x))))))

abs1 は常に非負の整数を返し、追加の公理を使用すると、いくつかの x について abs1 に負の結果が存在する必要があるため、問題は満足できなくなります。Z3 の Web バージョンは期待どおり unsat を返します。こちらを参照してください。

于 2015-02-24T09:43:20.500 に答える