Z3py: Float32()和BitVecSort(32)之间的强制和值提取

Question

我目前正在试验浮点(FP)理论，结合位向量；我正在使用Z3 4.6.0.0。

我在使用FP API时发现了有限的文档(似乎只有在z3.py本身上才有真正的命中)，所以我尝试提供“完整”的示例，以演示我(相信)应该如何使用该API。

下面是我第一次尝试在Z3py中使用FP理论：

#!/usr/bin/env python

from z3 import *

s = Solver()

#
# Create our value
#
to_find = "-12.345"
fp_val = FPVal(to_find, Float32())

#
# Create our variable
#
fp_var = Const("fp_var", Float32())

#
# Create the constraints
#
s.add(fp_var == fp_val)

assert s.check() == sat, "assertion never fails because the instance is SAT"

m = s.model()

#
# Prints -12.3449993134
#
print eval(str(m.eval(fp_var, model_completion=True)))

# EOF

如果您运行此示例，它将按预期工作，我们确实可以得到fp_var等于(我猜想)离-12.345最近的浮点数(到目前为止，除了使用eval作为Python获取值外)。

我的下一步是尝试将浮点值强制转换为位向量，同时检查非整数值：

#!/usr/bin/env python

from z3 import *

s = Solver()

#
# Create our value
#
to_find = "-12.345"
fp_val = FPVal(to_find, Float32())

#
# Create our variable
#
bv_var = Const("bv_var", BitVecSort(32))

#
# We now use a "cast" to allow us to do the floating point comparison
#
fp_var = fpSignedToFP(RNE(), bv_var, Float32())

#
# Create the constraints
#
s.add(fp_var == fp_val)

#
# This is UNSAT because fpSignedToFP only supports _integers_!
#
assert s.check() == unsat, "instance is UNSAT, so assertion doesn't fail"

# EOF

在本例中，我们尝试将位向量“转换”为浮点值(使用fpSignedToFP)，然后断言浮点值等于我们要寻找的值。然而，这与Z3的文档相匹配，我们得到了UNSAT，因为fpSignedToFP只支持整数。

然后，我开始“变得有创意”，看看是否可以使用fpToSBV API调用的传递性，该调用没有说明它有仅限于整数浮动的限制：

#!/usr/bin/env python

from z3 import *

print get_full_version()

s = Solver()

#
# Create our value
#
to_find = "-12.345"
fp_val = FPVal(to_find, Float32())

#
# Create our variable
#
bv_var = Const("bv_var", BitVecSort(32))

#
# We now create an additional, ancillary variable
#
fp_var = Const("fp_var", Float32())

#
# Create the constraints
#
s.add(fp_var == fp_val)
s.add(bv_var == fpToSBV(RNE(), fp_var, BitVecSort(32)))

assert s.check() == sat, "this example works"

m = s.model()

#
# Prints -12.3449993134
#
print eval(str(m.eval(fp_var, model_completion=True)))

#
# To read out the value from the BV, we create a new variable, assert it is
# the same as the originating BV, and then extract our new variable
#
eval_fp = Const("eval_fp", Float32())
s.add(bv_var == fpToSBV(RNE(), eval_fp, BitVecSort(32)))

assert s.check() == sat, "this cannot change the satisfiability"

m = s.model()

#
# Prints +oo True True
#
print str(m.eval(eval_fp, model_completion=True)),
print m.eval(eval_fp, model_completion=True).isInf(),
print m.eval(eval_fp, model_completion=True).isPositive()

# EOF

为了稍微解释一下这个例子:我们将问题编码为正常的，但不是为浮点表达式创建一个术语，而是创建一个全新的常量，并通过fpToSBV断言我们的位向量等于浮点值。我们对我们希望找到的值的断言是针对我们的浮点值的。如果这个模型是可满足的，那么我们就创建另一个浮点常数，它指向我们原来的位向量，我们试图提取这个常数的值。

这给了一条这样的链子：

• bv_var == fpToSBV(fp_var)
• fp_var == -12.345
• fpToSBV(eval_fp) == bv_var

我原本希望传递性能给fp_var和eval_fp同样的值。然而，当fp_var得到正确的值时，eval_fp则显示为正无穷大！

我还尝试将fpToSBV和fpSignedToFP结合使用，以确定这是否有效(由于fpSignedToFP的局限性，我对此表示怀疑)：

#!/usr/bin/env python

from z3 import *

s = Solver()

#
# Create our value
#
to_find = "-12.345"
bv_val = fpToSBV(RNE(), FPVal(to_find, Float32()), BitVecSort(32))

#
# Create our variable
#
bv_var = Const("bv_var", BitVecSort(32))

#
# Create the constraints
#
s.add(bv_var == bv_val)

assert s.check() == sat, "this example works"

m = s.model()

#
# Floating point constant to evaluate
#
eval_fp = fpSignedToFP(RNE(), bv_var, Float32())

#
# Prints -12.0
#
print eval(str(m.eval(eval_fp, model_completion=True)))

# EOF

这是最成功的，并且实际上给出了一个整数，关闭了我们约束的浮点值(即-12.0)。但是，它仍然不包含小数位之后的值。

因此，我的问题是:在Z3中，是否有可能将浮点值强制转换为位向量，然后又“退出”？如果是的话，应该怎样做呢？或者，位向量/浮点操作是否只是“部分解释”(比如int2bv和朋友)？

更新

在进行了更多的实验之后，我发现以下工作(使用Z3特定的扩展fpToIEEEBV)：

#!/usr/bin/env python

from z3 import *

s = Solver()

#
# Create our value
#
to_find = "-12.345"
fp_val = FPVal(to_find, Float32())

#
# Create our variable
#
bv_var = Const("bv_var", BitVecSort(32))

#
# Convert the value to check to a BV
#
bv_val = fpToIEEEBV(fp_val)

#
# Create the constraints
#
s.add(bv_var == bv_val)

assert s.check() == sat, "this example is SAT, so don't see this"

m = s.model()

#
# Evaluation expression
#
eval_expr = fpBVToFP(bv_var, Float32())

#
# Prints -12.3449993134
#
print eval(str(m.eval(eval_expr)))

# EOF

这是处理这个问题的正确方法吗？

Answer 1

撇开Python的工作方式不谈，这已经在浮点逻辑的定义中指定了，参见此处：http://smtlib.cs.uiowa.edu/theories-FloatingPoint.shtml。

特别是注意到其中一些职能的偏袒性：

“所有fp.to_*函数对于NaN和无穷大输入值都没有指定。此外，对于超出范围的有限数输入(包括fp.to_ubv的所有负数)，fp.to_ubv和fp.to_sbv没有指定。 (= (fp.to_real (_ NaN 8 24)) (fp.to_real (fp c1 c2 C3) 对于所有二元常数c1、c2和c3 (适当的排序)，在这个理论中是可以满足的。“

因此，您所做的(挂起Python特定方面)是按照标准进行的，并有上述警告。

使用交换格式

为了转换到/从IEEE754交换格式，逻辑提供了一种将给定位向量转换为相应浮点的方法：

；从IEEE754-2008交换格式中的单位字符串表示形式，使用m= eb + sb ((_ to_fp eb sb) (_ BitVec m) (_ FloatingPoint eb sb))

另一方面，逻辑是这样说的：

没有将(_ FloatingPoint eb sb)转换为相应的IEEE754-2008二进制格式的功能，它是具有m= eb + sb的位向量(_ BitVec m)，因为(_ NaN eb sb)具有多个定义良好的表示形式。相反，建议采用以下类型的编码，其中f是排序项(_ FloatingPoint eb sb)： (声明- BitVec b () ()) (断言(= ((_ to_fp eb sb) b) f))

再说一遍，所有这些都在http://smtlib.cs.uiowa.edu/theories-FloatingPoint.shtml中