似乎关于 XOR 的推理会导致 Z3 的内存使用爆炸(提交 210bca8f456361f696152be909e33a4e8b58607f2)。例如,派生a+b+c
自与 AC 等价的东西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)
这是一个公认的限制吗?我可以使用其他公式来回答 Z3 的此类查询吗?
连续性:我之前在这个任务中误用了 HORN 逻辑。