Explosive memory use when reasoning about XOR (all AC theories?)

Question

It appears that reasoning about XOR causes explosive memory use for Z3 (commit 210bca8f456361f696152be909e33a4e8b58607f2). For example, deriving a+b+c from something that is AC equivalent to a+b+c+x+x+y+y+z+z:

(declare-fun known (Bool) Bool)
(declare-fun p (Bool Bool Bool) Bool)

; Lift xor
(assert (forall ((x Bool) (y Bool))
            (=> (and (known x) (known y)) (known (xor x y)))))

; Can reason about xor well
(assert (exists ((a1 Bool) (b1 Bool) (c1 Bool) (ra Bool) (rb Bool) (rc Bool))
            (and (p a1 b1 c1)
                 (known (xor a1 (xor ra rc)))
                 (known (xor b1 (xor rb ra)))
                 (known (xor c1 (xor rc rb))))))

; Assert that we can derive a+b+c.
; Note: The behavior (non-termination) is the same when this example is
;       inverted (forall ... not ...)
(assert (exists ((a1 Bool) (b1 Bool) (c1 Bool))
            (and (p a1 b1 c1)
                 (known (xor a1 (xor b1 c1))))))
(check-sat)

Is this an accepted limitation? Are there alternate formulations I can use to answer queries like this with Z3?

Continuity: I had previously misused the HORN logic for this task.

Answer 1

The problem is that the assertion

(assert (forall ((x Bool) (y Bool))
            (=> (and (known x) (known y)) (known (xor x y)))))

is really bad for the E-matching engine. This is one of the engines used to handle quantifiers in Z3. There are many possible workarounds.

1) Use quantifier elimination. You just have to replace (check-sat) with (check-sat-using (then qe smt))

2) Annotate the quantifier with a :weight attribute. The E-matching engine will stop producing new instances earlier. Here is an example:

(assert (forall ((x Bool) (y Bool))
        (!  (=> (and (known x) (known y)) (known (xor x y)))
            :weight 10)))

3) Disable the E-matching engine. Then, Z3 will use only the MBQI (model-based quantifier instantiation) engine, which is much more effective for this kind of problem. To disable E-matching, we should use

(set-option :smt.ematching false)

Remark: in Z3 version <= 4.3.1, this option is called (set-option :ematching false)