Z3 FP 逻辑:产生意想不到的模型 [英] Z3 FP logic: produces unexpected model

问题描述

对于这个问题:http://rise4fun.com/Z3/YNBG

Z3 生产模型:

sat
((s0 FP!val!0))

我期待看到一个真实的数字作为模型.对于这种情况，它几乎就像将 FP 视为一种未解释的排序.有没有办法让Z3在这里产生一个实数?

I was expecting to see a true number as the model. It's almost as if it's treating FP as an uninterpreted sort for this case. Is there a way to get Z3 to produce a real number here?

推荐答案

感谢您报告此问题.事实上，FPA 的模型补全中存在一个错误.该修复程序已在 Codeplex 的不稳定分支中提供.

Thanks for reporting this. Indeed, there was a bug in the model completion for FPA. The fix is already available in the unstable branch at Codeplex.

注意 ==(浮点等于)和 NaN 总是假的，也就是说，在这个例子中，任何 s0 都满足公式.这些值现在完全被正确省略(在 get-model 中)，或者模型以 NaN 完成(对于 get-value 或通常在启用模型完成时).

Note that == (floating point equal) with NaN is always false, i.e., in this example, any s0 satisfies the formula. Such values are now correctly omitted at all (in get-model) or the model is completed with a NaN (for get-value or generally when model completion is enabled).

这篇关于Z3 FP 逻辑:产生意想不到的模型的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！