模型中的排序不匹配

我已经用z3分析了QF_AUFLIA中的一个公式。结果是sat。通过(get-model)返回该模型包含以下行：模型中的排序不匹配

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

根据我的SMTLIBv2语言的理解，这种说法是畸形的。 =只应用于相同类型的参数。然而，2有排序Int和false有排序Bool。

invalid function application, sort mismatch on argument at position 2

这是一个错误：

当我反馈只是这两条线到Z3，它跟我说同意？

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

来源

2012-01-03 Georg

是的，这似乎是模型构造中的一个错误。你可以给我们发送这个伪造模型的公式吗？谢谢。 – 2012-01-03 14:47:38

我刚刚给你发了一封电子邮件。 – Georg 2012-01-03 15:02:50

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

来源

2012-01-05 00:45:43

模型中的排序不匹配

回答

相关问题