【发布时间】：2019-07-02 18:34:47
【问题描述】：
我有一个布尔模型，其中变量x 的值是0x1000，现在我想了解是否可以将数字表示为浮点数。如果是的话，我可以举一个例子来说明我应该怎么做吗？
谢谢
【问题讨论】：
-
AFAIK，boolector 似乎还不支持浮点 SMT-LIB 理论。在公式中将 FP 减少为 BV 的想法对我来说听起来很可怕。因此，您可能想尝试其他 smt 求解器。
标签： smt
【发布时间】：2019-07-02 18:34:47
【问题描述】：
不幸的是，我与 boolector 团队确认 fp 理论不受 atm 支持。
【讨论】：