CODEWITHSUNDEEP
z3
Thomas M. DuBuisson
Thomas M. DuBuisson

Reputation: 64740

Why can't Z3/HORN solve xor?

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?

Upvotes: 3

Views: 689

Answers (1)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8359

The problem is that the benchmark is annotated as "HORN", but the formulas do not properly belong to the HORN fragment that is supported. If you remove the 

(set-logic HORN)

line, then Z3 answers sat by applying the default strategy. With the (set-logic HORN) line, Z3 uses only the HORN strategy.

It gives up if the formula does not belong to the supported fragment. The supported fragment of Horn clauses assume that the assertions are universally quantified (forall quantified). The assertions should also be Horn clauses (implications), such that the head of the implication is either an uninterpreted predicate or some formula without any uninterpreted predicates. The body of the implication (left side of the implication) is a conjunction of formulas, that are either an occurrence of the uninterpreted predicate or some formula without the uninterpreted predicate. A horn clause can also be an atomic formula consisting of an application of an uninterpreted predicate. The pre-processor does recognize some formulas that are not directly formulated as implications, but it is easier for experimentation to conform with pure Horn clauses.

Here are some sample Horn clauses:

 (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)

Upvotes: 4

Related Questions