4

定義した変数とともにモデル文字列を取得しようとすると、モデルに次のように追加の出力が表示されます-

 z3name!0=3, z3name!1=-2, z3name!10=0, z3name!11=0, z3name!12=0, z3name!13=0, z3name!14=0, z3name!15=0, z3name!2=0, z3name!3=0, z3name!4=2, z3name!5=2, z3name!6=0, z3name!7=-3, z3name!8=2, z3name!9=0

これが誤った出力なのか知りたいのですが？それとも、Z3で使用されているのはいくつかの中間変数ですか？

私が定義した変数の値は私には問題ないように思われるからです。私は以前にそのような出力を見たことがないので、私はこの疑問を抱きました。

4

2 に答える 2

5

Z3にはいくつかの前処理ステップがあります。それらのいくつかは新しい変数を導入します。新しい変数は通常、結果のモデルから削除されます。そうでない場合、これはバグです。ただし、このバグは正確性には影響しません。ただの不便です。

あなたがあなたの問題を投稿することができればそれは素晴らしいでしょう。導入された補助変数を排除していない前処理ステップを特定することができます。

于 2012-06-11T15:32:54.470 に答える
1

これは古いトピックだと思いますが、レオナルドが呼んだのと同じ「バグ」を抱えていることに気づきました。OPは彼のコードを投稿しなかったので、私はおそらくそれを修正するのに役立つと思いました（ただし、正確さが実際に維持されている限り、この余分な出力は私にとって問題ではありません）。

たとえば、「+」演算子の最後のアサーションで「/」を変更すると、問題が解消されるようです。

(declare-fun fun0!0 () Int)
(declare-fun fun0!-1 () Int)
(declare-fun var0 () Int)

(assert (and
    (and
        (or (= fun0!0 0) (= fun0!0 1) (= fun0!0 2))
        (or (= fun0!-1 0) (= fun0!-1 1) (= fun0!-1 2))
        (or (= var0 1) (= var0 -1))
    )
    (and (or (= var0 0) (= var0 -1)))
))

(define-fun fun0 ((i! Int)) Int
    (ite
        (= i! 0)
        fun0!0
        (ite
            (= i! -1)
            fun0!-1
            (- 0 1)
        )
    )
)

(assert (=
    (fun0 var0)
    (/ var0 var0)
))
(check-sat)
于 2017-11-18T22:58:25.997 に答える