3

While we are on the topic of horn clauses, I have been trying to figure out the capabilities and limitations of μZ. I taught Z3 the theory of xor over a user defined sort, but it is unable to apply the rules effectively, resulting in unknown for any interesting query. Pairing down, I obtained this example that surprisingly returns 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)

Am I wrong to expect sat even when the uninterpreted p is used? I note the linked question includes an uninterpreted function, inv, but is handled by Z3. Should I have inferred this short-coming from the PDR paper or is there another publication that could illuminate the current state of Z3 PDR?

EDIT: I am guessing this result is due to the use of existential quantification. If that's the case, and given that my problem requires existentials, is there a reasonable alternative formulation?

4

1 回答 1

4

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

(set-logic HORN)

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

如果公式不属于支持的片段，它会放弃。支持的 Horn 子句片段假定断言是普遍量化的（forall quantified）。断言也应该是 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)
于 2013-07-05T18:07:56.200 回答