如何使用 HORN 逻辑证明 Z3 中的两个关系相等

Question

我在 Z3 中使用 Horn Logic 来对 CSP（过程代数）进行模型检查，因为 Horn Logic 擅长处理递归定义。但是，我遇到了一些技巧问题。例如，我有以下代码：

(declare-rel A (Int))
(declare-rel B (Int))

(rule (A 1))
(rule (A 2))

(rule (B 1))
(rule (B 2))

那么，我如何证明 A 和 B 相等。这类似于使用 Horn Logic 在 Z3 中证明两个集合的等价性。

拜托，谁能给我一个线索？非常感谢。

Answer 1

有一个支持分层否定的引擎。 它仅适用于有限域。使用分层否定，您可以 检查等价性。例如：

(declare-rel A ((_ BitVec 8)))
(declare-rel B ((_ BitVec 8)))
(declare-rel q ())

(rule (A #x01))
(rule (A #x02))

(rule (B #x01))
(rule (B #x02))

(declare-var x (_ BitVec 8))

(rule (=> (and (A x) (not (B x))) q))
(rule (=> (and (B x) (not (A x))) q))

(query q)