z3 - 为什么Z3/HORN不能解xor？

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) 

行，然后通过应用默认策略坐下 Z3 个答案。对于 (set-logic HORN) 行，Z3 仅使用 HORN 策略。

如果公式不属于支持的片段，则放弃。受支持的 Horn 子句片段假定断言是普遍量化的(forall 量化)。断言也应该是 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)