Python 和 Z3:整数和浮点数，如何以正确的方式管理它们? [英] Python and Z3: integers and floating, how to manage them in the correct way?

问题描述

需要 Z3 和 Python 方面的帮助...看起来我太笨了.我的代码:

need help with Z3 and Python...it looks I'm too dumb for this. My code:

from z3 import *

num1 = Int('num1')
num2 = Int('num2')
num3 = Int('num3')

s = Solver()
s.add( 2 * num1 - num2 + 0.5 * num3 == 5412.0)
s.add( 2 * num1 + 3 * num2 + 4 * num3 == 28312.0)

结果如下:

[num3 = 1, num1 = 5568, num2 = 5724]

这并不完全正确:第一个表达式实际上返回 5412.5，而不是 5412.0.我想这与Int"与一些点数"(0.5)的混合使用有关.我实际上需要将numX"保留为Int"，因为它们是整数(这是一个约束).我想我错过了如何管理这种混合情况.有人可以帮我吗?

Which is not completely correct: the first expression actually returns 5412.5, not 5412.0. I guess it has to do with the mixed usage of "Int" with some "point numbers" (0.5). I actually need to keep the "numX" as "Int", since they are integers (this is a constraint). I guess I'm missing how to manage this mixed situation. Someone can help me?

谢谢，

已编辑

感谢别名"的回答，我找到了正确的方向:

Thanks to "alias" answer I got the right direction:

添加

cc1 = RealVal(0.5)

然后在表达式中使用该常量，我得到了正确的结果.

and then using that constant in the expression, I got the correct result.

谢谢大家！

推荐答案

Python 绑定到 Z3 受到弱类型的影响是完全正确的.这在最出乎意料的情况下经常回来咬人.

You're absolutely correct that Python bindings to Z3 suffer from weakly typing. This comes back to bite quite often, when least expected.

在这些情况下，sexpr() 方法是您的朋友.将 print s.sexpr() 添加到程序末尾.它打印以下内容:

In these cases, sexpr() method is your friend. Add print s.sexpr() to the end of your program. It prints the following:

(declare-fun num3 () Int)
(declare-fun num2 () Int)
(declare-fun num1 () Int)
(assert (= (+ (- (* 2 num1) num2) (* 0 num3)) 5412))
(assert (= (+ (* 2 num1) (* 3 num2) (* 4 num3)) 28312))

你可以看到你的0.5变成了0！这完全不是你想要的.欢迎来到我会强迫你让事情适合你"的世界.

And you can see your 0.5 became 0! Which is totally not what you wanted. Welcome to the world of "I'll coerce to make things fit behind your back."

要解决这个问题，您确实需要非常清楚转换.Z3 支持浮点数和实数.(即，具有无限精度.)并且算术在 SMTLib 领域中不会混合和匹配，因此您必须非常小心地构造适当的常量.

To solve this, you really need to be very clear on conversions. Z3 supports floating-point and also real numbers. (i.e., with infinite precision.) And arithmetic doesn't mix-and-match in the SMTLib land, so you have to be very careful on how you construct the proper constants.

这篇关于Python 和 Z3:整数和浮点数，如何以正确的方式管理它们?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！