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 回答