Retrieve the bounds of an Extract node in z3py

Question

I am using z3py. My question is, how do I retrieve the bounds of an Extract node? I thought Extract would be a function with arity three, but it isn't:

>>> 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

Each Extract operation is typed (apparently) by the first two arguments (I infer this because the decls aren't equal).

If I'm given a BitVecRef which is an Extract operation, how can I tell the bounds of the operation? So for Extract(i, j, x) I want a function that gives me back i and j.

Answer 1

The bounds are encoded as "parameters" together with the term. These parameters don't get passed as regular arguments. The python API does not expose access to parameters, but the C API does, and you can call these functions from Python (it is just a little more work).

The function you need is Z3_get_decl_int_parameter.

Here is a sample using the function: 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)