z3 是否支持将运算符标记为关联运算符、交换运算符或两者兼而有之？

Does z3 supports tagging operators as associative, commutative, or both?

提问人：dde 提问时间：9/20/2017 更新时间：9/20/2017 访问量：149

问：

我想以 SMT 格式编写证明义务，其中某些函数具有一些共同的通用属性（即关联性和交换性）。

一个简单的解决方案是在证明义务中包括相应的公理。我想这意味着对这些属性的推理将在很大程度上取决于量词实例化算法。其他技术，例如重写，可能会更有效率，我想知道 Z3 是否实现了这种技术。API 中存在 Z3_OP_PR_REFLEXIVITY 和 Z3_OP_PR_COMMUTATIVITY 等值表明情况可能如此。

我的第一个问题是：

  • Z3 是否有办法处理用户定义符号的通用属性，而不是通过用户定义公理的量词实例化？

如果答案是肯定的，那么：

  • 哪些是这样的通用属性？

  • 由于据我所知，SMT-LIB 标准没有为用户定义的符号（仅理论符号）固定此类属性，那么声明用户定义符号具有给定属性的 SMT 语法是什么？

Z3 SMT

评论

1赞 alias 9/21/2017
关于 SMT-Lib 中属性的旁注：如果您指的是 属性，我相信这些属性只是允许语法细节来简化编写表达式，实际上并没有向求解器发出运算符是关联的信号。据我所知，在用户级别这样做的唯一方法是输入您提到的量化公理，至少只要您保持使用 SMT-Lib 输入格式。:left-assoc:right-assoc

答： 暂无答案

上一个：C++17 Trans int 到前缀为“0”字符串的快速方法

下一个：为什么 CVC4 产品运算符不适用于套装？