Просматривая исходный код Z3, я наткнулся на кучу файлов, ссылающихся на QF_FPA, который, по-видимому, обозначает арифметику с плавающей запятой без количественных выражений. Тем не менее, мне кажется, что я не могу найти какую-либо документацию, касающуюся его состояния или того, как его можно использовать через различные внешние интерфейсы (в частности, SMT-Lib2). Это кодировка IEEE-754 FP? Если да, то какие точности / операции поддерживаются? Любая документация будет наиболее полезной ..