我想用SMT格式编写证明义务，其中一些函数具有一些共同的通用属性（即关联性和可交换性） .
一个简单的解决方案是在证明义务中包含相应的公理 . 我想这意味着这些属性的推理将在很大程度上取决于量词实例化算法 . 其他技术，如重写，可能更有效，我想知道Z3是否实现了这种技术 . API中存在诸如Z3_OP_PR_REFLEXIVITY和Z3_OP_PR_COMMUTATIVITY之类的值表明这可能是这种情况 .
我的第一个问题是：
- 除了通过用户定义公理的量化实例化之外，Z3是否具有处理用户定义符号的通用属性的方法？
如果答案是肯定的，那么：
-
这样的通用属性是什么？
-
因为据我所知，SMT-LIB标准没有修复用户定义符号（仅理论符号）的这些属性，用于声明用户定义符号具有给定属性的SMT语法是什么？