=>および連鎖可能性=

Question

レオナルド：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（およびそれ以前のバージョン）は、これら2つの '機能' をサポートしていません。 Z3 3.2に追加します。