模型中的排序不匹配

发布于 2024-12-24 16:52:32 字数 513 浏览 2 评论 0原文

我用 z3 分析了 QF_AUFLIA 中的公式。结果是sat。 (get-model) 返回的模型包含以下几行：

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

根据我对 SMTLIBv2 语言的理解，该语句格式错误。 = 只能应用于相同类型的参数。但是，2 具有 Int 排序，false 具有 Bool 排序。

当我将这两行反馈给 z3 时，它同意我的说法：

invalid function application, sort mismatch on argument at position 2

这是一个错误吗？

如果不是，我该如何解释 (= 2 false)？

原文

I have analyzed a formula in QF_AUFLIA with z3. The result was sat. The model returned by (get-model) contained the following lines:

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

According to my understanding of the SMTLIBv2 language, this statement is malformed. = should only be applied to arguments of the same sort. However, 2 has sort Int and false has sort Bool.

When I feed back just these two lines to z3, it agrees with me by saying:

invalid function application, sort mismatch on argument at position 2

Is this a bug?

If not, how am I supposed to interpret (= 2 false)?

分享到QQ

分享到微博

如果你对这篇内容有疑问，欢迎到本站社区发帖提问参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。

发布评论

需要登录才能够评论，你可以免费注册一个本站的账号。

林空鹿饮溪 2024-12-31 16:52:32

该问题是由于输入中的类型错误造成的。 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)

The problem was due to a type error in the input. Z3 3.2 misses some type errors in macro applications. This problem was fixed. The next release will correctly report the type error (aka sort mismatch). Here is a minimal example that exposes the problem:

(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)

回复收藏 0 原文

~没有更多了~