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 戦略のみを使用します。

数式がサポートされているフラグメントに属していない場合はあきらめます。ホーン句のサポートされているフラグメントは、アサーションが普遍的に定量化されていることを前提としています (forall quantified)。アサーションもホーン節 (含意) である必要があります。含意の先頭は、解釈されていない述語か、解釈されていない述語を含まない式のいずれかです。含意の本体 (含意の左側) は、未解釈の述語の出現か、未解釈の述語を含まない式のいずれかである式の結合です。ホーン節は、解釈されない述語の適用からなる原子式であることもできます。プリプロセッサは、含意として直接定式化されていないいくつかの式を認識しますが、純粋なホーン節に準拠する方が実験が容易です。

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 に答える