0

我正在使用 z3py。我的问题是，如何检索Extract节点的边界？我认为Extract这将是一个具有三元数的函数，但它不是：

>>> x = BitVecVal(3, 32)
>>> e = Extract(15, 0, x)
>>> e.decl()
Extract
>>> e.decl().arity()
1
>>> e2 = Extract(7, 0, x)
>>> e2.decl()
Extract
>>> e.decl() == e2.decl()
False

每个Extract操作（显然）由前两个参数输入（我推断这是因为 decls 不相等）。

如果给我一个BitVecRefwhich 是一个Extract操作，我如何判断操作的范围？因此，对于Extract(i, j, x)我想要一个能够让我返回i和j.

4

1 回答 1

2

边界与术语一起被编码为“参数”。这些参数不会作为常规参数传递。python API 不公开对参数的访问，但 C API 公开，并且您可以从 Python 调用这些函数（这只是多一点工作）。

您需要的函数是 Z3_get_decl_int_parameter。

这是使用该功能的示例：http ://rise4fun.com/Z3Py/Rsl8

x = BitVec('x',32)
t = Extract(10,5,x)

f = t.decl()
print Z3_get_decl_int_parameter(t.ctx.ref(), f.ast, 0)
print Z3_get_decl_int_parameter(t.ctx.ref(), f.ast, 1)
于 2013-06-19T07:15:35.660 回答