1

假设我有一个用户定义的交换和关联运算符 op。下面的代码无效，因为我使用的 op 具有两个以上的参数。让我们暂时假设它是有效的，并且它意味着“应用 op 的方式是无关紧要的”。

(declare-sort T 0)
(declare-fun op (T T) T)
(declare-fun P (T) Bool)
(declare-const a T)
(declare-const b T)
(declare-const c T)
(declare-const d T)
(declare-const k T)
; associativity
(assert (forall ((x T) (y T)) (z T)) 
                (= (op x (op y z)) 
                   (op (op x y) z))))
; commutativity
(assert (forall ((x T) (y T))) 
                (= (op x y) 
                   (op y x))))
; assumption 1
(assert (forall ((x T) (y T)) (= (op x y) k)))
; assumption 2
(assert (P (op a c k)))
; conjecture
(assert (not (P (op a b c d))))

确保假设 1 用 x, y := b, d 实例化并且假设 2 适用于证明猜想的最佳方法是什么？

我正在考虑的一种解决方案是生成所有可能对应于 (op abcd) 的二叉树。然而，这是相当昂贵的：有 5 种不同的二叉树，有 4 片叶子和 24 种不同的叶子排列，总共 120 棵不同的二叉树。我也可以忍住并希望 z3 自己使用关联性和交换性并触发假设 1 的正确实例化。

如果我们考虑到像 (op abc) 这样的链可以出现在全称量化中，问题就变得更加棘手。我们可能可以使用模式 (op a (op bc))、(op b (op ac)) 等来最大化量化被实例化的机会，但模式必须出现在某个地方，而 z3 可能没有指导让它自己出现。

有什么更好的我可以做的吗？

谢谢！西蒙

4

1 回答 1

1

Z3 对匹配模 A、C、AC、ACI 没有任何特殊支持。对于您给出的特定示例，事实证明假设 1 更为重要，但这只是该特定示例的产物。

于 2014-04-14T16:37:52.187 回答