z3 - => 的关联性和 = 的可链接性

Question

Leonardo：根据http://goedel.cs.uiowa.edu/smtlib/papers/smt-lib-reference-v2.0-r10 ​​.12.21.pdf 的第 3.7.1 节，=>是右关联的并且=是可链接的。不过Z3的网络版好像不支持这样的用途。我需要设置一个选项来获得这种行为吗？

谢谢..

Answer 1

不，Z3 3.1（和更早的版本）不支持这两个“功能”。我会将它们添加到 Z3 3.2。