为什么 Z3/HORN 不能解决异或？

Question

当我们讨论horn clauses 的主题时，我一直在试图弄清楚 μZ 的功能和局限性。我向 Z3 教授了用户定义排序的异或理论，但它无法有效地应用规则，导致任何有趣的查询都出现unknown。配对下来，我得到了这个意外返回unknown的例子：

(set-logic HORN)
(declare-fun p (Bool Bool Bool) Bool)

; Test if Z3 can discover two a1+b1+c1 by canceling ra, rb, and rc
(assert (exists ((a1 Bool) (b1 Bool) (c1 Bool) (ra Bool) (rb Bool) (rc Bool))
                (and (p a1 b1 c1)
                 (xor (xor a1 (xor ra rc))
                      (xor b1 (xor rb ra))
                      (xor c1 (xor rc rb))))))

; Assert the adversary can not derive the secret, a+b+c.
(assert (exists ((a1 Bool) (b1 Bool) (c1 Bool))
            (and (p a1 b1 c1) (xor a1 (xor b1 c1)))))
(check-sat)

即使使用未解释的p，我期望sat 是错误的吗？我注意到链接的问题包括一个未解释的函数inv，但由 Z3 处理。我应该从 PDR 论文中推断出这个缺点，还是有其他出版物可以阐明 Z3 PDR 的当前状态？

编辑：我猜这个结果是由于使用了存在量化。如果是这样，并且考虑到我的问题需要存在主义，是否有合理的替代表述？

Answer 1

问题是基准被注释为“HORN”，但公式​​不正确地属于支持的 HORN 片段。 如果您删除

(set-logic HORN) 

line，然后 Z3 通过应用默认策略来回答。 对于 (set-logic HORN) 行，Z3 仅使用 HORN 策略。

如果公式不属于支持的片段，它会放弃。 支持的 Horn 子句片段假设断言是普遍量化的 （全部量化）。断言也应该是 Horn 子句（蕴涵），这样 蕴涵的头部要么是一个未解释的谓词，要么是一些没有任何含义的公式 未解释的谓词。暗示的主体（暗示的左侧） 是公式的结合，或者是未解释谓词的出现 或一些没有未解释谓词的公式。 喇叭子句也可以是一个原子公式，由一个未解释的应用程序组成 谓词。 预处理器确实可以识别一些不是直接公式化的公式 作为暗示，但实验更容易符合纯 Horn 子句。

以下是一些示例 Horn 子句：

 (forall ((a Bool) (b Bool)) (=> (xor a b) (p a b)))

 (forall ((a Bool) (b Bool)) (=> (and (xor a b) (p a b)) false))

 (p true false)