为什么RatNum没有ToDecimal()方法？

Question

我想将RatNum表达式转换为Dot Net小数.RatNum有一个ToDecimalString方法,但不是ToDecimal方法.这有什么理由吗？除了Decimal.Parse(ratnum.ToDecimalString(2))之外还有其他方法可以将RatNum转换为小数吗？谢谢.

Answer 1

对这个问题的简短回答是System.Decimal类型是(非IEEE 754)浮点格式,而Z3的RatNum是有理数的无限精度格式.这是必要的,因为有理数的十进制扩展不一定是有限的(例如,对于1/3).

我们可以使用ToStringDecimal,它采用精度p并生成一个最多为p位的有理数的十进制字符串表示.请注意,这可以是比Int64或Single/Double/Decimal更多的数字.

或者,我们可以使用ToString来生成精确的表示,例如'1/3'.

还有一些函数可以获得有理数的分子和分母,然后可以用它来产生其他格式的小数.

因此,答案很长:Z3是无限精确的,如果解决方案需要近似,则必须在Z3之外完成,或者通过建议的转换为/从字符串转换的方法,或通过其他转换,例如

x.Numerator.Int / x.Denominator.Int

如果已知这些整数不会超过int类型的最大值,并且应用程序没有受到结果的浮点近似的影响.