Z3是否有促进关联/交换运算符链中的子公式匹配的功能？

Question

假设我有一个用户定义的交换和结合运算符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，a，b，c，d)的所有可能的二叉树。我也可以保留并希望z3自己使用结合性和交换性，并触发假设1的正确实例化。

如果我们考虑到(op，a，b，c)这样的链可以出现在通用量化中，问题就会变得更加复杂。我们可能会使用模式(op a (op B c))，(op b (op A C))等来最大化量化被实例化的机会，但是模式必须出现在某个地方，而z3可能没有让它自己出现的指导。

有什么我能做得更好的吗？

谢谢!西蒙

Answer 1

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