interface - 如何将 Z3 中的 Expr(Const number) 转换为 MPQ/MPFR 中的对象

Question

当我使用Z3-opt（Ocaml版本）解决一些规划问题时，我从 Z3 得到这样的结果：

(+ (/ 31.0 10.0) (* (to_real (- 1)) epsilon ))

这个结果的类型是 Z3.Expr。我想知道如何将这个结果（Z3.Expr）转换为另一个常见的数据类型对象（例如，MPQ/MPFR）。

Z3-opt（Ocaml 版本）是否为此提供了ocaml 接口？

非常感谢。