0

私はZ3で以下のSMT2仕様を実行しています。目標はeval、最後に-trueまたは-のいずれかに対する答えを取得するfalseことですが、代わりにletステートメントを取得します。これはバグですか、letそれとも特定の方法で解釈することになっていますか？手作業でコンパイルするfalseと非常に簡単に見えますが、Z3は混乱しているようです。

(declare-sort PolymorphicClass 0)

(declare-fun PolymorphicClass!val!6 () PolymorphicClass)
(declare-fun PolymorphicClass!val!13 () PolymorphicClass)
(declare-fun PolymorphicClass!val!2 () PolymorphicClass)
(declare-fun PolymorphicClass!val!12 () PolymorphicClass)
(declare-fun PolymorphicClass!val!14 () PolymorphicClass)
(declare-fun PolymorphicClass!val!10 () PolymorphicClass)
(declare-fun PolymorphicClass!val!8 () PolymorphicClass)
(declare-fun PolymorphicClass!val!9 () PolymorphicClass)
(declare-fun PolymorphicClass!val!15 () PolymorphicClass)
(declare-fun PolymorphicClass!val!0 () PolymorphicClass)
(declare-fun PolymorphicClass!val!1 () PolymorphicClass)
(declare-fun PolymorphicClass!val!11 () PolymorphicClass)
(declare-fun PolymorphicClass!val!3 () PolymorphicClass)
(declare-fun PolymorphicClass!val!5 () PolymorphicClass)
(declare-fun PolymorphicClass!val!4 () PolymorphicClass)
(declare-fun PolymorphicClass!val!7 () PolymorphicClass)

(define-fun k!623 ((x!1 PolymorphicClass)) PolymorphicClass
  (ite (= x!1 PolymorphicClass!val!15) PolymorphicClass!val!15
  (ite (= x!1 PolymorphicClass!val!2) PolymorphicClass!val!2
  (ite (= x!1 PolymorphicClass!val!7) PolymorphicClass!val!7
  (ite (= x!1 PolymorphicClass!val!8) PolymorphicClass!val!8
  (ite (= x!1 PolymorphicClass!val!10) PolymorphicClass!val!10
  (ite (= x!1 PolymorphicClass!val!9) PolymorphicClass!val!9
  (ite (= x!1 PolymorphicClass!val!14) PolymorphicClass!val!14
  (ite (= x!1 PolymorphicClass!val!0) PolymorphicClass!val!0
  (ite (= x!1 PolymorphicClass!val!6) PolymorphicClass!val!6
  (ite (= x!1 PolymorphicClass!val!5) PolymorphicClass!val!5
  (ite (= x!1 PolymorphicClass!val!1) PolymorphicClass!val!1
  (ite (= x!1 PolymorphicClass!val!4) PolymorphicClass!val!4
  (ite (= x!1 PolymorphicClass!val!12) PolymorphicClass!val!12
  (ite (= x!1 PolymorphicClass!val!11) PolymorphicClass!val!11
    PolymorphicClass!val!13)))))))))))))))

(define-fun isBlog!641 ((x!1 PolymorphicClass)) Bool
  (ite (= x!1 PolymorphicClass!val!0) true
  (ite (= x!1 PolymorphicClass!val!1) true
    false)))

(define-fun isBlog ((x!1 PolymorphicClass)) Bool
  (isBlog!641 (k!623 x!1)))

(check-sat)
(get-model)

(eval (isBlog PolymorphicClass!val!6))

(exit)

Z3から得られる出力は次のとおりです。

sat
(model 
)
(let ((a!1 (ite (= PolymorphicClass!val!6 PolymorphicClass!val!9)
                PolymorphicClass!val!9
                (ite (= PolymorphicClass!val!6 PolymorphicClass!val!14)
                     PolymorphicClass!val!14
                     (ite (= PolymorphicClass!val!6 PolymorphicClass!val!0)
                          PolymorphicClass!val!0
                          PolymorphicClass!val!6)))))
(let ((a!2 (ite (= PolymorphicClass!val!6 PolymorphicClass!val!7)
                PolymorphicClass!val!7
                (ite (= PolymorphicClass!val!6 PolymorphicClass!val!8)
                     PolymorphicClass!val!8
                     (ite (= PolymorphicClass!val!6 PolymorphicClass!val!10)
                          PolymorphicClass!val!10
                          a!1)))))
(let ((a!3 (ite (= PolymorphicClass!val!6 PolymorphicClass!val!15)
                PolymorphicClass!val!15
                (ite (= PolymorphicClass!val!6 PolymorphicClass!val!2)
                     PolymorphicClass!val!2
                     a!2))))
          (or (= a!3 PolymorphicClass!val!0) (= a!3 PolymorphicClass!val!1)))))
4

1 に答える 1

1

あなたの値は実際の制約では使用されていません（定義でのみ）。モデル補完を使用して、制約で使用されていない値をZ3が確実に評価するようにすることができます。

だからあなたは呼び出すことができます：

   (eval (isBlog PolymorphicClass!val!6) :model-completion true)

適切な評価を得るために。

関連する質問を参照してください：Z3 4.3：追加情報については完全なモデルを入手してください。

于 2013-02-04T20:27:51.963 に答える